<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Call for Papers: CFV'06</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Fourth International Workshop on Constraints in Formal Verification (CVF'06),</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><a href="http://www.easychair.org/FLoC-06/CFV.html"><font face="Times New Roman">http://www.easychair.org/FLoC-06/CFV.html</font></a></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><span style="mso-spacerun: yes"><font face="Times New Roman"> </font></span></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Paper submission deadline: June 5</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">CFV'06 will be held on August 22, and will be part of</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">the 3rd<span style="mso-spacerun: yes"> </span>International Joint Conference on Automated Reasoning (IJCAR'06), </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"><a href="http://ijcar06.uni-koblenz.de/">http://ijcar06.uni-koblenz.de/</a></font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">a conference at the Federated Logic Conference (FLoC)</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"><a href="http://research.microsoft.com/floc06/">http://research.microsoft.com/floc06/</a></font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">in Seattle, Washington, August 2006</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Overview</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">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.
</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">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.
</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">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.
</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Scope</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">The scope of the workshop includes topics related with the application of constraint technology in formal verification, namely: </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">application of constraint solvers to hardware verification; </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">application of constraint solvers to software verification; </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">dedicated solvers for formal verification problems; </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">challenging formal verification problems. </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Delivery</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">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.
</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Submissions</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Submissions can include one of the following: </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">-A workshop paper of up to 15 pages in LNCS format. </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">-A short paper of up to 4 pages, in LNCS format, describing an industrial experience.</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Workshop Chairs</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Joao Marques-Silva, University of Southampton, UK</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Miroslav Velev, Consultant, U.S.A.</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Program Committee</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Armin Biere, Johannes Kepler University, Austria</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Louise Dennis, University of Nottingham, U.K. </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Wolfgang Kunz, Technical University of Kaiserslautern, Germany</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Ines Lynce, Technical University of Lisbon, Portugal </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Darko Marinov, University of Illinois at Urbana-Champaign, U.S.A.</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">John Moondanos, Intel, U.S.A. </font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Chao Wang, NEC Research Labs, U.S.A.</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman">Li-C. Wang, University of Santa Barbara, U.S.A.</font></p>
<p class="MsoNormal" style="MARGIN: 0in 0in 0pt"><font face="Times New Roman"> </font></p>