Automated reasoning concerns itself with the development of logical methods for analysis and verification, mainly of software. These include methods based on satisfiability checking (SAT), but also constraint programming, abstract interpretation, and model learning.

In the Automata and Applications group, we focus on a range of logical and formal methods to analyze, verify, and better understand complex systems. The team's work spans:

• Bounded Model Checking (BMC): using SAT solvers to encode verification problems as Boolean formulas, allowing direct evaluation of temporal logic specifications. This approach can be more efficient than converting the system into automata and provides a compact symbolic representation for systems derived from higher-level models. While BMC focuses on traces of bounded length and is therefore not complete, it can still produce high-quality counterexamples in practice. The team also studies optimizations to exploit the structure of BMC problems and improve solver efficiency [1,2].

• Model Learning: synthesizing formulas or automata from observed system behaviors or traces. This includes problems of explainability, where a temporal formula is synthesized to distinguish between two given samples. Both passive SAT-based learning and active learning approaches, as well as hybrid methods using imperfect oracles, are investigated to handle cases where ideal oracles are unavailable [3].

• Abstract Interpretation and Constraint Programming: analyzing program properties through symbolic representations and constraints, complementing SAT-based verification and model learning. This allows reasoning about complex behaviors without exploring all possible traces explicitly.

The team also contributes on optimizing SAT solvers, exploring general enhancements such as exploiting symmetries in logical formulas and using dedicated programming interfaces to dynamically introduce new clauses. These improvements have been incorporated into tools like Painless [4].

Related Publications