Monday 14 |
09:00 - 09:45 |
Cliff Jones |
| Refining Rely/Guarantee
(joint work with Ian Hayes and Rob Colvin)
slides
|
09:45 - 10:30 |
Klaus Havelund |
| Monitoring with Data Automata
slides
abstract
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.
|
10:30 - 11:00 |
Coffee break |
11:00 - 12:30 |
Sandrine Blazy |
| Formal verification of a static analyzer
(joint work with David Pichardie, Jacques-Henri Jourdan, Vincent
Laporte and Xavier Leroy)
slides
|
12:30 - 14:00 |
Lunch |
14:00 - 14:45 |
Florent Kirchner |
| Combining formal tools for the source code verification
of functional temporal properties
slides
|
14:45 - 15:30 |
Wolfgang Paul |
| Multi core processors and casino programming
slides
|
15:30 - 16:00 |
Coffee break |
16:00 - 17:30 |
discussion |
| designing a verification-friendly programming language
| |
|
Tuesday 15 |
09:00 - 09:45 |
Tony Hoare (1/2) |
| Algebra, Denotational Semantics, and the Debugging of
Concurrent Programs
slides
abstract
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.
|
09:45 - 10:30 |
Arnd Poetzsch-Heffter |
| Proving Backward Compatibility for Object-Oriented Libraries
(joint work with Yannick Welsch)
slides
abstract
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.
|
10:30 - 11:00 |
Coffee break |
11:00 - 12:30 |
Peter Puschner |
| Enforcing Constant Execution Times for Software
slides
abstract
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.
|
|
12:30 - 14:00 |
Lunch |
14:00 - 15:00 |
Natarajan Shankar |
| Report on Verified Software Competition (VSCOMP) 2014
slides
|
15:00 - 15:30 |
Coffee break |
15:30 - 17:00 |
discussion |
| on a possible EU project (Jim Woodcock)
| |
|
Wednesday 16
|
09:00 - 09:45 |
Tony Hoare (2/2) |
| Algebra, Operational Semantics, and Verification Logic
slides
abstract
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.
|
09:45 - 10:30 |
Claude Marché |
| Beyond SPARK 2014: The ProofInUse project
slides
|
10:30 - 11:00 |
Coffee break |
11:00 - 12:30 |
Shaz Qadeer |
| Automated and modular refinement for reasoning about concurrency
slides
abstract
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.
|
12:30 - 14:00 |
Lunch |
14:00 - 15:00 |
Natarajan Shankar |
| ADD for CPS
slides
|