CFV'09 Sixth International Workshop on Constraints in Formal Verification
Grenoble, France, June 26, 2009.
a satellite event of CAV'09



Program

9:00 - 10:00 Session 1
9:00 - 10:00 Invited Talk: SAT and SMT Solving in a Multi-Core Environment
Bernd Becker (University of Freiburg, Germany)
10:00 - 10:30 Break
10:30 - 12:30 Session 2
10:30 - 11:00 Robustness Check for Multiple Faults Using Formal Techniques
Stefan Frehse, Goerschwin Fey, Andre Suelflow, and Rolf Drechsler (University of Bremen, Germany)
11:00 - 11:30 A Debug Methodology for Arithmetic Circuits Based on Horner Expansion Diagram
Omid Sarbishei (Sharif University of Technology, Iran), Bijan Alizadeh (University of Tokyo, Japan), Masahiro Fujita (University of Tokyo, Japan)
11:30 - 12:00 A New Prenexing Strategy for Quantified Boolean Formulae with Bi-Implications
Benoit Da Mota, Igor Stéphan, and Pascal Nicolas (LERIA University of Angers, France)
12:00 - 12:30 Using QBF to Increase the Accuracy of SAT-Based Debugging
Andre Suelflow, Goerschwin Fey, and Rolf Drechsler (University of Bremen, Germany)
12:30 - 14:00 Lunch (Provided)
14:00 - 15:30 Session 3
14:00 - 15:00 Invited Talk: SMT Solving and Applications of Bit-Level Constraints
Nikolaj Bjørner (Microsoft Research, U.S.A.)
15:00 - 15:30 Sound, Efficient, Bit-Precise Static Analysis
Yannick Moy, Nikolaj Bjørner, and David Sielaff (Microsoft Research, U.S.A.)
15:30 - 16:00 Break
16:00 - 17:00 Session 4
16:00 - 16:30 Enclosure Constraints for Floating Point Software Verification
Jan Duracz, Amin Farjudian, and Michal Konecny (Aston University, U.K.)
16:30 - 17:00 Randomized Metric Embeddings for Analyzing Protein Folding Pathway Constraints
Sumit K. Jha (Carnegie Mellon University, U.S.A.), and Susmit Jha (UC Berkeley, U.S.A.)


Overview

Formal verification is of crucial significance in the development of hardware and software systems. In the last few years, tremendous progress was made in both the speed and capacity of constraint technology. Most notably, SAT solvers have become orders of magnitude faster and capable of handling problems that are orders of magnitude bigger, thus enabling the formal verification of more complex computer systems. As a result, the formal verification of hardware and software has become a promising area for research and industrial applications.

The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems.

This workshop will be of interest to researchers from both academia and industry, working on constraints or on formal verification and interested in the application of constraints to formal verification.


Scope

The scope of the workshop includes topics related to the application of constraint technology to formal verification, namely:

  • application of constraint solvers to hardware verification;
  • application of constraint solvers to software verification;
  • dedicated solvers for formal verification problems;
  • challenging formal verification problems.


Delivery

The workshop is scheduled for June 26, 2009. It will be structured to allow ample time for discussion and demonstration of new tools and new problem instances.


Submissions

Submissions should be in the LNCS style and in one of the following types:

  • a regular paper of up to 15 pages;
  • a short paper of up to 4 pages, describing an industrial experience.

Papers should be e-mailed in pdf format to the workshop chair: mvelev@gmail.com


Important Dates

The important dates for the workshop are as follows:

Abstract submission deadlineApril 15
Paper submission deadlineApril 22
Notification of acceptanceMay 10
Camera-ready version deadlineMay 31
Workshop dateJune 26


Invited Speakers

Bernd Becker, University of Freiburg, Germany
Talk title: SAT and SMT Solving in a Multi-Core Environment

Nikolaj Bjørner, Microsoft Research, U.S.A.
Talk title: SMT Solving and Applications of Bit-Level Constraints


Workshop Chairs

Miroslav Velev, Aries Design Automation, U.S.A.
Email: mvelev@gmail.com

Masahiro Fujita, University of Tokyo, Japan
Email: fujita@ee.t.u-tokyo.ac.jp


Program Committee

Jay Bhadra, Freescale, U.S.A.

Sérgio Vale Aguiar Campos, Universidade Federal de Minas Gerais, Brazil

Maciej Ciesielski, University of Massachusetts, U.S.A.

Goerschwin Fey, University of Bremen, Germany

Alex D. Groce, NASA-JPL, U.S.A.

Michael Hsiao, Virginia Tech, U.S.A.

Chung-Yang (Ric) Huang, National Taiwan University, Taiwan

John Franco, University of Cincinnati, U.S.A.

Priyank Kalla, University of Utah, U.S.A.

Shin-ichi Minato, Hokkaido University, Japan

Steve Prestwich, University College Cork, Ireland

Andreas Veneris, University of Toronto, Canada