<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"> SMT 2021 Call for Participation<o:p></o:p></p>
<p class="MsoNormal"> 19th International Workshop on Satisfiability Modulo Theories (SMT 2021)<o:p></o:p></p>
<p class="MsoNormal"> July 18-19, 2021, Online<o:p></o:p></p>
<p class="MsoNormal"> 8am -- 12:45pm PDT<o:p></o:p></p>
<p class="MsoNormal"> Affiliated with CAV 2021<o:p></o:p></p>
<p class="MsoNormal"> <a href="http://smt-workshop.cs.uiowa.edu/2021/index.shtml">http://smt-workshop.cs.uiowa.edu/2021/index.shtml</a> <o:p></o:p></p>
<p class="MsoNormal"> Registration: <a href="https://regmaster.com/2021conf/CAV21/register.php">
https://regmaster.com/2021conf/CAV21/register.php</a><o:p></o:p></p>
<p class="MsoNormal"><span lang="EN-US"> </span>Early Registration till July 9: 75$/10$ (students); Regular Registration: 125$/15$ (students)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">================================================================================================================================================<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">We are pleased to invite you to participate in the SMT 2021 workshop.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Determining the satisfiability of first-order formulas modulo background theories, known as Satisfiability Modulo Theories (SMT), has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization,
scheduling, and other areas. The aim of the annual SMT workshop is to bring together researchers and users of SMT tools and techniques.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">This year, we have an exciting and versatile program, which includes the following sessions:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Sunday, July 18<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">1. <span lang="EN-US"> </span>Invited Talk by Guy Katz (Hebrew University): Using SMT and Abstraction-Refinement for Neural Network Verification
<o:p></o:p></p>
<p class="MsoNormal">2. Theory of SMT<o:p></o:p></p>
<p class="MsoNormal">3. Proofs and Interpolation<o:p></o:p></p>
<p class="MsoNormal">4. Boosting SMT Solving<o:p></o:p></p>
<p class="MsoNormal">5. SMT Competition 2021: Report<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Monday, July 19<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">1. <span lang="EN-US"> </span>Invited Talk by Karem Sakallah (University of Michigan): AVR: Word-Level Verification by Equality Abstraction of Data State<o:p></o:p></p>
<p class="MsoNormal">2. SMT Applications<o:p></o:p></p>
<p class="MsoNormal">3. SMT-LIB and API (Technical Session)<o:p></o:p></p>
<p class="MsoNormal">4. SMT-LIB and Business Meeting<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Program details appear at <a href="http://smt-workshop.cs.uiowa.edu/2021/program.shtml">
http://smt-workshop.cs.uiowa.edu/2021/program.shtml</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Talks will be live and will include Q&A. <o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Program Chairs:<o:p></o:p></p>
<p class="MsoNormal">- Aina Niemetz (Stanford University)<o:p></o:p></p>
<p class="MsoNormal">- Alexander Nadel (Intel)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p>---------------------------------------------------------------------<br>
Intel Israel (74) Limited</p>
<p>This e-mail and any attachments may contain confidential material for<br>
the sole use of the intended recipient(s). Any review or distribution<br>
by others is strictly prohibited. If you are not the intended<br>
recipient, please contact the sender and delete all copies.</p></body>
</html>