CFV'07 Fourth Workshop on Constraints in Formal Verification
Bremen, Germany, July 16, 2007
a satellite event of CADE-21



Program

9:00 - 11:00Special Invited Talks Session on Satisfiability Modulo Theories (joint with the DISPROVING'07 and VERIFY'07 Workshops)
9:00 - 10:00 Invited Talk: Trends and Challenges in Satisfiability Modulo Theories
Cesare Tinelli (University of Iowa, U.S.A.)
10:00 - 11:00 Invited Talk: Satisfiability Modulo the Theory of Bit Vectors
Alessandro Cimatti (ITC-IRST, Italy)
11:00 - 11:20 Break
11:20 - 12:50Session on Advances in Decision Procedures
11:20 - 11:50LTED: A Canonical and Compact Hybrid Word-Boolean Representation as a Formal Model for Hardware/Software Co-Designs
Bijan Alizadeh, and Masahiro Fujita (VLSI Design and Education Center, University of Tokyo, Japan)
11:50 - 12:20Efficient CNF Encoding for Selecting 1 from N Objects
Gihwon Kwon (Kyonggi University, Korea), and Will Klieber (Carnegie Mellon University, U.S.A.)
12:20 - 12:50Using Bit Vector Decision Procedures for Analysis of Protein Folding Pathways
Christopher J. Langmead, and Sumit K. Jha (Carnegie Mellon University, U.S.A.)
12:50 - 14:00 Lunch (Provided)
14:00 - 15:00 Invited Talk: Enforcement of Control-Flow-Based Security Policies
Ulfar Erlingsson (Microsoft Research, Silicon Valley, U.S.A.)
15:00 - 15:10 Break
15:10 - 16:10Session on Application of Constraints to Property Checking
15:10 - 15:40On Bridging Simulation and Formal Verification
Eugene Goldberg (Cadence Berkeley Labs, U.S.A.)
15:40 - 16:10Formal Robustness Checking
Görschwin Fey, and Rolf Drechsler (University of Bremen, Germany)

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 a full day on July 16, 2007. 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 format 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.

Workshop papers should be submitted electronically in pdf format. Papers should be formatted using the Lecture Notes in Computer Science (LNCS) style.

Paper submissions should be e-mailed to the workshop chair at: mvelev@gmail.com


Important Dates

The important dates for the workshop are as follows:

Paper submission deadlineMay 15
Notification of acceptanceMay 31
Camera-ready version deadlineJune 15
Workshop DateJuly 16

Invited Speakers

Alessandro Cimatti, ITC-IRST, Italy
Talk title: Satisfiability Modulo the Theory of Bit Vectors

Ulfar Erlingsson, Microsoft Research, Silicon Valley, U.S.A.
Talk title: Verifiable Enforcement of Control-Flow-Based Security Policies


Workshop Chair

Miroslav Velev, Consultant, U.S.A.
Email: mvelev@gmail.com


Program Committee

Armin Biere, Johannes Kepler University, Austria

Roderick Bloem, Graz University of Technology, Austria

Louise Dennis, University of Liverpool, U.K.

Masahiro Fujita, University of Tokyo, Japan

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

Oliver Kullmann, Swansea University, U.K.

Wolfgang Kunz, Technical University of Kaiserslautern, Germany

Marius Minea, "Politehnica" University of Timisoara, Romania

John Moondanos, Intel, U.S.A.

Andreas Veneris, University of Toronto, Canada

Chao Wang, NEC Research Labs, U.S.A.

Li-C. Wang, University of Santa Barbara, U.S.A.