<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:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:12.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:655576516;
mso-list-template-ids:913595280;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:1377654902;
mso-list-template-ids:-468412598;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style>
</head>
<body lang="en-IL" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Dear List moderator,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">We will be grateful if you can distribute the Call for Papers below, concerning a special issue of the journal FMSD, dedicated to 25 years of CEGAR.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">We believe that it is relevant to a great part of your audience.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">Many thanks and</span><span lang="en-IL"> best regards,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Orna, Samarjit and Somesh<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">-----------------------------------------------------------------------------------------------------------------<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><a href="https://sites.google.com/wisc.edu/cegar25/home"><span style="color:#467886">CEGAR25</span></a><o:p></o:p></span></p>
<p class="MsoNormal"><b><span lang="en-IL">Call for Papers: Special Issue on the Theoretical Foundations and Applications of Counterexample Guided Abstraction Refinement (CEGAR)</span></b><span lang="en-IL"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><b><span lang="en-IL">Guest editors</span></b><span lang="en-IL"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Orna Grumberg, Technion, Israel (email: <a href="mailto:orna@cs.technion.ac.il" target="_blank"><span style="color:#467886">orna@cs.technion.ac.il</span></a>)<br>
Samarjit Chakraborty, UNC Chapel Hill, USA (email: <a href="mailto:samarjit@cs.unc.edu" target="_blank"><span style="color:#467886">samarjit@cs.unc.edu</span></a>)<br>
Somesh Jha, UW-Madison, USA (email: <a href="mailto:jha@cs.wisc.edu" target="_blank"><span style="color:#467886">jha@cs.wisc.edu</span></a>)<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><br>
<b>Submission</b><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Please submit your manuscript to Formal Methods in System Design (FMSD) as a regular submission.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Once you enter the details of the manuscript, you will have the option of choosing a collection. There, choose “Special issue on 25 years of CEGAR”.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><b><span lang="en-IL">Tentative Deadlines</span></b><span lang="en-IL"><o:p></o:p></span></p>
<ul style="margin-top:0cm" type="square">
<li class="MsoNormal" style="mso-list:l0 level1 lfo1"><span lang="en-IL">Papers should be submitted by <i><span style="color:red">February 28, 2026</span></i>.<o:p></o:p></span></li><li class="MsoNormal" style="mso-list:l0 level1 lfo1"><span lang="en-IL">Reviews will be provided in approximately 3 months after the deadline.<o:p></o:p></span></li><li class="MsoNormal" style="mso-list:l0 level1 lfo1"><span lang="en-IL">Revisions will be due approximately one month after the reviews are sent.<o:p></o:p></span></li></ul>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><b><span lang="en-IL">Special Issue on CEGAR in the Formal Methods in System Design Journal</span></b><span lang="en-IL"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Several examples described a short glimpse of the many extensions and applications of CEGAR. More importantly, it illustrates how the research community is still broadening its applicability and theoretical depth. Hence,
to recognize the 25th year of CEGAR, and provide a good overview of the current state of the CEGAR approach and its many applications, we solicit papers for a special issue on the theoretical foundations and applications of CEGAR in the <b>Formal Methods in
Systems Design</b> (FMSD) journal. Some of the topics of interest are listed below, but all submissions that extend, investigate, or apply the CEGAR paradigm in different application domains are welcome.<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span lang="en-IL"><o:p> </o:p></span></p>
<ul style="margin-top:0cm" type="square">
<li class="MsoNormal" style="mso-list:l1 level1 lfo2"><span lang="en-IL">Retrospective papers that expand on previously published papers on the topic of CEGAR, in particular, on how the results from those papers have been extended<o:p></o:p></span></li><li class="MsoNormal" style="mso-list:l1 level1 lfo2"><span lang="en-IL">Tutorial style papers explaining certain extensions or applications of CEGAR along the lines of the various extensions listed earlier in this call for papers<o:p></o:p></span></li><li class="MsoNormal" style="mso-list:l1 level1 lfo2"><span lang="en-IL">Theoretical investigations of CEGAR<o:p></o:p></span></li><li class="MsoNormal" style="mso-list:l1 level1 lfo2"><span lang="en-IL">Applications of CEGAR to verification in various domains, such as hardware, software, cyber-physical systems and security.<o:p></o:p></span></li></ul>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><i><span lang="en-IL">Authors can submit an expanded version of previously published papers and clearly indicate the difference between the submission and the previous published papers.</span></i><span lang="en-IL"><o:p></o:p></span></p>
<p class="MsoNormal"><b><span lang="en-IL"><o:p> </o:p></span></b></p>
<p class="MsoNormal"><b><span lang="en-IL">CEGAR Background</span></b><span lang="en-IL"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Counterexample Guided Abstraction Refinement (CEGAR) has been a powerful paradigm in formal verification. The basic step in CEGAR is to refine the abstraction used in formal verification based on spurious counterexamples–counterexamples
that are an artifact of the coarseness of the abstraction and do not correspond to “real” counterexamples. The initial paper on CEGAR was published in CAV 2000, and thus celebrates 25 this year. An extended version of the paper was published in the Journal
of the ACM in 2003.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">CEGAR authors were the recipients of the CAV award in 2015.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">One of the most well-known uses of CEGAR has been in the cotnext of predicate abstraction and symbolic refinement. Here, instead of concrete state systems, predicate-abstracted Boolean programs were used and refinement
became symbolic, guided by interpolants or unsatisfiable cores extracted from SMT solvers, thereby automating abstraction over infinite-state systems, with applications in software verification. Examples of this approach include SLAM, BLAST, and predicate
discovery using SMT solvers. <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">However, since its publication in 2000, CEGAR has proven to be an extremely rich concept and numerous research efforts have extended the basic idea and applied it to many additional domains, including the following:<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Verification of infinite-state and hybrid systems - work here generalized CEGAR beyond discrete systems to systems with continuous dynamics or unbounded data. Here, refinement involves refining numerical abstractions
(e.g., tightening convex regions) or hybrid automata partitions based on spurious counterexamples. Examples of this include numerical abstractions using polyhedra, hybrid CEGAR, and using symbolic transition systems with acceleration. <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Compositional and modular CEGAR - an immensely successful use of CEGAR, in which instead of analyzing the full system monolithically, refinement is performed locally within modules or components, and counterexamples guide
local abstractions and assumptions. This makes CEGAR scalable to large concurrent and distributed systems. Examples of this approach include assume-guarantee reasoning and interface abstraction refinement.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Probabilistic and Quantitative CEGAR - in this domain counterexamples can be probabilistic traces and refinement adjusts probabilistic abstractions to improve precision. Examples of this approach are CEGAR for Markov
Decision Processes, and abstraction refinement for stochastic games. <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL">Learning and data-driven CEGAR - taking this approach learning methods are integrated into CEGAR loops to automate abstraction choices or counterexample classification. Examples of this approach include machine learning-aided
predicate selection and CEGAR with reinforcement learning refinement policies. <o:p></o:p></span></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"> <o:p></o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="en-IL"><o:p> </o:p></span></p>
</div>
</body>
</html>