Third International Workshop on

Constraints in Formal Verification

Held in conjunction with

20th International Conference on Automated Deduction

[ Overview ]

[ Scope ]

[ Delivery ]

[ Submissions ]

[ Important Dates ]

[ Invited Speakers ]

[ Schedule ]

[ Organization ]

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 academia and industry, working in constraints or in formal verification and interested in the application of constraints in formal verification.

[ Back to top ]

Scope

The scope of the workshop includes topics related with the application of constraint technology in 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.

[ Back to top ]

Delivery

The workshop will be scheduled for one full day. We expect to structure the workshop to allow ample time for discussion and demonstration of new tools and new problem instances.

All workshop attendees must pay the CADE workshop registration fee.

[ Back to top ]

Submissions

Submissions can include one of the following:

• A workshop paper of up to 15 pages in LNCS format.
• A short paper of up to 4 pages, in LNCS format, 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.

Please send your submissions by email to cfv05-sub@sat.inesc-id.pt using the subject line "CADE05 CFV Workshop Submission".

The proceedings of CFV workshop are expected to be published as a volume of ENTCS, together with the proceedings of the other CADE'05 workshops.

Authors of selected papers will be invited to submit extended versions of their papers for review for a special issue of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT). The special issue is scheduled for January 2006, and will have a submission deadline in September 2005.

[ Back to top ]

Important Dates

The proposed schedule of important dates for the workshop is as follows:

[ Back to top ]

Invited Speakers

Masahiro Fujita
University of Tokyo, Japan

Fabio Somenzi
University of Colorado, U.S.A.

Tentative Workshop Schedule

[ Back to top ]

Workshop Chairs

Joao Marques-Silva
Technical University of Lisbon, IST/INESC-ID
Email: jpms@inesc-id.pt

Miroslav Velev
Reservoir Labs, U.S.A.
Email: mvelev@ece.cmu.edu

[ Back to top ]

Program Committee

Magdy Abadir, Freescale Semiconductor Inc., U.S.A.

Enrico Giunchiglia, Univ. Genova, Italy

Aarti Gupta, NEC Research Labs, U.S.A.

Ziyad Hanna, Intel, U.S.A.

Yakov Novikov, Infenion, Germany

Andreas Podelski, Max-Planck-Institut für Informatik, Germany

Mukul Prasad, Fujitsu Labs of America, U.S.A.

Stefano Quer, Politecnico di Torino, Italy

Toby Walsh, University of New South Wales, Australia

[ Back to top ]