Formal Methods Talks in 2003
These are the talks and abstracts of talks given in this year.
The list is ordeded in reverse order.
(other years: 2003
| 2004
| 2005
| 2006
| 2007)
2003
MCK, A Model Checker for Knowledge
Date: Dec 2
Speaker: Peter Gammie
Abstract:
This talk will introduce MCK, a system for model checking specifications expressed in the logic of knowledge and time that has been developed at The School of Computer Science and Engineering at the University of New South Wales. I will present a brief overview of the logic of knowledge and time, a few examples drawn from the distributed systems literature to illustrate what the system is capable of, and a discussion of the pragmatics of designing and implementing MCK.
Proving soundness of Stålmarck's method in FOL
Date: Nov 25
Speaker: Magnus Björk
Abstract:
I will give an introduction to semantics of classical first order logic, and soundness proofs. Specifically I will show how to prove soundness of Stålmarck's method in first order logic. I will begin by defining concepts like formulas, domains, interpretations, truth, satisfaction, and substitutions, which are standard in FOL. I will then introduce the special concepts in Stålmarck's method, e.g. rigid vs. universal variables, explicit sets, and logical intersections. Then we will look at some lemmas, and prove some of them. Finally, I'll show the definition of the proof system of Stålmarck's method, and how to prove that derivations are sound.
If you have a copy of my licentiate thesis, then bring it along as a reference. I hope that this talk will contain lots of interaction.
A Coverage Analysis for Safety Property Lists
Date: Nov 18
Speaker: Koen Claessen
Links: draft paper
Abstract:
In property-based formal verification, a natural question that often arises is 'Have we specified enough properties?' In this talk, we provide a way of approximating an answer to this question. We present a relatively cheap analysis that, given the interface of a design under verification, plus a formal safety property list, identifies cases where some outputs of the design are not constrained at all by the properties. For practical reasons, we also provide an easy way for the verification engineer to explicitly state that certain outputs are allowed to be underconstrained. The presented methodology is independent of the used specification language and the underlying verification technology; it can be adapted to most specification languages such as for example Sugar or ForSpec.
Probabilistic Equivalence Checking
Date: Nov 4
Speaker: Rene Krenz
Abstract:
Probabilistic methods in design verification are based on the fundamental idea to compress the specific characteristics of a Boolean function into a single integer hash value. Two Boolean functions will produce the same hash value with 100% certainty if they are equivalent. If the functions are different, the probability that they hash onto the same value is very small, thus resulting in a low probability for producing "false positive" verification results. Relaxing the requirement of 100% correctness may dramatically increase the capacity of verification. After a short introduction to probabilistic verification and their application a new algorithm will be presented to compute the hash values on a circuit graph. It will be shown how dominator relations in the circuit graph are applied to partition the hash value computation.
A Model Generation Style Completeness Proof for Constrained Formula Tableaux with Superposition
Date: Oct 7
Speaker: Martin Giese
Abstract:
A calculus is presented that integrates equality handling by superposition into a free variable tableau calculus. Completeness of the calculus is proved by an adaptation of the model generation technique commonly used for completeness proofs of resolution calculi. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov.
Partitioning induction rules to reduce/simplify user interaction
Date: Oct 3
Speaker: Angela Wallenburg
Abstract:
This is going to be a dry-run of the talk I am going to give at FATES in Montreal, Canada.
Symbolic Trajectory Evaluation
Date: Sep 23
Speaker: Jan-Willem Roorda
Abstract:
To prepare myself and others for Tom Melham's visit next week, I will give an introduction to STE (Symbolic Trajectory Evaluation), a specification/verification method in use at for example Intel.
Temporal Induction by Incremental SAT-solving
Date: May 27
Speaker: Niklas Een
Abstract:
The talk will be a semi-continuation of my Winter-meeting presentation. There I presented two extensions of a SAT-solver, one of which was "Incremental SAT". On Tuesday I will explain how I and Niklas Sörensson used this extension to create a model checker based on induction (new stuff!). I will quickly repeat how a SAT-solver works, so don't worry if you forgot (or slept through) my winter meeting talk.
OCL Specifications for the Java Card API
Date: May 20
Speaker: Daniel Larsson
Abstract:
This Master's thesis discusses the development of OCL specifications for Java Card API, and is part of the KeY project. OCL is a specification language, i.e. it is used to express formally the requirements of a system. The KeY tool is a CASE tool, in which formal methods (formal specification and formal verification) are integrated with contemporary software development techniques. The main purpose of the OCL specifications is to simplify the verification of Java Card programs within the KeY tool. Verification means that one through mathematical and logical methods proves that the implementation fulfils the requirements in the specification. Already existing specifications written in JML, a specification language specially suited for Java, has been used as a starting point for the development of the OCL specifications. OCL is a more general language. Problems that have to be solved are, for instance, how to express in OCL the throwing of exceptions, how to test if a reference variable contains a null value, and how to handle the risk of overflow in the context of arithmetic integer operations. It has been shown that OCL lacks some important properties when it comes to specifying Java programs, but in other aspects is superior to JML.
Simplification Rules for Constrained Formula Tableaux
Date: May 13
Speaker: Martin Giese
Abstract:
Several variants of a first-order simplification rule for non-normal form tableaux using syntactic constraints are presented. These can be used as a framework for porting methods like unit resolution or hyper tableaux to non-normal form free variable tableaux.
Description and Analysis of Multipliers using Lava
Date: Apr 29
Speaker: Emil Axelsson
Abstract:
In this talk I will deal with the question: Is Lava a suitable language for construction of binary multipliers? The most common multiplier methods are described both in general and as Lava descriptions. All methods can be split into two basic steps, so I present a general interface, where any method for the first step can be combined with any method for the second step. This way, a variety of multiplier circuits, all with different properties, can be expressed as higher-level combinations of the two basic steps. It is shown that Lava is a very powerful tool for both constructing and verifying generic binary multipliers. The functional behaviour of Lava allows complex generic networks to be described by small, abstract and easy to understand expressions. I also show how the environment in Lava can be slightly modified, to obtain self-optimising hardware and simple performance estimation methods.
Finite Model Generation for First Order Logic
Date: Apr 22
Speaker: Koen Claessen
Abstract:
In this talk, I will present a finite model finder for first order logic, called "Paradox", that Niklas Sörensson and I have developed recently. The tool works by translating the FOL problem into a sequence of SAT problems, and then using the incremental SAT solver Satnik (written by Niklas) to find the models. We have developed a number of new techniques to improve dramatically on the well-known idea of translating FOL into SAT. I will give an overview of these techniques.
The talk will also contain a number of fun applications of finite model finding.
Modification Conditions: Specifying what a Method Doesn't Do
Date: Mar 25
Speaker: Bernhard Beckert (Universität Karlsruhe)
Abstract:
Software specification languages allow to describe what a function or method does, i.e., in which way its invocation changes the program state. But using pre-/post-condition pairs and invariants, it is difficult to specify what a method does *not* do, i.e., which parts of the state remain unchanged. This difficulty, which is also know as "frame problem", plays an important role in the specification of object-oriented software, where methods often have side-effects. In the KeY project, which aims at integrating object-oriented design and formal verification, we use the Object Constraint Language for specification, Java as the target implementation language, and JavaDL (a variant of Dynamic Logic) for correctness proofs.
In my talk, I explain the frame problem in detail and describe the solution used in the KeY project. We extend specifications by "modification conditions", which specify those elements of a program state state that a method may change. I describe how that knowledge is made use of in a correctness proofs with the JavaDL calculus.
A Translation of SyncCharts into First Order Logic
(a Master's thesis presentation)
Date: Mar 18
Speaker: Hans Svensson
Abstract:
Traditional automatic verification techniques for high-level synchronous systems, such as explicit model checking and symbolic model checking using BDDs or SAT solvers, have known limitations. For example, the verification is limited to explicitly finite systems, and there is a problem with potential exponential blowup in BDD size (or state machine size). Lately a new approach has been taken with a starting point in the much more expressive first order logic (FOL). This means that it is possible to model finite as well as infinite state systems. The correctness of the system can be verified using a FOL theorem prover. To be able to use this kind of verification, one must have a translation of the system into first order logic formulas. SyncCharts is a modeling language that is used to describe reactive systems. The goal of the thesis is to examine the possibility to translate SyncCharts into first order logic and apply formal verification to SyncChart designs.
The presentation will present some parts of the translation, not going into every detail. A brief presentation of some first order logic concepts will be given. The presentation will contain a short introduction to SyncCharts.
Integration of Automated and Interactive Theorem Proving
Date: Mar 11
Speaker: Martin Giese
Abstract:
Various attempts have been made in the past at combining automated theorem provers for classical first order logic and interactive proof systems. All these attempts try to combine pre-existing systems, by translating goals of the interactive theorem prover into the input language for the automaton, and possibly translating back a proof if one was found. In the talk, the disadvantages of such a translation based approach will be discussed. A methodology is developed, which lets the interactive and automated parts share one calculus. As a part of this methodology, an extension to classical 1st order logic called `epsilon terms' will be introduced and explained.
Most of the ideas presented in this talk have been, are currently being, or will hopefully soon be implemented in the prover of the KeY system.
Behaviour of Driverless Vehicles
Date: Feb 18
Speaker: Jan-Erik Eriksson (Saab)
Abstract:
Jan-Erik Eriksson from Saab will present a problem that he has in proving properties about the behaviour of a driverless vehicle. He is involved in building a pilotless aeroplane that is intended to fly in civil airspace. Thus, he is going to need to prove to the authorities that it behaves in reasonable ways! He has proposed a master's project in the area and this meeting is intended to be the beginning of a dialogue about the ways in which formal methods can be applied to this problem. Jan-Erik's first description of the proposed project (a Word document) is here.
A Theorem Proving Approach to Analysis of Secure Information Flow
Date: ? 1
Speaker: Reiner Hähnle
Abstract:
Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches suffer from the need for abstraction and the high cost of building dedicated tools for real programming languages. We recast the information flow problem in a general program logic rather than a problem-specific one. We investigate the feasibility of this approach by showing how a general purpose tool for software verification can be used to perform information flow analyses. We are able to handle phenomena like method calls, loops, and object types for the target language JavaCard. We are also able to prove insecurity of programs and to express declassification of information.