Search

The overall problem addressed in this paper is the long-standing problem of program correct- ness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent) ob- jects. The method defines correctness in terms of a simulation relation between the transition system which specifies the program semantics and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the particular model of active objects considered in this paper. As a proof-of-concept we apply our method to the correctness of a parallel simulator of multicore memory systems.

This paper introduces a dynamic logic extension of separation logic. The assertion language of separation logic is extended with modalities for the five types of the basic instructions of separation logic: simple assignment, look-up, mutation, allocation, and de-allocation. The main novelty of the resulting dynamic logic is that it allows to combine different approaches to resolving these modalities. One such approach is based on the standard weakest precondition calculus of separation logic. The other approach introduced in this paper provides a novel alternative formalization in the proposed dynamic logic extension of separation logic. The soundness and completeness of this axiomatization has been formalized in the Coq theorem prover.

The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

We present a novel assertional proof method for reasoning about global invariant properties of active objects in the context of the Abstract Behavioral Specification (ABS) language. The main result of this paper is a formal justification of the proof method which establishes both its soundness and completeness with respect to a formally defined operational trace semantics.

We present a novel assertional proof method for reasoning about global invariant properties of active objects in the context of the Abstract Behavioral Specification (ABS) language. The main result of this paper is a formal justification of the proof method which establishes both its soundness and completeness with respect to a formally defined operational trace semantics.

We introduce a new way of reasoning about invariance in terms of footprints in a program logic for object-oriented components. A footprint of an object-oriented component is formalized as a monadic predicate that describes which objects on the heap can be affected by the execution of the component. Assuming encapsulation, this amounts to specifying which objects of the component can be called. Adaptation of local specifications into global specifications amounts to showing invariance of assertions, which is ensured by means of a form of bounded quantification which excludes references to a given footprint.

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and translate Isabelle theorems to user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning.

We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.

The project files for the article 'Integrating ADTs in KeY and their Application to History-based reasoning.'

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and translate Isabelle theorems to user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning.

We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.

This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.

Software libraries, such as the Java Collection Framework, are used by many applications: Thus their correctness is of utmost importance. The state-of-the-art KeY system can be used to formally reason about program correctness of Java programs. Recently, KeY has been used to show major flaws in the Java Collection Framework. However, some methods are challenging for verification, namely those involving parameters of interface type. This lecture discussed a new history-based specification method for reasoning about the correctness of clients and arbitrary implementations of interfaces, and the Collection interface in particular.

Active objects interact via asynchronous messages which specify method invocations. In contrast to the run to completion mode of method execution, mechanisms for suspending the execution of a method allow an active object to schedule cooperatively its methods in a co-routine manner. In this paper, we show how cooperative scheduling can be reduced to a run to completion mode of execution. We do so by a formal translation using a guarded command language for describing the execution of method bodies.

In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java’s Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).

As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework.

The project files for the article `A Tutorial on Verifying LinkedList using KeY'. The archive contains: A bundled version of KeY, version 2.6.3. This requires a recent version of Java Runtime Edition (JRE) to be executed, say OpenJDK8. A number of stub contracts (jre/ directory).A skeleton LinkedList source file (src/java/util/LinkedList.old) for the reader of the tutorial to fill in the methods and contracts.The LinkedList source file after all modifications have been done (src/java/util/LinkedList.java)A number of proof files that can be loaded in KeY, that verify the correctness of the methods with respect to their contract as given in the solution.

This is a tutorial paper on using KeY to demonstrate formal verification of state-of-the-art, real software. In sufficient detail for a beginning user of JML and KeY, the specification and verification of part of a corrected version of the java.util.LinkedList class of the Java Collection framework is explained. The paper includes video material that shows recordings of interactive sessions, and project files with solutions. As such, this material is also interesting for the expert user and the developer of KeY as a ‘benchmark’ for specification and (automatic) verification techniques.

We present a formal translation of a resource-Aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-Translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

This is a Maude implementation of concolic execution for a guarded commands language.

This repository consists of the proof files for the paper "History-based Specification and Verification of Java Collections in KeY".

Active objects interact via asynchronous messages which specify method invocations. In contrast to the run to completion mode of method execution, mechanisms for suspending the execution of a method allow an active object to schedule cooperatively its methods in a co-routine manner. In this paper, we show how cooperative scheduling can be reduced to a run to completion mode of execution. We do so by a formal translation using a guarded command language for describing the execution of method bodies.

As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework.

In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java’s Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).

Software libraries, such as the Java Collection Framework, are used by many applications: Thus their correctness is of utmost importance. The state-of-the-art KeY system can be used to formally reason about program correctness of Java programs. Recently, KeY has been used to show major flaws in the Java Collection Framework. However, some methods are challenging for verification, namely those involving parameters of interface type. This lecture discussed a new history-based specification method for reasoning about the correctness of clients and arbitrary implementations of interfaces, and the Collection interface in particular.

This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.

We present a formal translation of a resource-Aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-Translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

The project files for the article `A Tutorial on Verifying LinkedList using KeY'. The archive contains: A bundled version of KeY, version 2.6.3. This requires a recent version of Java Runtime Edition (JRE) to be executed, say OpenJDK8. A number of stub contracts (jre/ directory).A skeleton LinkedList source file (src/java/util/LinkedList.old) for the reader of the tutorial to fill in the methods and contracts.The LinkedList source file after all modifications have been done (src/java/util/LinkedList.java)A number of proof files that can be loaded in KeY, that verify the correctness of the methods with respect to their contract as given in the solution.

This is a tutorial paper on using KeY to demonstrate formal verification of state-of-the-art, real software. In sufficient detail for a beginning user of JML and KeY, the specification and verification of part of a corrected version of the java.util.LinkedList class of the Java Collection framework is explained. The paper includes video material that shows recordings of interactive sessions, and project files with solutions. As such, this material is also interesting for the expert user and the developer of KeY as a ‘benchmark’ for specification and (automatic) verification techniques.

Symbolic execution is an important technique for software analysis, which enables systematic model exploration by following all possible execution paths for a given program. For multithreaded shared variable programs, this technique leads to a state space explosion. Partial order reduction is a technique which allows equivalent execution paths to be recognized, reducing the state space explosion problem. This paper provides formal justifications for these techniques in a multithreaded setting by proving the correctness and completeness of symbolic execution for multithreaded shared variable programs, with and without the use of partial order reduction. We then show how these formal justifications carry over to prove the soundness and relative completeness of a proof system for such multithreaded shared variable programs in dynamic logic, such that partial order reduction can be used to simplify the proof construction by mitigating the state space explosion.

In concurrent object models, objects encapsulate local state, schedule local processes, interact via asynchronous method calls, and methods of different objects are executed concurrently. In this paper, we introduce a compositional tra

In this paper, we provide a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. We first introduce such a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables.

Asynchronous Actor-based programming has gained increasing attention as a model of concurrency and distribution. The Abstract Behavioral Specification (ABS) language is an actor-based programming language that has been developed for both the modeling and formal analysis of distributed systems. In ABS, actors are modeled as concurrent objects that communicate by asynchronous method calls. Return values are also communicated asynchronously via return statements and so-called futures. Many modern distributed software applications require a form of continuous interaction between their components which consists of streaming data from a server to its clients. In this paper, we extend the ABS language in order to support the streaming of data. We introduce the notion of “future-based data streams” by augmenting the syntax, type system, and operational semantics of ABS. As a proof of concept, we further discuss a prototype implementation for supporting future-based data streams on top of ABS, and discuss the impact of the use of these data streams in ABS on the performance in the implementation of a distributed application for the generation of social networks.

This paper describes the development of a parallel simulator of a multicore memory system from a model formalized as a structural operational semantics (SOS). Our implementation uses the Abstract Behavioral Specification (ABS) language, an executable, active object modelling language with a formal semantics, targeting distributed systems. We develop general design patterns in ABS for implementing SOS, and describe their application to the SOS model of multicore memory systems. We show how these patterns allow a formal correctness proof that the implementation simulates the formal operational model and discuss further parallelization and fairness of the simulator.

Structural Operational Semantics (SOS) provides a general format to describe a model as a transition system with very powerful synchronization mechanisms. Actor systems are distributed, asynchronously communicating units of computation with encapsulated state, with much weaker means of synchronizing between actors. In this paper, we discuss an implementation of a SOS model using actors in the object-oriented actor language ABS and how to argue that global properties about the model are inherited from the SOS level to the actor implementation. The work stems from a case study modelling the memory system of a cache-coherent multicore architecture.

This archive contains a formal specification of Java's linked list. The archive contains an annotated version of java.util.LinkedList using the Java Modeling Language. Additionally, it includes the KeY version used to formally verify the annotated methods, and the corresponding proof files.

Structural Operational Semantics (SOS) provides a general format to describe a model as a transition system with very powerful synchronization mechanisms. Actor systems are distributed, asynchronously communicating units of computation with encapsulated state, with much weaker means of synchronizing between actors. In this paper, we discuss an implementation of a SOS model using actors in the object-oriented actor language ABS and how to argue that global properties about the model are inherited from the SOS level to the actor implementation. The work stems from a case study modelling the memory system of a cache-coherent multicore architecture.

This paper describes the development of a parallel simulator of a multicore memory system from a model formalized as a structural operational semantics (SOS). Our implementation uses the Abstract Behavioral Specification (ABS) language, an executable, active object modelling language with a formal semantics, targeting distributed systems. We develop general design patterns in ABS for implementing SOS, and describe their application to the SOS model of multicore memory systems. We show how these patterns allow a formal correctness proof that the implementation simulates the formal operational model and discuss further parallelization and fairness of the simulator.

In concurrent object models, objects encapsulate local state, schedule local processes, interact via asynchronous method calls, and methods of different objects are executed concurrently. In this paper, we introduce a compositional trace semantics for concurrent objects and provide an axiomatic characterization of the general properties of reachable traces, that is, traces that can be generated by a concurrent object program. The main result of this paper is a soundness and completeness proof of the axiomatic characterization.

Asynchronous Actor-based programming has gained increasing attention as a model of concurrency and distribution. The Abstract Behavioral Specification (ABS) language is an actor-based programming language that has been developed for both the modeling and formal analysis of distributed systems. In ABS, actors are modeled as concurrent objects that communicate by asynchronous method calls. Return values are also communicated asynchronously via return statements and so-called futures. Many modern distributed software applications require a form of continuous interaction between their components which consists of streaming data from a server to its clients. In this paper, we extend the ABS language in order to support the streaming of data. We introduce the notion of “future-based data streams” by augmenting the syntax, type system, and operational semantics of ABS. As a proof of concept, we further discuss a prototype implementation for supporting future-based data streams on top of ABS, and discuss the impact of the use of these data streams in ABS on the performance in the implementation of a distributed application for the generation of social networks.

In this paper, we provide a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. We first introduce such a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables.

In this paper, we introduce a Java library for actors integrated seamlessly with futures and supporting coroutines. Coroutines allow actors to suspend the execution of a message and possibly schedule other messages before resuming the suspended continuation. As such coroutines enhance actors as a major building block for constructing software components. The library is used together with a compiler to generate code from an application model into an executable program in Java. A formal description of the translation process is provided together with the most important library methods. We highlight the importance of having a scalable and efficient implementation by means of some typical benchmarks which model a large number of tasks, coroutines and actors.

We discuss an extension of the coordination modeling language Paradigm. The extension is geared towards data-dependent interaction among components, where the coordination is influenced by possibly distributed data. The approach is illustrated by the well-known example of a bakery where tickets are issued to serve clients in order. Also, it is described how to encode Paradigm models with data in the process language of the mCRL2 toolset for further analysis of the coordination.