We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. The core of our approach is a specification style that prescribes a way to assign a level expression to each method such that each callee’s level is below the caller’s, even in the presence of dynamic binding. The specification style yields specifications that properly hide implementation details. The main idea is to use multisets of method names as levels, and to associate with each object levels that abstractly reflect the way the object is built from other objects. A method’s level is then defined in terms of the method’s own name and the levels associated with the objects passed as arguments. We first present the specification style in the context of programs that do not modify object fields. We then combine it with separation logic and abstract predicate families to obtain an approach for programs with heap mutation. In a third step, we address concurrency, by incorporating an existing approach for verifying deadlock freedom of channels and locks. Our main contribution here is to achieve information hiding by using the proposed termination levels for lock ordering as well. Also, we introduce call permissions to enable elegant verification of termination of programs where threads cause work in other threads, such as in thread pools or fine-grained concurrent algorithms involving compare-and-swap loops. We explain how our approach can be used also to verify the liveness of nonterminating programs.

A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic solution to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems.

We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.

The ”state explosion problem” can be alleviated by using partial order reduction techniques. These methods rely on expanding only a fragment of the full state space of a program, which is sufficient for verifying the formulas of temporal logics LTL −X or CTL −X * (i.e., LTL or CTL * without the next state operator). This is guaranteed by preserving either a stuttering maximal trace equivalence or a stuttering bisimulation between the full and the reduced state space. Since a stuttering bisimulation is much more restrictive than a stuttering maximal trace equivalence, resulting in less powerful reductions for CTL −X * , we study here partial order reductions that preserve equivalences ”in-between”, in particular a stuttering simulation which is induced by the universal fragment of CTL: −X * , called ACTL −X * The reductions generated by our method preserve also branching simulation and weak simulation, but surprisingly, they do not appear to be included into the reductions obtained by Peled's method for verifying LTL −X properties. Therefore, in addition to ACTL −X * reduction method we suggest also an improvement of the LTL −X reduction method. Moreover, we prove that reduction for concurrency fair version of ACTL −X * is more efficient than for ACTL −X * .

Abstract. A new notion, covering, generalising independence is introduced. It enables improved effects of partial-order reduction techniques when applied to real-time systems. Furthermore, we formulate a number of locally checkable conditions for covering that can be used as the basis for a practical algorithm. Correctness is proven with respect to a chosen discretisation method.

Abstract To specify and verify real-time systems, we consider a real-time version of temporal logic called Explicit Clock Temporal Logic. Timing properties are specified by extending the classical framework of temporal logic with a special variable which explicitly refers to a global notion of time. Programs are written in an Occam-like real-time language with synchronous message passing. To show that a program satisfies a specification, we formulate a proof system which is proved to be sound and relatively complete. The proof system is compositional, which makes it possible to decompose the design of a large system into the design of subsystems. This is shown by the verification of a small part of an avionics system.

In this paper we advance the radical notion that a computational model based on the reals provides a more abstract description of concurrent and reactive systems, than the conventional integers based behavioral model of execution sequences. The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a fully abstract temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of finite variability, we achieve a balanced formalism that is insensitive to finite stuttering, but can recognize infinite stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.

A compositional temporal logic proof system for the specification and verification of concurrent programs is presented. Versions of the system are developed for shared variables and communication based programming languages that include procedures.