|9:00 - 10:00
||Joint Session with VERIFY’08|
Invited Talk: Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving
Alex D. Groce
|10:00 - 10:30
|10:30 - 12:30
||Joint Session with VERIFY’08
|10:30 - 11:30
||Invited Talk: Verification of Bit-Vector Arithmetic|
Priyank Kalla (University of Utah, U.S.A.)
|11:30 - 12:00
||Model Stack for the Pervasive Verification of a Microkernel-Based Operating System|
Matthias Daum, Jan Dörrenbächer, and Sebastian Bogan (Saarland University, Germany)
|12:00 - 12:30
||Modular-HED: A Canonical Decision Diagram for Modular Equivalence Verification of Polynomial Functions|
Bijan Alizadeh (Sharif University of Technology, Iran), and Masahiro Fujita (University of Tokyo, Japan)
|12:30 - 14:00
|14:00 - 15:30
||Joint Session with VERIFY’08
|14:00 - 15:00
||Invited Talk: Certificate Translation|
Gilles Barthe (IMDEA Software, Spain)
|15:00 - 15:30
||Satisfiability Modulo Bit-precise Theories for Program Exploration|
Nikolaj Bjørner, Leonardo de Moura, and Nikolai Tillmann (Microsoft, U.S.A.)
|15:30 - 16:00
|16:00 - 18:00
|16:00 - 16:30
||Polynomial Function Enclosures and Floating Point Software Verification|
Jan Andrzej Duracz and Michal Konecny (Aston University, U.K.)
|16:30 - 17:00
||Quantitative Analysis of the SAT-Controlled Redundancy Addition and Removal Technique|
Chung-Yang (Ric) Huang, and Chi-An Wu (National Taiwan University, Taiwan)
|17:00 - 17:30
||Adding Unsafe Constraints to Improve SAT Solver Performance|
John Franco (University of Cincinnati, U.S.A.), and Sean Weaver (U.S. Department of Defense, U.S.A.)
|17:30 - 18:00
||Large Scale Genetic Identity Inference Using Symbolic Model Checking|
Rodrigo Gomes (Universidade Federal de Minas Gerais, Brasil),
Carolina Cota (Pontificia Universidade Catolica de Minas Gerais, Brasil),
Mark Song (Pontificia Universidade Catolica de Minas Gerais, Brasil), and
Sergio Campos (Universidade Federal de Minas Gerais, Brasil)
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.
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.
The workshop is scheduled for August 11, 2008. It will be structured
to allow ample time for discussion and demonstration of new tools and new problem instances.
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:
The important dates for the workshop are as follows:
|Abstract submission deadline||May 15|
|Paper submission deadline||May 22|
|Notification of acceptance||June 10|
|Camera-ready version deadline||June 30|
|Workshop Date||August 11|
The authors of selected papers will be invited to submit extended versions for
publication in a special issue of Annals of Mathematics and Artificial Intelligence,
to be edited by Miroslav Velev and John Franco.
Talk title: Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving
Priyank Kalla, University of Utah, U.S.A.
Talk title: Verification of Bit-Vector Arithmetic
Miroslav Velev, U.S.A.
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.
Michael Hsiao, Virginia Tech, U.S.A.
Chung-Yang (Ric) Huang, National Taiwan University, Taiwan
John Franco, University of Cincinnati, U.S.A.
Masahiro Fujita, University of Tokyo, Japan
Oliver Kullmann, Swansea University, U.K.
Wolfgang Kunz, Technical University of Kaiserslautern, Germany
Gihwon Kwon, Kyonggi University, Korea
Prabhat Mishra, University of Florida, U.S.A.
Steve Prestwich, University College Cork, Ireland
Andreas Veneris, University of Toronto, Canada
Toby Walsh, NICTA and University of New South Wales, Australia