Logic-Based Program Synthesis and Transformation
20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers
Erschienen am 21. April 2011
X, 249 Seiten
978-3-642-20551-4 (ISBN)
Beschreibung
This book constitutes the thoroughly refereed post-proceedings of the 20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010, held in Hagenberg, Austria in July 2010. The 13 revised full papers presented together with two invited papers were carefully reviewed and selected from 26 submissions. Among the topics covered are specification, synthesis, verification, analysis, optimization, specialization, security, certification, application and tools, program/model manipulation, and transformation techniques for any programming language paradigm.
Weitere Details
Weitere Ausgaben
Andere Ausgaben
María Alpuente
Logic-Based Program Synthesis and Transformation
20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers
Buch
05/2011
1. Auflage
Springer
53,49 €
Versand in 7-9 Tagen
Inhalt
- Title Page
- Preface
- Organization
- Table of Contents
- Three Syntactic Theories for Combinatory Graph Reduction
- Introduction
- Two Inter-derivable Semantic Artifacts for Storeless Combinatory Graph Reduction
- A Reduction Semantics
- A Storeless Abstract Machine
- Summary and Conclusion
- Preprocessing Combinatory Terms into Term Graphs
- A Reduction Semantics
- A Storeless Abstract Machine
- Summary and Conclusion
- Store-Based Combinatory Graph Reduction
- A Reduction Semantics
- A Store-Based Abstract Machine
- Summary and Conclusion
- Related Work
- Conclusion and Future Work
- References
- Analysis of Air Traffic Track Data with the AutoBayes Synthesis System
- Introduction
- The AutoBayes Program Synthesis System
- Multivariate Clustering of Aircraft Track Data
- AutoBayes Clustering Models
- Experiments and Results
- Change-Point Detection Models
- The CAS/Mach Transition
- Change-Point Detection with AutoBayes
- CDA Detection
- Conclusions
- References
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
- Introduction
- Simplicial Models
- A Mathematical Model
- The EAT Model
- The Kenzo Model
- Schema of the Proof
- Proving that EAT Objects Are Simplicial Sets
- Proving That Kenzo Objects Are Simplicial Sets
- ACL2 Technical Issues
- Correctness of Face and Degeneracy Operators
- A Generic Simplicial Set Theory
- Obtaining ACL2 Correctness Certifications for Concrete Kenzo Simplicial Sets Families
- Conclusions and Future Work
- References
- Graph Generation to Statically Represent CSP Processes
- Introduction
- The Syntax and Semantics of CSP
- Context-Sensitive Synchronized Control-Flow Graphs
- An Algorithm to Generate the CSCFG
- Correctness
- Conclusions
- References
- Verification of the Schorr-Waite Algorithm - From Trees to Graphs
- Introduction
- Schorr-Waite on Pure Trees
- Imperative Language and Its Memory Model
- Implementation for Pure Trees
- Schorr-Waite on Trees with Pointers
- Implementation for Trees with Pointers
- Related Work
- Conclusions
- References
- MikiBeta : A General GUI Library for Visualizing Proof Trees System Description and Demonstration
- Introduction
- Overview of Mikiß
- Using Mikiß
- Definition of Judgements Using Two-Level Types
- Four Generic Functions
- Definition of Inference Rules
- Writing Arbitrary Code
- The Mikiß System
- Fix.F : A Functor Generating Data Modules
- Various Supporting Functions in Fix.F
- Miki.F: A Functor Generating a GUI
- Examples
- The ? Calculus with Let Polymorphism
- The ? Calculus with Shift and Reset
- System F
- Combinatory Logic
- Other Logical Systems
- Related Work
- Conclusion and Future Work
- References
- Compositional CLP-Based Test Data Generation for Imperative Languages
- Introduction
- CLP-Based Test Case Generation
- From Imperative to Equivalent CLP Programs
- Symbolic Execution
- Method Summaries Obtained by TDG
- A Compositional CLP-Based TDG Approach
- Composition in Symbolic Execution
- Approaches to Compositional TDG
- Handling Native Code during Symbolic Execution
- Compositionality of Different Coverage Criteria
- Reusing Summaries Obtained for Different Criteria
- Experimental Results
- Conclusions
- References
- On Inductive Proofs by Extended Unfold/Fold Transformation Rules
- Introduction
- A Framework for Unfold/Fold Transformation
- Transformation Rules
- Application Conditions of Transformation Rules
- An Extended Framework for Unfold/Fold Transformation System
- Negative Unfolding with Existential Variables
- Simultaneous Folding
- Negative Folding and the Correctness of the Extended Transformation System
- Related Work and Concluding Remarks
- References
- Non-termination Analysis of Logic Programs Using Types
- Introduction
- Preliminaries
- Logic Programming
- Types
- Non-failure Analysis and Program Specialization
- Moded-Typed SLD-Trees and the NFG Transition
- Moded-Typed SLD-Trees and Loop Checking
- The $NFG$ Transition
- Correlation with Concrete Queries
- Typed Non-termination Analysis with Non-failing Goals
- Non-termination of Inclusion Loops
- Input-Generalizations
- Program Specialization
- Conclusion and Future Work
- References
- Scaling Up Algorithmic Debugging with Virtual Execution Trees
- Introduction
- Declarative Debugging
- A New Architecture for Declarative Debuggers
- Redefining the Strategies for Declarative Debugging
- Implementation
- Adapting the Architecture for Other Languages
- Conclusions
- References
- Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation
- Introduction
- Specifying CTL Properties by CLP Programs
- Verifying Infinite State Systems by Specializing CLP Programs
- Generalization Strategies
- The $Generalize&Fold$ Procedure
- Well-Quasi Orderings and Generalization Operators on Linear Constraints
- Experimental Evaluation
- Conclusions
- References
- Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
- Introduction
- Preliminaries
- Termination Graphs
- Transformation into Definite Logic Programs
- Transformation into Dependency Triple Problems
- Implementation and Experiments
- Conclusion
- References
- A Hybrid Approach to Conjunctive Partial Evaluation of Logic Programs
- Introduction
- Pre-processing Stage
- Partial Evaluation Stage
- Post-processing Stage
- Experimental Evaluation
- Concluding Remarks and Future Work
- References
- Abstract Diagnosis of First Order Functional Logic Programs
- Introduction
- Notations and Assumptions
- The Semantic Framework
- Incremental Answer Semantics
- Abstraction Scheme
- Abstract Diagnosis of Functional Logic Programs
- Applicability of the Framework
- Conclusions
- References
- The First-Order Nominal Link
- Introduction
- Background
- Nominal Structure: From Nominal to First-Order
- Quadratic Unification Algorithm
- Nominal Unification as a Relation on Term Nodes
- A Quadratic Nominal Unification Algorithm
- Conclusions
- References
- Author Index
