Logic-Based Program Synthesis and Transformation: 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8–10, 2019, Revised Selected ... Computer Science and General Issues)

✍ Scribed by Maurizio Gabbrielli (editor)

• Publisher: Springer
• Year: 2020
• Tongue: English
• Leaves: 270
• Category: Library

✦ Synopsis

This book constitutes the thoroughly refereed post-conference proceedings of the 29th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2019, held in Porto, Portugal, in October 2019. The 15 revised full papers were carefully reviewed and selected from 32 submissions. In addition to the 15 papers, this volume includes 2 invited papers.
The symposium cover all aspects of logic-based program development, stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large. This year LOPSTR extends its traditional topics to include also logic-based program development based on integration of sub-symbolic and symbolic models, on machine learning techniques and on differential semantics. The papers are grouped into the following topics: static analysis, program synthesis, constraints and unification, debugging and verification, and program transformation.

✦ Table of Contents

Preface
Organization
Invited Papers
Reversibilization in Functional and Concurrent Programming
Horn Clauses and Tree Automata for Imperative Program Verification
Contents
Static Analysis
1
On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics
1 Introduction
2 Basic notions in denotational semantics
3 Termination specification
4 Fixpoint induction principle
5 Impossibility to prove termination by fixpoint induction with a denotational semantics
6 Iteration induction principle
7 Impossibility to prove termination by iteration induction
8 Generalized iteration induction principle
9 Proving total correctness by generalized iteration induction
10 Parameter dependency
11 Recursive non-termination
12 Proving termination by a variant/convergence function
13 Equivalence of the termination proof by generalized iteration induction and by variant/convergence function principle
14 Extension to total correctness
15 Application to the while iteration
16 Conclusion
Acknowledgements
References
A General Framework for Static Cost Analysis of Parallel Logic Programs
1 Introduction
2 Overview of the Approach
3 The Parametric Cost Relations Framework for Sequential Programs
4 Our Extended Resource Analysis Framework for Parallel Programs
4.1 Solving Cost Recurrence Relations Involving max Operation
5 Implementation and Experimental Results
6 Related Work
7 Conclusions
References
Incremental Analysis of Logic Programs with Assertions and Open Predicates
1 Introduction
2 Background
3 An Approach to Modular Generic Programming: Traits
4 Goal-Dependent Abstract Interpretation
4.1 Goal-Dependent Program Analysis
5 Incremental Analysis of Programs with Assertions
5.1 The Incremental Analyzer of Programs with Assertions
5.2 Use Cases
6 Experiments
7 Related Work
8 Conclusions
A Assertions
References
Computing Abstract Distances in Logic Programs
1 Introduction
2 Background and Notation
3 Distances in Abstract Domains
3.1 Distances in Lattices and Abstract Domains
3.2 Distances in Logic Programming Domains
4 Distances Between Analyses
5 Experimental Evaluation
6 Related Work
7 Conclusions
References
Program Synthesis
Synthesizing Imperative Code from Answer Set Programming Specifications
1 Introduction
2 Background
3 Motivating Example
4 Synthesizing Code for Graph Coloring
5 Synthesis Assumptions
6 Synthesis Task
6.1 Syntax-Directed Translation
6.2 Synthesis Procedure
6.3 Transformation Rules
6.4 Efficiency of the Synthesized Code
6.5 Proof of Correctness
7 Conclusion
References
Verified Construction of Fair Voting Rules
1 Introduction
2 Concepts and Definitions from Social Choice Theory
3 Composable Modules and Compositional Structures
3.1 Electoral Modules
3.2 Sequential Composition
3.3 Revision Composition
3.4 Parallel Composition
3.5 Loop Composition
3.6 A Simple Example
4 Verified Modular Construction Framework
4.1 Isabelle and Higher-Order Logic (HOL)
4.2 Verified Construction Based on Composition Rules
5 Case Study
6 Related Work
7 Conclusion
References
Constraints and Unification
Solving Proximity Constraints
1 Introduction
2 Preliminaries
3 Solving Unification Problems
3.1 Pre-unification Rules
3.2 Rules for Neighborhood Constraints
4 Final Remarks
References
A Certified Functional Nominal C-Unification Algorithm
1 Introduction
2 Background
2.1 Nominal Terms, Permutations and Substitutions
2.2 Freshness and -equality
2.3 Nominal C-Unification
3 Specification
3.1 Auxiliary Functions
3.2 Main Algorithm
3.3 Examples
4 Formalization
4.1 Termination
4.2 Soundness and Completeness
5 Interesting Points of Formalization and Implementation
6 Conclusion and Future Work
References
Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming
1 Introduction
2 Related Work
3 Background
3.1 s(CASP)
3.2 Event Calculus
4 From Event Calculus to s(CASP)
4.1 Modeling BEC with s(CASP)
4.2 Translating the BEC Axioms into s(CASP)
4.3 Translation of the Narrative
4.4 Continuous Change: A Complete Encoding
5 Examples and Evaluation
6 Conclusions
A F2LP Encoding of the Light Scenario
B Adapted F2LP Translation of the Light Scenario with Increased Precision
References
Debugging and Verification
An Integrated Approach to Assertion-Based Random Testing in Prolog
1 Introduction and Motivation
2 Using LPtest Within the Ciao Model
3 Test Case Generation
4 Integration with Static Analysis
5 Shrinking
6 A Case Study
7 Related Work
8 Conclusions and Future Work
References
Trace Analysis Using an Event-Driven Interval Temporal Logic
1 Introduction
2 Related Work
3 Event-Driven Systems and Logic eLTL
3.1 Syntax and Semantics of eLTL
3.2 Examples
3.3 Comparison with LTL
4 Implementation
5 Conclusions
References
The Prolog Debugger and Declarative Programming
1 Introduction
2 Prolog Debugger
2.1 Byrd Box Model and LD-Resolution
2.2 Debugger Output
2.3 Obtaining Top-Level Traces
3 Diagnosis
3.1 Diagnosing Incorrectness
3.2 Prolog Debugger and Incorrectness
3.3 Diagnosing Incompleteness
3.4 Prolog Debugger and Incompleteness
4 Conclusions
References
Program Transformation
A Port Graph Rewriting Approach to Relational Database Modelling
1 Introduction
2 Background
2.1 Relational Databases
2.2 Port Graph Rewriting and Porgy
3 Port Graphs for Database Modelling
3.1 A Visual Domain Specific Language for Database Modelling
3.2 Variadic Rewriting Rules
4 Computing the Syntactic Closure of
4.1 Rewriting Rules
4.2 Syntactic Closure Strategy
4.3 Example of Application
4.4 Visual Analysis of the Closure
4.5 Correctness
5 Finding a Minimal Cover
6 Conclusion and Future Work
References
Generalization-Driven Semantic Clone Detection in CLP
1 Introduction and Motivation
2 Semantic Clones: Setting the Stage
3 Generalization-Driven Clone Detection Process
4 Conclusions and Future Work
References
Semi-inversion of Conditional Constructor Term Rewriting Systems
1 Introduction
2 The Semi-inversion Algorithm—An Overview
3 Conditional Constructor Systems and Semi-inversion
3.1 Preliminaries for Conditional Term Rewriting
3.2 Conditional Constructor Systems
3.3 Semi-inverse
3.4 Modeling Programming Languages and Evaluation Strategies
4 The Semi-inversion Algorithm
4.1 Control of Rule Generation
4.2 Local Semi-inversion of Conditional Rules
4.3 A Heuristic Approach to Reordering Conditions
4.4 Correctness of the Semi-inversion Algorithm
5 Application of the Semi-inverter
5.1 Discrete Simulation of a Free Fall
5.2 Encrypter and Decrypter
5.3 Inverted Inverter
6 Conclusion
References
Author Index