Final Program

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.

Location

The workshop will take place in the Hilton Hotel in San Jose, California, on November 21, 2013, right after ICCAD'13. 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 IEEE style and in one of the following types:

• a regular paper of up to 6 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:

Invited Speakers

Thomas Ball, Microsoft, U.S.A.
Talk title: Efficient Modular SAT Solving for Property-Directed Reachability

Kristin Rozier, NASA, U.S.A.
Talk title: LTL Satisfiability Checking

Workshop Chair

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

Program Committee

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

Masahiro Fujita, University of Tokyo, Japan

Alex D. Groce, Oregon State University, U.S.A.

Sumit Jha, University of Central Florida, U.S.A.

Susmit Jha, Intel, U.S.A.

Andreas Veneris, University of Toronto, Canada