Logic Based Program Synthesis and Transformation: 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20, 2002, Revised Selected Papers (Lecture Notes in Computer Science, 2664)

✍ Scribed by M. Leuschel (editor)

• Publisher: Springer
• Year: 2003
• Tongue: English
• Leaves: 290
• Category: Library

✦ Synopsis

This book constitutes the thoroughly refereed post-proceedings of the 12th International Workshop on Logic Based Program Synthesis and Transformation, LOPSTR 2002, held in Madrid, Spain in September 2002.

The 15 revised full papers presented together with 7 abstracts were carefully selected during two rounds of reviewing and revision from 40 submissions. The papers are organized in topical sections on debugging and types, tabling and constraints, abstract interpretation, program refinement, verification, partial evaluation, and rewriting and object-oriented development.

✦ Table of Contents

Logic Based
Preface
Program Committee
Table of Contents
Abstract Diagnosis of Functional Programs
1 Introduction
1 Introduction
2 Preliminaries
3 The Semantic Framework
4 Abstract Semantics
4.1 A Case Study: The Domain {\it depth(k)}
5 Abstract Diagnosis of Functional Programs
5.1 Our Case Study
6 Conclusions
References
2 Preliminaries
3 The Semantic Framework
4 Abstract Semantics
4.1 A Case Study: The Domain depth(k)
5 Abstract Diagnosis of Functional Programs
5.1 Our Case Study
6 Conclusions
References
A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene
1 Introduction
2 Description and Properties of PTS}
3 Sequent Calculi for PTS. Properties
4 Related Works and Conclusions
References
Constraint Solver Synthesis Using Tabled Resolution for Constraint Logic Programming
1 Introduction
2 Generation of Primitive Propagation Rules
2.1 The {\sc prim-miner} Algorithm
2.2 Advantage of Tabled Resolution for Rule Generation
2.3 Selection of Interesting Rules and Performance of Generation
2.4 Generation of Primitive Splitting Rules
3 Generation of More General Propagation Rules
4 Generation of Simplification Rules
5 Conclusion and Future Work
References
Translating Datalog-Like Optimization Queries into ILOG Programs
References
Tabling Structures for Bottom-Up Logic Programming
References
A General Framework for Variable Aliasing:Towards Optimal Operatorsfor Sharing Properties
1 Introduction
2 Notation
3 The Concrete Semantics
3.1 Concrete Domain and Operators
3.2 A Different Concrete Domain
4 The Abstract Domain $@mathtt {ShLin}^{omega }$
4.1 Unification and Matching
4.2 A Characterization for Resultant Sharing Groups
5 Domains for Linearity and Aliasing
5.1 King's Domain
5.2 The Domain $@mathtt {Sharing}times @mathtt {Lin}$
6 Conclusion and Future Work
References
Two Variables per Linear Inequalityas an Abstract Domain
1 Introduction
2 Abstract Domain
2.1 Convex Hull and Closure
2.2 Two-Variables per Inequality Domain
2.3 Complete Form for the Two-Variables per Inequality Domain
2.4 Ordering the Two-Variables per Inequality Domain
2.5 Entailment between Three Inequalities
3 Completion: A Variant of Nelson's Satisfiability Algorithm
3.1 Complexity of the {\it complete} Operation
3.2 Satisfiability and the {\complete} Operation
4 Join: Planar Convex Hull on Each Projection
5 Projection
6 Entailment
7 Widening
7.1 Widening for Termination
7.2 Widening for Tractability
8 Future Work
9 Related Work
10 Conclusion
References
Convex Hull Abstractions in Specialization of CLP Programs
1 Introduction
2 A Constraint Domain
2.1 Linear Arithmetic Constraints
2.2 Constrained Atoms and Conjunctions
3 An Algorithm for Specialization with Constraints
3.1 Generation of Calls and Answers
3.2 Approximation Using Convex Hulls and Widening
3.3 Generation of the Specialized Program
3.4 Correctness of the Specialization
4 Examples
4.1 Specialization Strategy
4.2 Assessment
5 Related Work
6 Final Remarks
6.1 Future Work
References
Collecting Potential Optimisations
Introduction and Motivation
Optimisation Derivation Framework
References
An Operational Approach to Program Extraction in the Calculus of Constructions
1 Introduction
2 Background
3 The Theory of Specifications
3.1 Triplicating ${sf C}$ for the Theory of Specifications
3.2 Splitting the Syntax
3.3 Operational Semantics for Program Extraction
3.4 Typing Pairs
3.5 An Example of Program Extraction
4 Properties
5 Further Work
References
A Appendix
Refinement of Higher-Order Logic Programs
1 Introduction
2 Type System
2.1 Types
2.2 Terms
3 Wide-Spectrum Language
3.1 Basic Constructs
3.2 Procedures
3.3 Refinement
3.4 Example Specification and Implementation
4 Higher-Order Refinement
5 Semantics
5.1 Variables and Values
5.2 Bindings, States and Predicates
5.3 Term Evaluation
6 Program Execution
6.1 Executions
6.2 Semantic Function for Commands
7 Refinement
8 Recursion
9 Procedures and Equality
10 Conclusions
References
A Generic Program for Minimal Subsets with Applications
1 Introduction
2 Generic Computation of Minimal Subsets
2.1 The Program Development
2.2 Refinements
3 Applications
3.1 Vertex Cover
3.2 Transitive Reduction
3.3 Some Further Applications
4 Concluding Remarks
References
Justification Based on Program Transformation* (Extended Abstract)
References
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
1 Introduction
2 The Weak Monadic Second Order Theoryhfill penalty -@M of One Successor
3 Translating WS1S Formulas into Normal Logic Programs
4 The Transformation Rules
5 The Unfold/Fold Synthesis Method
6 Deciding WS1S via the Unfold/Fold Proof Method
7 An Application to the Verification of Infinite State Systems: The Dynamic Bakery Protocol
8 Related Work and Conclusions
References
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers
1 Introduction
2 A Generic Framework to Develop Propositional SAT–Provers
2.1 Semantic Tableaux
2.2 Sequents and the Gentzen System
2.3 Davis–Putnam Method
3 Formalizing the Generic SAT–Prover in ACL2
3.1 Definition of the Generic Algorithm
3.2 Termination
4 Instantiating the Generic Framework
4.1 A Tableaux Based SAT–Prover
4.2 Sequent and Davis–Putnam Based SAT–Provers
4.3 Execution Examples
5 Conclusions and Further Work
References
A Proof System for Information Flow Security
1 Introduction
2 Basic Notions: The SPA Language
3 The $P_BNDC$ Security Property
4 Hypothetical $P_BNDC$ Processes
5 Systems of Definitions
6 Example: A Process Monitor
7 Related Works and Conclusion
References
Forward Slicing of Multi-paradigm Declarative Programs Based on Partial Evaluation
1 Introduction
2 Foundations
3 Forward Slicing
3.1 Monovariant/Monogenetic Partial Evaluation
3.2 Computing Program Dependences
3.3 Extraction of the Slice
4 Backward Slicing
5 Implementation
6 Conclusions and Related Work
References
A Fixed Point Semanticsfor Logic Programs Extended with Cuts
1 Introduction
2 Preliminaries
3 A Bottom-Up Semantics for Pure Prolog
4 A Bottom-Up Semantics for Pure Prolog Extended with Cut
5 Discussion
5.1 An Application of the Semantics
5.2 Related Work
References
Abstract Partial Deduction Challenged (Summary)
References
Towards Correct Object-Oriented Design Frameworks in Computational Logic (Extended Abstract)
References
Mapping Modular SOS to Rewriting Logic
1 Introduction
2 Modular SOS and Rewriting Logic
2.1 Modular Structural Operational Semantics
2.2 Rewriting Logic
3 {\cal M}{\it to}{\cal R}: Mapping {\it MSOS} to {\it RWL}
3.1 From {\it MSOS} Specifications to Rewrite Theories
3.2 The Mapping from {\it ALTS} to {\cal R}-systems
4 The Correctness Proof of {\cal M} {\it to} {\cal R}
5 The MSOS-SL Interpreter
6 Conclusion
References
Program Synthesis Based on the Equivalent Transformation Computation Model
References
Author Index