Formal Methods Talks in 2007

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)

2007

Date Speaker Title Extra
Aug 24 Oleg Mürk Deductive Verification of C Programs with KeY (master thesis) abstract
Jun 1 Helga Velroyen Nontermination proofs of imperative programs abstract
Mar 30 Kristofer Björkström Accelerating NCBI blast over ten times on a FPGA with the high-level language Mitrion-C abstract
Mar 16 Yueh-Ting Liao Design and Analysis of Adders using Lava abstract
Feb 9 Cezar Ionescu Relation-based Algorithms in a Haskell-based BSP (Bulk Synchronous Processing) Model abstract
Jan 19 Roderick Bloem Synthesizing Systems from their Specifications abstract, Note: Time 11:15


A Compositional Approach to the Combination of Combinational and Sequential Equivalence Checking of Circuits Without Known Reset States

Date: Sep 13
Speaker: Per Bjesse
Links: Note: Thursday
Abstract:
As the pressure to produce smaller and faster designs increases, the need for formal verification of sequential transformations increases proportionally. In this talk we describe a framework that attempts to extend the set of designs that can be equivalence checked. Our focus lies in integrating sequential equivalence checking into a standard design flow that relies on combinational equivalence checking today. In order to do so, we can not make use of reset state or reset sequence information (as this is not given in combinational equivalence checking), and we need to mitigate the complexity inherent in the traditional sequential equivalence checking algorithms. Our solution integrates combinational and sequential equivalence checking in such a way that the individual analyses benefit from each other. The experimental results show that our framework can verify designs which are out of range for pure sequential equivalence checking methods aimed designs with unknown reset states.


Deductive Verification of C Programs with KeY (master thesis)

Date: Aug 24
Speaker: Oleg Mürk
Abstract:
In this thesis we present a Dynamic Logic for deductive verification of type-safe C programs (CDL). It allows verification of C programs w.r.t. operation contracts and invariants. Our approach is based on the KeY Dynamic Logic (DL) and tool, previously targeted on Java. We have extended the KeY architecture to support language variability --- DLs for new programming languages can be implemented as a plugin to the KeY tool. Based on this we have created KeY-C --- a tool for deductive verification of C programs.


Nontermination proofs of imperative programs

Date: Jun 1
Speaker: Helga Velroyen
Abstract:
Software which ends up in an endless loop and thus does not terminate, can become a serious problem in real life software systems. In my thesis I developed a method to detect endless loops in imperative programs. I implemented a tool which uses a theorem prover (KeY), which implements Dynamic Logic, to generate and refine invariants incrementally. Those invariants are then used to prove the non-termination of the program. The tool works fully automatic and the results so far are promising.


Accelerating NCBI blast over ten times on a FPGA with the high-level language Mitrion-C

Date: Mar 30
Speaker: Kristofer Björkström
Abstract:
One of the fastest and most used program packages for comparing biological sequences, such as DNA and proteins, today is NCBI:s Blast family, which is a heuristic sequence alignment tool kit. But the Blast kit cannot cope with the exponential increase in size of the biological databases. This thesis presents a way to accelerate the two Blast programs blastP and megablast over ten times by implementing them on Xilinx's XC4LX200 FPGA with the help of Mitrionics AB's high-level language Mitrion-C.


Design and Analysis of Adders using Lava

Date: Mar 16
Speaker: Yueh-Ting Liao
Abstract:
Lava is a Haskell-based system for describing and verifying circuits. In this master's project, we study the usefulness of Lava for designing and analysing arithmetic circuits. We use Lava in comparing three different parallel prefix adder designs based on papers by Knowles, Nicolas, and Choi. SMV is used to verify that the circuits generated by Lava are actually adders and Modelsim to check that the generated VHDL netlists are well-formed. Finally, Synopsys Design Compiler is used to compare the prefix networks that perform the carry calculations in the three adders for power consumption, delay and area. In the talk, we will show how Lava was used to write the adder and prefix network generators, as well as showing the results of the comparison. We will discuss the suitability of Lava for this kind of research on circuit design and analysis. We gratefully acknowledge Synopsys' donation of a license for Design Compiler and related tools.


Relation-based Algorithms in a Haskell-based BSP (Bulk Synchronous Processing) Model

Date: Feb 9
Speaker: Cezar Ionescu
Abstract:
We present a Haskell model of a class of parallel computations known as Bulk-Synchronous Parallel. The model is designed to allow the specification of parallel programming tasks, so that solutions can be derived, proven to be correct or at least, since the model is implemented in Haskell, tested in a simple, "clean room" environment. The model is "monadic", in that the main data type involved in parallel computations is an instance of the Monad class. The "do notation" provided by Haskell for monads gives the usage of our BSP model an imperative "look", making it suitable for programmers with less experience in functional programming. After the introduction of the elements of the model, we will present an example of its use in the context of a simple computational pattern, the "relation-based algorithm".


Synthesizing Systems from their Specifications

Date: Jan 19
Speaker: Roderick Bloem
Links: Note: Time 11:15
Abstract:
I will talk about automatic synthesis of circuits from specifications given in Linear Temporal Logic. (That is, you specify what the circuit should do, and our tool builds the circuit for you.) I will skim over the theory, describe an application to program repair, show a case study and discuss problems and research directions.