Logic-Based Program Synthesis and Transformation: 16th International Symposium, LOPSTR 2006, Venice, Italy, July 12-14, 2006, Revised Selected Papers (Lecture Notes in Computer Science, 4407)

✍ Scribed by Germán Puebla (editor)

• Publisher: Springer
• Year: 2007
• Tongue: English
• Leaves: 244
• Category: Library

✦ Synopsis

This book constitutes the thoroughly refereed postproceedings of the 16th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2006, held in Venice, Italy, July 2006 in conjunction with ICALP 2006, PPDP 2006, and CSFW 2006. The 14 revised full papers cover tools for program development, partial evaluation and program transformation, security and synthesis, debugging and testing, as well as termination and analysis.

✦ Table of Contents

Title page
Preface
Conference Organization
Table of Contents
How to Talk to a Human: The Semantic Web and the Clash of the Titans
The Semantic Web and XML: The Eternal Quest
The Semantic Web to the Rescue: Closed vs. Open Worlds
Just Aggregation?
The Benefits
The Costs
The C/B Ratio
The Cost of URIs
Another Perspective: Lost in Navigation
Technologies Examples: The Good and the Bad
Talk to a Human: Blogs and the Grillo Case
The Web and the Information Flows
Towards a Web Algebra
Infoshares and Infostructures
Info-extensions
The Future: From Towers to Trees?
CHESS: Systematic Stress Testing of Concurrent Software
Introduction
Algorithm
Application
Firewall Design
Generation of Constraint Solvers
Arm Features
How to Run ARM
Implementation of ARM
Conclusion
Constructing Consensus Logic Programs
Introduction
Preliminaries
Consensus Logic Programs
Computing Consensus Programs
Application to Multi-agent Consensus
Related Work
Conclusion
Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques
Introduction
Offline Partial Evaluation
Watchdog Mode
Experiments
The Web Interface and Semi-automatic Correction
Related Work and Conclusion
Improving Offline Narrowing-Driven Partial Evaluation Using Size-Change Graphs
Introduction
Preliminaries
A Simple Offline NPE Scheme
Ensuring Quasi-termination with Size-Change Graphs
Annotation Procedure
Experimental Evaluation
Conclusions and Future Work
Towards Description and Optimization of Abstract Machines in an Extension of Prolog
Introduction
A Prolog Variant to Describe Virtual Machines
New Features in the Language
Conditions to Ensure Efficient Code Generation
Analysis
Code Generation
Generating Emulators with $ImProlog$
Defining WAM Instructions in $ImProlog$
Assembling the Emulator
Automatic Generation of Abstract Machine Variations
Instruction Set Transformations
Transformations of Instruction Code
Experimental Evaluation
Conclusions
Combining Different Proof Techniques forVerifying Information Flow Security
Introduction
Information Flow Security in an Imperative Language
Security Policy, Labelings, and Security Condition
Combining Calculus
Compositionality Results and Basic Calculus Rules
Plugin: Strong Security
Plugin: Low-Deterministic Security
Soundness and Examples
Information Flow Security of a PDA Application
Plugins for Type-Based Analysis Techniques
Plugin : Boudol and Castellani's Security Type System
Plugin : Sabelfeld and Sand's Security Type System
Exemplary Type-Based Security Analysis
Conclusion
On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors
Introduction
Our Approach
The Monitor Environment
The Prototype
Policy Logic
A Language and Logic for Reference Monitors
The Programming Language
The Program Logic
Synthesis
Checking P3TL Satisfaction
Monitor Synthesis
Proof Synthesis
Discussion
Related Work
Conclusions and Future Work
Synthesis of Asynchronous Systems
Introduction
The Synthesis Problem
Single-Process Synthesis Under Full Scheduling
Preliminaries: Tree Automata
Overview
From Formulas to Automata
From Computation Trees to Strategy Trees
Nondeterminization
Strategy Construction
Complexity
Synthesis of Scheduler-Independent Implementations
Overview
Considering a Scheduler
Quantification over All Schedulers
Complexity
Synthesis with Explicit Assumptions on the Scheduler
Multi-process Synthesis
Conclusions
A Comparative Study of Algorithmic Debugging Strategies
Introduction
Algorithmic Debugging
Algorithmic Debugging Strategies
Single Stepping $(Shapiro, 1982)$
Top-Down Search $(Av-Ron, 1984)$
Divide and Query $(Shapiro, 1982)$
Hat-Delta $(Davie and Chitil, 2005)$
Subterm Dependency Tracking $(MacLarty et al., 2005)$
Dynamic Weighting Search $(Silva, 2006)$
Comparing Strategies
Conclusions
A Program Transformation for Tracing Functional Logic Computations
Introduction
Instrumented Semantics
Program Transformation
Path Information
Labeling Expressions
Global State
Redirecting Arguments
Transforming Expressions
Transforming Projections
Conclusion
Automated Termination Analysis for Logic Programs by Term Rewriting
Introduction
Preliminaries on Logic Programming and Rewriting
Transforming Logic Programs into TRSs
Termination of Infinitary Constructor Rewriting
Experiments and Conclusion
Detecting Non-termination of Term RewritingSystems Using an Unfolding Operator
Introduction
Preliminaries
Unfolding a TRS
Inferring Looping Terms
Eliminating Useless Rules
Abstraction
Detecting Useful Pairs
Experimental Results
Conclusion
Polytool: Proving Termination Automatically Based on Polynomial Interpretations
Introduction
The Polytool System
Experimental Evaluation
Comparison Between Hasta La Vista and Polytool
Comparison Between TALP and Polytool
Conclusions
Grids: A Domain for Analyzing the Distribution of Numerical Values
Introduction
Preliminaries
The Grid Domain
Implementation
Grid Widening
Conclusion
Author Index