<div dir="ltr"><p class="">Call for Papers</p>

<p class="">Eighth International Workshop on Constraints in Formal
Verification</p>

<p class="">San Jose, California, U.S.A., November 21, 2013.</p>

<p class="">A workshop affiliated with the IEEE/ACM International
Conference on Computer-Aided Design, November 18 – 21, 2013</p>

<p class="">Web site: <a href="http://www.miroslav-velev.com/cfv13.html">http://www.miroslav-velev.com/cfv13.html</a></p>

<p class=""> </p>

<p class="">Abstract submission deadline:      September 30</p>

<p class="">Paper submission deadline:           October
7</p>

<p class="">Notification of acceptance:          October
15</p>

<p class="">Camera-ready version deadline:  November 5</p>

<p class="">Workshop date:                              November 21</p>

<p class=""> </p>

<p class=""> </p>

<p class="">Overview</p>

<p class="">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.</p>

<p class="">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.</p>

<p class="">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.</p>

<p class=""> </p>

<p class=""> </p>

<p class="">Scope</p>

<p class="">The scope of the workshop includes topics related to the
application of constraint technology to formal verification, namely:</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>application of constraint solvers to hardware
verification;</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>application of constraint solvers to software
verification;</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>dedicated solvers for formal verification
problems;</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>challenging formal verification problems.</p>

<p class=""> </p>

<p class="">Location</p>

<p class="">The workshop will take place in the Hilton Hotel in San
Jose, California, on November 21, 2013, right after ICCAD&#39;13. It will be
structured to allow ample time for discussion and demonstration of new tools
and new problem instances.</p>

<p class=""> </p>

<p class=""> </p>

<p class="">Submissions</p>

<p class="">Submissions should be in the IEEE style and in one of the
following types:</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>a regular paper of up to 6 pages;</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>a short paper of up to 4 pages, describing an
industrial experience.</p>

<p class="">Papers should be e-mailed in pdf format to the workshop
chair: <a href="mailto:mvelev@gmail.com">mvelev@gmail.com</a></p>

<p class=""> </p>

<p class="">Invited Speakers</p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>Thomas Ball, Microsoft, U.S.A.</p>

<p class="">              Talk
title: Efficient Modular SAT Solving for Property-Directed Reachability</p>

<p class=""> </p>

<p class="" style>-<span style="font-size:7pt;font-family:&#39;Times New Roman&#39;">       
</span>Kristin Rozier, NASA, U.S.A.</p>

<p class="">              Talk
title: Application of Constraints to Formal Verification of Software at NASA</p>

<p class=""> </p>

<p class=""> </p>

<p class="">Workshop Chair</p>

<p class="">Miroslav Velev, Aries Design Automation, U.S.A.</p>

<p class="">Email: <a href="mailto:mvelev@gmail.com">mvelev@gmail.com</a></p>

<p class=""> </p>

<p class=""> </p>

<p class="">Program Committee</p>

<p class="">Maciej Ciesielski, University of Massachusetts, U.S.A.</p>

<p class="">Masahiro Fujita, University of Tokyo, Japan</p>

<p class="">Alex D. Groce, Oregon State University, U.S.A.</p>

<p class="">Sumit Jha, University of Central Florida, U.S.A.</p>

<p class="">Susmit Jha, Intel, U.S.A.</p>

<p class="">Andreas Veneris, University of Toronto, Canada</p><p class=""><br></p></div>