Skip to main content

Über dieses Buch

This book constitutes the thoroughly refereed post-conference proceedings of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2013, held in Madrid, Spain, in September 2013.

The 13 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 21 submissions during two rounds of reviewing and improvement. LOPSTR traditionally solicits papers in the areas of specification, synthesis, verification, transformation, analysis, optimization, composition, security, reuse, applications and tools, component-based software development, software architectures, agent-based software development, and program refinement.



Formalization and Execution of Linear Algebra: From Theorems to Algorithms

In this work we present a formalization of the Rank Nullity theorem of Linear Algebra in Isabelle/HOL. The formalization is of interest because of various reasons. First, it has been carried out based on the representation of mathematical structures proposed in the HOL Multivariate Analysis library of Isabelle/HOL (which is part of the standard distribution of the proof assistant). Hence, our proof shows the adequacy of such an infrastructure for the formalization of Linear Algebra. Moreover, we enrich the proof with an additional formalization of its computational meaning; to this purpose, we choose to implement the Gauss-Jordan elimination algorithm for matrices over fields, prove it correct, and then apply the Isabelle code generation facility that permits to execute the formalized algorithm. For the algorithm to be code generated, we use again the implementation of matrices available in the HOL Multivariate Analysis library, and enrich it with some necessary features. We report on the precise modifications that we introduce to get code execution from the original representation, and on the performance of the code obtained. We present an alternative verified type refinement of vectors that outperforms the original version. This refinement performs well enough as to be applied to the computation of the rank of some biomedical digital images. Our work proves itself as a suitable basis for the formalization of numerical Linear Algebra in HOL provers that can be successfully applied for computations of real case studies.
Jesús Aransay, Jose Divasón

Information Flow in Object-Oriented Software

This paper contributes to the investigation of object-sensitive information flow properties for sequential Java, i.e., properties that take into account information leakage through objects, as opposed to primitive values. We present two improvements to a popular object-sensitive non-interference property. Both reduce the burden on analysis and monitoring tools. We present a formalization of this property in a program logic – JavaDL in our case – which allows using an existing tool without requiring program modification. The third contribution is a novel fine-grained specification methodology. In our approach, arbitrary JavaDL terms (read ‘side-effect-free Java expressions’) may be assigned a security level – in contrast to security labels being attached to fields and variables only.
Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich

A Transformational Approach to Resource Analysis with Typed-Norms

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along a program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. The main contribution of this paper is a transformational approach to resource analysis with typed-norms. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also sketch a simple analysis that can be used to automatically infer the required, useful, typed-norms from programs.
Elvira Albert, Samir Genaim, Raúl Gutiérrez

A Finite Representation of the Narrowing Space

Narrowing basically extends rewriting by allowing free variables in terms and by replacing matching with unification. As a consequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still represents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (possibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.
Naoki Nishida, Germán Vidal

Energy Consumption Analysis of Programs Based on XMOS ISA-Level Models

Energy consumption analysis of embedded programs requires the analysis of low-level program representations. This is challenging because the gap between the high-level program structure and the low-level energy models needs to be bridged. Here, we describe techniques for recreating the structure of low-level programs and transforming these into Horn clauses in order to make use of a generic resource analysis framework (CiaoPP). Our analysis, which makes use of an energy model we produce for the underlying hardware, characterises the energy consumption of the program, and returns energy formulae parametrised by the size of the input data. We have performed an initial experimental assessment and obtained encouraging results when comparing the statically inferred formulae to direct energy measurements from the hardware running a set of benchmarks. Static energy estimation has applications in program optimisation and enables more energy-awareness in software development.
Umer Liqat, Steve Kerrison, Alejandro Serrano, Kyriakos Georgiou, Pedro Lopez-Garcia, Neville Grech, Manuel V. Hermenegildo, Kerstin Eder

From Outermost Reduction Semantics to Abstract Machine

Reduction semantics is a popular format for small-step operational semantics of deterministic programming languages with computational effects. Each reduction semantics gives rise to a reduction-based normalization function where the reduction sequence is enumerated. Refocusing is a practical way to transform a reduction-based normalization function into a reduction-free one where the reduction sequence is not enumerated. This reduction-free normalization function takes the form of an abstract machine that navigates from one redex site to the next without systematically detouring via the root of the term to enumerate the reduction sequence, in contrast to the reduction-based normalization function.
We have discovered that refocusing does not apply as readily for reduction semantics that use an outermost reduction strategy and have overlapping rules where a contractum can be a proper subpart of a redex. In this article, we consider such an outermost reduction semantics with backward-overlapping rules, and we investigate how to apply refocusing to still obtain a reduction-free normalization function in the form of an abstract machine.
Olivier Danvy, Jacob Johannsen

Towards Erlang Verification by Term Rewriting

This paper presents a transformational approach to the verification of Erlang programs. We define a stepwise transformation from (first-order) Erlang programs to (non-deterministic) term rewrite systems that compute an overapproximation of the original Erlang program. In this way, existing techniques for term rewriting become available. Furthermore, one can use narrowing as a symbolic execution extension of rewriting in order to design a verification technique. We illustrate our approach with some examples, including a deadlock analysis of a simple Erlang program.
Germán Vidal

Extending Co-logic Programs for Branching-Time Model Checking

Co-logic programming is a programming language allowing each predicate to be annotated as either inductive or coinductive. Assuming the stratification restriction, a condition on predicate dependency in co-logic programs (co-LPs), a top-down procedural semantics (co-SLD derivation) as well as an alternating fixpoint semantics has been given. In this paper, we present some extensions of co-LPs, especially focusing on the relationship with the existing alternating tree automata approaches to branching-time model checking. We first consider the local stratification restriction to allow a more general class of co-LPs, so that we can encode the CTL satisfaction relation as a co-LP, which is a direct encoding of the standard alternating automata by Kupferman et al. Next, we consider non-stratified co-LPs based on the Horn \(\mu \)-calculus. We give a proof procedure, co-SLD derivation with the parity acceptance condition, for non-stratified co-LPs, and show that it is sound and complete for a class of non-stratified co-LPs. Its application to a goal-directed top-down proof procedure for normal logic programs is also discussed.
Hirohisa Seki

Towards the Implementation of a Source-to-Source Transformation Tool for CHR Operational Semantics

Constraint Handling Rules (CHR) is a high-level committed-choice language based on multi-headed and guarded rules. Over the past decades, several extensions to CHR and variants of operational semantics were introduced. In this paper, we present a generic approach to simulate the execution of a set of different CHR operational semantics. The proposed approach uses source-to-source transformation to convert programs written under different CHR operational semantics into equivalent programs in the CHR refined operational semantics without the need to change the compiler or the runtime system.
Ghada Fakhry, Nada Sharaf, Slim Abdennadher

A Logical Encoding of Timed $$\pi $$ -Calculus

We develop a logical encoding of the operational semantics of timed \(\pi \)-calculus: a real-time extension of Milner’s \(\pi \)-calculus. This executable encoding is based on Horn logical semantics of programming languages and directly leads to an implementation for timed \(\pi \)-calculus. This implementation can be used for modeling and verification of real-time systems and cyber-physical.
Neda Saeedloei

A New Hybrid Debugging Architecture for Eclipse

During many years, Print Debugging has been the most used method for debugging. Nowadays, however, industrial languages come with a trace debugger that allows programmers to trace computations step by step using breakpoints and state viewers. Almost all modern programming environments include a trace debugger that allows us to inspect the state of a computation in any given point. Nevertheless, this debugging method has been criticized for being completely manual and time-consuming. Other debugging techniques have appeared to solve some of the problems of Trace Debugging, but they suffer from other problems such as scalability. In this work we present a new hybrid debugging technique. It is based on a combination of Trace Debugging, Algorithmic Debugging and Omniscient Debugging to produce a synergy that exploits the best properties and strong points of each technique. We describe the architecture of our hybrid debugger and our implementation that has been integrated into Eclipse as a plugin.
Juan González, David Insa, Josep Silva

Compiling a Functional Logic Language: The Fair Scheme

We present a compilation scheme for a functional logic programming language. The input program to our compiler is a constructor-based graph rewriting system in a non-confluent, but well-behaved class. This input is an intermediate representation of a functional logic program in a language such as Curry or \(\mathcal{TOY}\). The output program from our compiler consists of three procedures that make recursive calls and execute both rewrite and pull-tab steps. This output is an intermediate representation that is easy to encode in any number of programming languages. We formally and tersely define the compilation scheme from input to output programs. This compilation scheme is the only one to date that implements a deterministic strategy for non-deterministic computations with a proof of optimality and correctness.
Sergio Antoy, Andy Jost

Generating Specialized Interpreters for Modular Structural Operational Semantics

Modular Structural Operational Semantics (MSOS) is a variant of Structural Operational Semantics (SOS). It allows language constructs to be specified independently, such that no reformulation of existing rules in an MSOS specification is required when a language is extended with new constructs and features.
Introducing the Prolog MSOS Tool, we recall how to synthesize executable interpreters from small-step MSOS specifications by compiling MSOS rules into Prolog clauses. Implementing the transitive closure of compiled small-step rules gives an executable interpreter in Prolog. In the worst case, such interpreters traverse each intermediate program term in its full depth, resulting in a significant overhead in each step.
We show how to transform small-step MSOS specifications into corresponding big-step specifications via a two-step specialization by internalizing the rules implementing the transitive closure in MSOS and ‘refocusing’ the small-step rules. Specialized specifications result in generated interpreters with significantly reduced interpretive overhead.
Casper Bach Poulsen, Peter D. Mosses


Weitere Informationen

Premium Partner