This Dagstuhl Seminar aims to find new ways to represent and construct models of logical formulas, particularly large or infinite models. Models play a central role in formal reasoning. In mathematics, a model represents an object with certain properties, sometimes realizing a counterexample to a conjecture. In software verification, models typically represent an execution that reveals a bug in a program: finite (e.g. crash) or infinite (e.g. livelock). Program synthesis as a field is naturally close to model building. Models are inherently difficult to find: determining whether a sentence of first-order logic is satisfiable is undecidable, for example.

Current approaches, such as encoding model construction as Boolean satisfiability, rely on explicit representations that become rapidly intractable as the model size and state space grow. However, new opportunities are emerging from advances in mathematics, symbolic reasoning, satisfiability modulo theories (SMT), and program synthesis, which may enable the discovery of larger and more complex models.

Attendees will include researchers from automated reasoning, formal methods, and mathematics. By fostering collaboration between these communities, the seminar seeks to advance both the theoretical foundations and the practical capabilities of automated model finding. After orientation and illustrative talks covering the state of the art, knowledge exchange and problem-solving sessions begin in smaller groups. The main goal will be new methods for finding and representing large or infinite models, motivated by problems and techniques from abstract algebra. Secondary goals might include the requirements for trustworthy, checkable models; the design of certificates and languages for model representation; and the potential for cross-disciplinary tools that unify model generation, reasoning, and reuse.

If you are a mathematician: your insights into structure will be invaluable. Your favorite examples (and constructions) of finite and infinite objects and counterexamples will provide inspiration for the next generation of automated model builders. These may prove useful in your future mathematical work!

If you are a computer scientist: your intuition for programs and bugs will serve you well. Your main role here is to help invent and apply new or radically improved high-performance model-building routines, backed by new theory and inspired by techniques from other communities. Such routines will no doubt have many valuable applications in the seminar’s orbit and beyond.

Creative Commons BY 4.0

João Jorge Araújo, Mikoláš Janota, J.D. Phillips, and Michael Rawson