FATS: Formal Approaches To Software
Seminar series at ETH Zürich
Bertrand Meyer


What are the FATS seminars?

"Formal Approaches To Software" refers broadly to mathematically-based techniques helping the software process, with particular emphasis on verification and proofs. The field has made considerable advances in recent years, and has become increasingly relevant to practical software development.

The FATS seminars at ETH Zürich provide a discussion medium for those interested in the progress of this field. A non-exhaustive list of relevant topics includes program verification, theory of programming and programming languages, logics for computation, formal development techniques, formal specification. Reports on practical applications of these techniques in software projects are also welcome.

Time and place

The seminars are normally held on Wednesday afternoons, from 16:15 to 17:15 in room RZ F21. The format of the seminars is typically an informal presentation on a particular topic with the goal of fostering discussion among participants. Several presentations are from people from the Software Engineering group working in the field, but guest speakers (from other groups and institutions) are also invited to present.

Program, Fall 2009

16 September 2009, Wednesday
15:00-16:00, IFW E42
Reiner Hähnle
Chalmers University of Technology, Sweden
Title: Abstract Interpretation & Symbolic Execution
Abstract:
Static (i.e., compile-time) analysis methods for software validation and verification are rapidly gaining in importance. State-of-art methods and tools are able to prove security and functional properties of real-world software. Three of the most successful approaches include type systems, abstract interpretation, and deductive verification. So far, all three have been used in different contexts and were mostly investigated by different communities. In the talk I will demonstrate that the well-known paradigma of symbolic program execution offers a unified view on these three techniques with logic-based deduction as a common implementation base. Using an example from non-interference analysis, I will point out some of the synergies and new research perspectives that can be obtained from such a unified view.
23 September 2009, Wednesday
16:15-17:15, RZ F21
Martin Nordio
Chair of SW Engineering, ETH Zürich
Title: Proof Transformations for Object-Oriented Programs
Abstract:
In modern development schemes the processing of programs often involves an intermediate step of translation to some intermediate code, often called "bytecode". This intermediate code is executed through interpretation or a second phase of compilation known as "jitting". The execution of bytecode programs can produce unexpected behavior, which may comprise security and correctness of a software system. An important issue to address is the verification of these programs also known as mobile code. Expanding on the ideas of Proof-Carrying Code (PCC), in this talk we will introduce a verification process for bytecode programs based on proof-transforming compilation. The approach consist of translating proofs of object-oriented programs to bytecode proofs. The verification process is performed at the level of the source program making interaction easier than verifying bytecode programs. Then, a proof-transforming compiler translates automatically a contract-equipped program and its proof into bytecode representing both the program and the proof. Our approach addresses not only type safety properties, as in the original PCC work, but full functional correctness as expressed by the original contracts.
30 September 2009, Wednesday
16:15-17:15, RZ F21
Michael J. C. Gordon
University of Cambridge, UK
Title: Mechanically Proving Hoare Formulae
Abstract:
I will give an introduction to methods for proving Hoare formulae based both on the forward computation of postconditions and on the backwards computation of preconditions. Although precondition methods are better known, computing postconditions provides a verification framework that encompasses methods ranging from symbolic execution to full deductive proof of correctness.
7 October 2009, Wednesday
16:15-17:15, RZ F21
Cristiano Calcagno
Imperial College London, UK
Title: Compositional Shape Analysis by means of Bi-Abduction
Abstract:
We describe a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits -- increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision -- to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger programs (e.g., an entire Linux distribution) to test scalability and graceful imprecision.
14 October 2009, Wednesday
16:15-17:15, RZ F21
Nadia Polikarpova
Chair of SW Engineering, ETH Zürich
Title: Dynamic contract inference with Daikon and CITADEL
Abstract:
A dynamic contract detector is a tool that determines conditions holding throughout a software system execution. After these conditions have been found developers can assume that they also hold for all other executions and therefore form a specification (a set of contracts) of the system. One of the best known tools built on this principle is Daikon, developed in 2000 by Michael Ernst et al. To work with a particular programming language Daikon requires a language-specific front-end. At the Chair of Software Engineering we have developed such a front-end (called CITADEL) for the Eiffel programming language. In this lecture we will discuss the ideas behind Daikon and several heuristics that make its simple approach realistic. We will also discuss the specifics of CITADEL, some experimental results of effectiveness of dynamic contract inference and have a short demo.
21 October 2009, Wednesday
16:15-17:15, RZ F21
Gilles Barthe
Madrid Institute for Advanced Studies (iMdea), Spain
Title: Certificate Translation
Abstract:
Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature, it is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers.
Certificate translation is a general method to transfer to code consumers evidence gained through verification of source code; it relies on the notion of certificate, used in Proof-Carrying Code to convey to the code consumer independently verifiable evidence that programs respect policies. The talk provides sufficient conditions of existence for algorithms that transform certificates of source programs into certificates of compiled programs, and show that many common transformations comply with these conditions.
22 October 2009, Thursday
17:00-18:00, IFW E42
Jim Woodcock
University of York, UK
Title: The Verified Software Initiative & the Tokeneer Experiment
Abstract: We describe an experiment conducted as part of a pilot project in the Verified Software Initiative (VSI). We begin by recounting the background to the VSI and its six initial pilot projects, and give an update on the current progress of each project. We describe one of these, the Tokeneer ID Station in greater detail. Tokeneer was developed by Praxis High Integrity Systems and SPRE for the US National Security Agency, and it has been acclaimed by the US National Academies as representing best practice in software development. To date, only two errors have been found in Tokeneer, and the entire project archive has been released for experimentation within the VSI. We describe the first experiment using the Tokeneer archive, and our objective is to investigate the dependability claims for Tokeneer as a security-critical system. Our experiment uses a model-based testing technique that exploits formal methods and tools to discover 12 anomalous scenarios. We discuss four of these.
28 October 2009, Wednesday
15:00-16:00, RZ F21, and
16:15-17:15, RZ F21
Carroll Morgan
The University of New South Wales, Australia
Title: Development of non-interference-style secure implementations by program refinement
Abstract:
"Classical" program development by refinement is a technique for ensuring that source-level program code remains faithful to the semantic goals set out in its corresponding specification. Until recently the method has not extended to security-style properties, principally because classical refinement semantics is inadequate in security contexts, a difficulty known as te "Refinement Paradox".
The Shadow Semantics recently introduced (MPC 2006, Estonia) is an abstraction of probabilistic program semantics that is rich enough to distinguish between refinements that do preserve noninterference security properties and those that don't. In this talk I'll give a formal development of Private Information Retrieval [Chor 1999]; in doing so I'll explore some of the issues raised when considering statistical- as well as one-off attacks in the security-and-refinement context.

Armin Biere
Johannes Kepler University, Austria
Title: Introduction to Bounded Model Checking
Abstract:
One of the most important industrial applications of SAT is currently Bounded Model Checking (BMC). This technique is typically used for formal hardware verification in the context of Electronic Design Automation. But BMC has successfully been applied to many other domains as well. In practice, BMC is mainly used for falsification, which is concerned with violations of temporal properties. In this talk, we will also discuss complete extensions, including k-induction and interpolation. These extensions allow to prove properties.

4 November 2009, Wednesday
16:15-17:15, RZ F21
Daniel Kröning
Oxford University, UK
Title: Symbolic Counter Abstraction for Concurrent Software
Abstract:
The trend towards multi-core computing has made concurrent software an important target of computer-aided verification. Unfortunately, Model Checkers for such software suffer tremendously from combinatorial state space explosion. We show how to apply counter abstraction to real-world concurrent programs to factor out redundancy due to thread replication. The traditional global state representation as a vector of local states is replaced by a vector of thread counters, one per local state. In practice, straightforward implementations of this idea are unfavorably sensitive to the number of local states. We present a novel symbolic exploration algorithm that avoids this problem by carefully scheduling which counters to track at any moment during the search. Our experiments are carried out on Boolean programs, an abstraction promoted by the SLAM project. To our knowledge, this marks the first application of counter abstraction to programs with non-trivial local state spaces, and results in the first scalable Model Checker for concurrent Boolean programs.
11 November 2009, Wednesday
16:15-17:15, RZ F21
Joel Ouaknine
Oxford University, UK
Title: Time-Bounded Verification
Abstract:
I will discuss some recent results on verification problems for timed systems over time intervals of fixed, bounded length, highlighting interesting connections to classical untimed verification and to bounded model checking.
18 November 2009, Wednesday
16:15-17:15, RZ F21
Mauro Pezzè
University of Lugano, Switzerland and University of Milano-Bicocca, Italy
Title: Contextual Data Flow Analysis for Structural Testing of Object-Oriented Systems
Abstract:
The state based behavior of object oriented software is not well captured by classic structural testing approaches. In this lecture, we will understand how we can use data flow analysis to identify the state based behavior of object oriented software. We will see the benefits and the limitations of classic data flow analysis applied to state variables, and we will study contextual data flow analysis, an extension of classic analysis that identifies intra as well as inter-class interactions.
25 November 2009, Wednesday
16:15-17:15, RZ F21
Patrick Cousot
École Normale Supérieure, Paris, France
Title: An Informal Introduction to Static Analysis and Verification by Abstract Interpretation
2 December 2009, Wednesday
16:15-17:15, RZ F21
Jason (Yi) Wei
Chair of SW Engineering, ETH Zürich
Title: Automatic testing of object-oriented software
Abstract: Contracts provide specifications for software, which can be used to facilitate automatic testing. In this lecture, we'll discuss the basic idea of contract-based random testing, as well as techniques to improve its effectiveness. Topics include test case generation based on object distance, precondition satisfaction through guided object selection, contract inference and test case extraction during debugging.
9 December 2009, Wednesday
16:15-17:15, RZ F21
Andreas Leitner
Google Switzerland
Title: The Testing Process at Google
Abstract:
Testing is an integral part of the software development process at Google. This lecture will explain the purpose and the scope of testing at Google. It will cover the relationship between testing and software development, providing examples of testing technologies currently used.
The list of talks will be extended during the semester. Please recheck regularly for the updated program.

Contacts

The FATS seminars coordinators are Carlo A. Furia and Sebastian Nanz. Please contact the coordinators for any information regarding the seminar and to suggest new topics and speakers.

Access information

The seminar is open to the public, unless otherwise noted.

Credits

The seminar status is a pure research seminar. No credit is available for participating in the seminar.

Previous editions