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)

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. 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

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 in July 2006 in conjunction with ICALP 2006, PPDP 2006, and CSFW 2006.

The 14 revised full papers presented together with 2 invited talks were carefully selected and revised from 41 submissions during two rounds of reviewing and improvement. The papers are organized in topical sections on tools for program development, partial evaluation and program transformation, security and synthesis, debugging and testing, as well as termination and analysis.

This book constitutes the thoroughly refereed post-conference proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2012, held in Leuven, Belgium in September 2012.