Logic-Based Program Synthesis and Transformation

Name: Logic-Based Program Synthesis and Transformation | 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers

María Alpuente(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. April 2011

X, 249 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-20551-4 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

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

Systemvoraussetzungen

Als PDF speichern Als Link merken