<DIV id=yiv1050228779> <DIV id=mb_0> <DIV style="DIRECTION: ltr"><SPAN><FONT style="BACKGROUND-COLOR: #ffff88">Call</FONT></SPAN> for Papers<BR><SPAN><FONT style="BACKGROUND-COLOR: #ffff88">CFV</FONT></SPAN>'<SPAN><FONT style="BACKGROUND-COLOR: #ffff88">07</FONT></SPAN>: Fourth International Workshop on Constraints in Formal Verification<BR><SPAN id=lw_1178616390_0 style="BACKGROUND: none transparent scroll repeat 0% 0%; CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Bremen, Germany</SPAN>, July 16, 2007<BR>A satellite event of the 21st Conference on Automated Deduction (CADE-21)<BR><SPAN><FONT style="BACKGROUND-COLOR: #ffff88">CFV</FONT></SPAN>'<SPAN><FONT style="BACKGROUND-COLOR: #ffff88">07</FONT></SPAN> web site: <A href="http://www.miroslav-velev.com/cfv07.html" target=_blank rel=nofollow><SPAN id=lw_1178616390_1 style="BACKGROUND: none transparent scroll repeat 0% 0%"><FONT
color=#003399>http://www.miroslav-velev.com/cfv07.html</FONT></SPAN></A></DIV> <DIV style="DIRECTION: ltr"><BR> </DIV> <DIV style="DIRECTION: ltr">Submission deadline: May 15, 2007<BR><BR>Overview<BR>------------------------<BR>Formal verification is of crucial significance in the development of<BR>hardware and software systems. In the last few years, tremendous<BR>progress was made in both the speed and capacity of constraint<BR>technology. Most notably, SAT solvers have become orders of magnitude<BR>faster and capable of handling problems that are orders of magnitude<BR>bigger, thus enabling the formal verification of more complex computer<BR>systems. As a result, the formal verification of hardware and software<BR>has become a promising area for research and industrial applications.<BR>The main goals of the Constraints in Formal Verification workshop are<BR>to bring together researchers from the CSP/SAT and the formal<BR>verification communities, to describe new
applications of constraint<BR>technology to formal verification, to disseminate new challenging<BR>problem instances, and to propose new dedicated algorithms for hard<BR>formal verification problems.<BR>This workshop will be of interest to researchers from both academia<BR>and industry, working on constraints or on formal verification and<BR>interested in the application of constraints to formal verification.<BR><BR><BR>Scope<BR>------------------------<BR>The scope of the workshop includes topics related to the application<BR>of constraint technology to formal verification, namely:<BR>- application of constraint solvers to hardware verification;<BR>- application of constraint solvers to software verification;<BR>- dedicated solvers for formal verification problems;<BR>- challenging formal verification problems.<BR><BR><BR>Delivery<BR>------------------------<BR>The workshop is scheduled for a full day on July 16, 2007. It will be<BR>structured to allow ample time for
discussion and demonstration of new<BR>tools and new problem instances.<BR><BR><BR>Submissions<BR>------------------------<BR>Submissions should be in the LNCS format and in one of the following types:<BR>- a regular paper of up to 15 pages;<BR>- a short paper of up to 4 pages, describing an industrial experience.<BR>Workshop papers should be submitted electronically in pdf format.<BR>Papers should be formatted using the Lecture Notes in Computer Science<BR>(LNCS) style.<BR>Paper submissions should be e-mailed to the workshop chair at: <A href="http://us.f324.mail.yahoo.com/ym/Compose?To=mvelev@gmail.com" target=_blank rel=nofollow><SPAN id=lw_1178616390_2><FONT color=#003399>mvelev@gmail.com</FONT></SPAN></A><BR><BR><BR>Important Dates<BR>------------------------<BR>The important dates for the workshop are as follows:<BR>- paper submission deadline: May 15<BR>- notification of acceptance: May 31<BR>- camera-ready version deadline: June 15<BR>- workshop
Date: July 16<BR><BR><BR>Invited Speakers<BR>------------------------<BR>Alessandro Cimatti, ITC-IRST, <SPAN id=lw_1178616390_3 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Italy</SPAN><BR>Talk title: Satisfiability Modulo the Theory of Bit Vectors<BR><BR>Ulfar Erlingsson, Microsoft Research, <SPAN id=lw_1178616390_4 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Silicon Valley</SPAN>, U.S.A.<BR>Talk title: Verifiable Enforcement of Control-Flow-Based Security Policies<BR><BR><BR>Workshop Chair<BR>------------------------<BR>Miroslav Velev, Consultant, U.S.A.<BR>Email: <A href="http://us.f324.mail.yahoo.com/ym/Compose?To=mvelev@gmail.com" target=_blank rel=nofollow><SPAN id=lw_1178616390_5><FONT color=#003399>mvelev@gmail.com</FONT></SPAN></A><BR><BR><BR>Program Committee<BR>------------------------<BR>Armin Biere, Johannes Kepler University, <SPAN id=lw_1178616390_6 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed;
HEIGHT: 1em">Austria</SPAN><BR>Roderick Bloem, Graz University of Technology, <SPAN id=lw_1178616390_7 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Austria</SPAN><BR>Louise Dennis, University of Liverpool, U.K.<BR>Masahiro Fujita, University of <SPAN id=lw_1178616390_8 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Tokyo, Japan</SPAN><BR>Priyank Kalla, <SPAN id=lw_1178616390_9 style="BACKGROUND: none transparent scroll repeat 0% 0%; CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">University of Utah</SPAN>, U.S.A.<BR>Oliver Kullmann, Swansea University, U.K.<BR>Wolfgang Kunz, Technical University of <SPAN id=lw_1178616390_10 style="CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Kaiserslautern, Germany</SPAN><BR>Marius Minea, "Politehnica" University of <SPAN id=lw_1178616390_11 style="BACKGROUND: none transparent scroll repeat 0% 0%; CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT:
1em">Timisoara, Romania</SPAN><BR>John Moondanos, <SPAN id=lw_1178616390_12 style="BACKGROUND: none transparent scroll repeat 0% 0%; CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Intel</SPAN>, U.S.A.<BR>Andreas Veneris, University of <SPAN id=lw_1178616390_13 style="BACKGROUND: none transparent scroll repeat 0% 0%; CURSOR: hand; BORDER-BOTTOM: #0066cc 1px dashed; HEIGHT: 1em">Toronto, Canada</SPAN><BR>Chao Wang, NEC Research Labs, U.S.A.<BR>Li-C. Wang, University of Santa Barbara, U.S.A.<BR></DIV></DIV></DIV> <FORM name=showLetter2 action=/ym/ShowLetter?Idx=0&Search=&YY=52998&y5beta=yes&y5beta=yes&order=down&sort=date&pos=0&view=a&head=b method=post> </FORM>