CEGAR 25 Special Issue
Call for Papers: Special Issue on the Theoretical Foundations and Applications of Counterexample Guided Abstraction Refinement (CEGAR)
Guest editors
Orna Grumberg, Technion, Israel (email: orna@cs.technion.ac.il)
Samarjit Chakraborty, UNC Chapel Hill, USA (email: samarjit@cs.unc.edu)
Somesh Jha, UW-Madison, USA (email: jha@cs.wisc.edu)
Submission
Please submit your manuscript to Formal Methods in System Design (FMSD) as a regular submission.
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”.
Tentative Deadlines
Papers should be submitted by February 28, 2026.
Reviews will be provided in approximately 3 months after the deadline.
Revisions will be due approximately one month after the reviews are sent.
Special Issue on CEGAR in the Formal Methods in System Design Journal
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 Formal Methods in Systems Design (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.
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
Tutorial style papers explaining certain extensions or applications of CEGAR along the lines of the various extensions listed earlier in this call for papers
Theoretical investigations of CEGAR
Applications of CEGAR to verification in various domains, such as hardware, software, cyber-physical systems and security.
Authors can submit an expanded version of previously published papers and clearly indicate the difference between the submission and the previous published papers.
CEGAR Background
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.
CEGAR authors were the recipients of the CAV award in 2015.
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.
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:
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.
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.
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.
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.