[Om-announce] Call for papers: Constraints in Formal Verification 2007 (CFV'07) Bremen, Germany, July 16, 2007

[Chao Wang]

Call for Papers

CFV'07:  Fourth International Workshop on Constraints in Formal
Verification

Bremen, Germany, July 16, 2007

A satellite event of the 21st Conference on Automated Deduction
(CADE-21)

CFV'07  web site: http://www.miroslav-velev.com/cfv07.html


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 at gmail.com


Important Dates
------------------------
The important dates for the workshop are as follows:
- paper submission deadline:  May 15
- notification of acceptance:  May 31
- camera-ready version deadline:  June 15
- workshop Date:  July 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 at 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.