<html 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=Windows-1252">
<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:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
@font-face
{font-family:"Helvetica Neue";
panose-1:2 0 5 3 0 0 0 2 0 4;}
@font-face
{font-family:"Helvetica Neue Light";
panose-1:2 0 4 3 0 0 0 2 0 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:21171915;
mso-list-template-ids:1964014600;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1
{mso-list-id:87164755;
mso-list-template-ids:918606946;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2
{mso-list-id:695885478;
mso-list-template-ids:-1237392222;}
@list l2:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level2
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level3
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level4
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level5
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level6
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level7
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level8
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l2:level9
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3
{mso-list-id:1389959618;
mso-list-template-ids:-916450524;}
@list l3:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level2
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level3
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level4
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level5
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level6
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level7
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level8
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level9
{mso-level-number-format:bullet;
mso-level-text:\F0B7 ;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">*******************************************************************************<o:p></o:p></p>
<p class="MsoNormal"> CALL FOR PAPERS<o:p></o:p></p>
<p class="MsoNormal"> 26th International Conference on Verification, Model Checking, and Abstract<o:p></o:p></p>
<p class="MsoNormal"> Interpretation<o:p></o:p></p>
<p class="MsoNormal"> VMCAI 2025<o:p></o:p></p>
<p class="MsoNormal"> January 20-21, 2025<o:p></o:p></p>
<p class="MsoNormal"> <a href="https://urldefense.com/v3/__https://conf.researchr.org/home/VMCAI-2025__;!!IBzWLUs!Qg1h6hzjXagfBnHEy5Rq3viBppszaoTy7Cp7Dgf8HWLTOihxcQa0h5_sVWAbBlF_JEqxju_Zq3ngs2uTphm5wfQtwagJ6KNPtZjWIMv2zU4LQw$">
https://conf.researchr.org/home/VMCAI-2025</a><o:p></o:p></p>
<p class="MsoNormal">*******************************************************************************<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">**Please note deadline extension for VMCAI 2025 below.**<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">[VMCAI 2025 Conference Website](<a href="https://urldefense.com/v3/__https://conf.researchr.org/home/VMCAI-2025__;!!IBzWLUs!Qg1h6hzjXagfBnHEy5Rq3viBppszaoTy7Cp7Dgf8HWLTOihxcQa0h5_sVWAbBlF_JEqxju_Zq3ngs2uTphm5wfQtwagJ6KNPtZjWIMv2zU4LQw$">https://conf.researchr.org/home/VMCAI-2025</a>)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">**VMCAI 2025** is the 26th International Conference on Verification, Model Checking, and Abstract Interpretation. The conference will be held during January 20-21, 2025. VMCAI provides a forum for researchers from the communities of Verification,
Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">### Scope<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The program will consist of refereed research papers as well as invited lectures and tutorials. Research contributions can report new results as well as experimental evaluations and comparisons of existing techniques.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Topics include, but are not limited to:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">- Program Verification<o:p></o:p></p>
<p class="MsoNormal">- Model Checking<o:p></o:p></p>
<p class="MsoNormal">- Abstract Interpretation<o:p></o:p></p>
<p class="MsoNormal">- Abstract Domains<o:p></o:p></p>
<p class="MsoNormal">- Program Synthesis<o:p></o:p></p>
<p class="MsoNormal">- Static Analysis<o:p></o:p></p>
<p class="MsoNormal">- Type Systems<o:p></o:p></p>
<p class="MsoNormal">- Deductive Methods<o:p></o:p></p>
<p class="MsoNormal">- Program Logics<o:p></o:p></p>
<p class="MsoNormal">- First-Order Theories<o:p></o:p></p>
<p class="MsoNormal">- Decision Procedures<o:p></o:p></p>
<p class="MsoNormal">- Interpolation<o:p></o:p></p>
<p class="MsoNormal">- Horn Clause Solving<o:p></o:p></p>
<p class="MsoNormal">- Program Certification<o:p></o:p></p>
<p class="MsoNormal">- Separation Logic<o:p></o:p></p>
<p class="MsoNormal">- Probabilistic Programming and Analysis<o:p></o:p></p>
<p class="MsoNormal">- Error Diagnosis<o:p></o:p></p>
<p class="MsoNormal">- Detection of Bugs and Security Vulnerabilities<o:p></o:p></p>
<p class="MsoNormal">- Program Transformations<o:p></o:p></p>
<p class="MsoNormal">- Hybrid and Cyber-physical Systems<o:p></o:p></p>
<p class="MsoNormal">- Concurrent and Distributed Systems<o:p></o:p></p>
<p class="MsoNormal">- Analysis of Numerical Properties<o:p></o:p></p>
<p class="MsoNormal">- Analysis of Smart Contracts<o:p></o:p></p>
<p class="MsoNormal">- Analysis of Neural Networks<o:p></o:p></p>
<p class="MsoNormal">- Case Studies on all of the above topics<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, and object-oriented programming.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">### Important Dates AoE (UTC-12)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">- **October 1, 2024 AOE**: Paper submission deadline (extended).<o:p></o:p></p>
<p class="MsoNormal">- **November 8, 2024**: Notification<o:p></o:p></p>
<p class="MsoNormal">- **November 22, 2024**: Camera-ready version due<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">### Submissions<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Submissions are required to follow Springer’s LNCS format. The page limit depends on the paper’s category (see below). In each category, additional material beyond the page limit may be placed in a clearly marked appendix, to be read at
the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website. Submission is via EasyChair. Note: submissions will open on August 26th.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">All accepted papers will be published in Springer’s Lecture Notes in Computer Science series. The corresponding author of each paper will need to complete and sign a License-to-Publish form to be submitted together with the camera-ready
version.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Submissions will undergo a single-blind review process. Submissions should not be anonymized for the purposes of review. There will be three categories of papers: regular papers, tool papers, and case studies. Papers in each category have
a different page limit and will be evaluated differently.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">**Regular papers** clearly identify and justify an advance to the field of verification, abstract interpretation, or model checking. Where applicable, they are supported by experimental validation. Regular papers are restricted to 20 pages
in LNCS format, not counting references.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">**Tool papers** present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations and emphasize the design and implementation
concerns, including software architecture and core data structures. A regular tool paper should give a clear account of the tool’s functionality, discuss the tool’s practical capabilities with reference to the type and size of problems it can handle, describe
experience with realistic case studies, and where applicable, provide a rigorous experimental evaluation. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions
of the tool, preferably substantiated by data on enhancements in terms of resources and capabilities. Authors are strongly encouraged to make their tools publicly available and submit an artifact. Tool papers are restricted to 12 pages in LNCS format, not
counting references.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">**Case studies** are expected to describe the use of verification, model checking, and abstract interpretation techniques in new application domains or industrial settings. Papers in this category do not necessarily need to present original
research results but are expected to contain novel applications of formal methods techniques as well as an evaluation of these techniques in the chosen application domain. Such papers are encouraged to discuss the unique challenges of transferring research
ideas to a real-world setting and reflect on any lessons learned from this technology transfer experience. Case study papers are restricted to 20 pages in LNCS format, not counting references. (Shorter case study papers are also welcome.)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal"><span style="font-size:10.0pt;mso-ligatures:none">-- <o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><b><span style="font-size:10.0pt;font-family:"Helvetica Neue";mso-ligatures:none">Ashutosh Trivedi<o:p></o:p></span></b></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Helvetica Neue Light";color:black;mso-ligatures:none">Associate Professor
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Helvetica Neue Light";color:black;mso-ligatures:none">Department of Computer Science<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Helvetica Neue Light";color:black;mso-ligatures:none">University of Colorado Boulder<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Helvetica Neue Light";color:black;background:white;mso-ligatures:none">Boulder, Colorado 80309<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>