IFIP WG 1.9/2.15 Verified Software

Cliff Jones

Klaus Havelund

The field of runtime verification has during the last decade seen a multitude of systems for monitoring event sequences (traces) emitted by a running system. The objective is to ensure correctness of a system by checking its execution traces against formal specifications representing requirements. A special challenge is monitoring of data parameterized events, where monitors have to keep track of the combination of control states as well as data constraints, relating events and the data they carry across time points. This poses a challenge wrt. efficiency of monitors, as well as expressiveness of logics. We present a form of automaton, referred to as data automata, suited for monitoring sequences of data-carrying events. This form of automata allows states to be parameterized with data, forming named records, which are stored in an efficiently indexed data structure. Data automata are characterized by allowing transition conditions to refer to other parameterized states, and by allowing transitions sequences, giving the look and feel of temporal logic. The presented automaton concept is inspired by rule-based systems, especially the RETE algorithm, which is one of the well-established algorithms for executing rule-based systems. We present an optimized external DSL for data automata, as well as a comparable unoptimized internal DSL (API) in the Scala programming language, in order to compare the two solutions.

Coffee break

Sandrine Blazy

Lunch

Florent Kirchner

Wolfgang Paul

Coffee break

discussion

Tony Hoare (1/2)

A denotational semantics gives a mathematical model of the relationship between a program and all its possible executions in any environment and on any computer system. It thereby specifies the intended behaviour of a program debugging tool, which displays a trace of the execution of a program that encounters an error. The goal of a model checker is to discover traces that lead to programming errors considered relevant by the programmer. The introduction of concurrency and non-determinacy only increases the need for sophisticated program debugging tools.

To give maximum assistance in locating the error, a display of the trace should selectively display all events that have taken place, at any desired level of granularity, as defined by the syntax tree of the program. It should also display the dependency relation between the events, so that the symptom of a failure can be traced back to its causes, and the results of a change can be traced forward to its effects. Erroneous events such as assertion and assumption failures must be indicated, and also erroneous dependencies, such as interferences of one thread inflicted on another.

It turns out that a Denotational Semantics for a concurrent programming language can be based on just these primitives. The operators for sequential composition (;) and concurrent composition (||) and the refinement relation (<) between programs are simply defined, and proved to enjoy the obvious algebraic properties. An understanding of the algebra should be a sufficient prerequisite for effective use of any tool that is based on the semantics.

Arnd Poetzsch-Heffter

We develop a fully abstract trace-based semantics for sets of classes in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the package and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap and support class hiding. The soundness and completeness of our approach is proven. Based on this semantics, we develop a technique for checking backward compatibility of packages. The technique is implemented using the Boogie framework as a backend.

Coffee break

Peter Puschner

Some part of our work focuses on software architectures and code-generation strategies that allow us to generate code that is time-predictable and has a small or even zero variation in execution time when executed with different input data.

To achieve this goal we developed the so-called single-path code generation approach. The single-path code generation produces code that executes the same sequence of instructions for all inputs, i.e., it avoids input-dependent branches in the control flow. To achieve this, the single-path code generator uses predicated instructions instead of data-dependent branches. The iteration count of all generated loops in the code are constant.

The proposed code-generation approach targets at all applications that benefit from constant execution times of software. Examples for such applications are real-time applications that need invariable timing, as well as applications with high security needs. Wrt. security, our approach can help to inhibit attacks that would otherwise exploit data-dependent execution times as a side channel.

Lunch

Natarajan Shankar

Coffee break

discussion

Tony Hoare (2/2)

An operational semantics is a deduction system that describes how a program should be executed. It specifies the intended function of an implementation of the language by compilers and interpreters. The basic judgement of the deduction system is a Milner transition r ->q-> p . Here, r is the program to be executed, q is a possible first action of the execution, and p is the rest of the program (continuation) which remains to be executed after q is completed. The transition can be defined algebraically by the algebraic inequation q ; p < r . The deduction system that Milner used to define CCS can be proved sound with respect to the algebra.

A verification logic is a deduction system which describes how a proof of correctness of the program can be constructed. It specifies the intended function of program verifiers and analysers. The basic judgement is a Hoare triple {p} q {r} . Here q is the program that remains to be executed, p is a precondition, describing the effect of the program executed so far, and r is a postcondition, describing the overall effect when q is completed. For efficient proof, p and r are usually descriptions of memory state, but in the presence of concurrency it is useful to allow them to be arbitrary programs, which by definition describe their own behaviour. The triple can then be defined by the algebraic inequation p;q < r . The deduction system used by O'Hearn for Concurrent Separation Logic can then be proved sound with respect to the algebra.

In many cases the soundness proof can be reversed, to prove the algebraic laws on the basis of the conjunction of the Operational Semantics and the Verification Logic. This remarkable unification provides evidence that a toolset including a range of compilers, interpreters, verifiers, analysers, model checkers and debugging aids are mutually consistent.

Claude Marché

Coffee break

Shaz Qadeer

We present CIVL, a language and verifier for concurrent programs based on automated and modular refinement reasoning. CIVL supports reasoning about a concurrent program at many levels of abstraction. Atomic actions in a high-level description are refined to fine-grain and optimized lower-level implementations. Modular specifications and proof annotations, such as location invariants and procedure pre- and post-conditions, are specified separately, independently at each level in terms of the variables visible at that level. We have implemented CIVL as an extension to the Boogie language and verifier. We have used CIVL to refine a realistic concurrent garbage collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.

Lunch

Natarajan Shankar