publications

2026

1. Liveness Proofs for Hardware Model Checking

   Nils Froleyks, Emily Yu, Bart Bogaerts, and 2 more authors

   In Computer Aided Verification - 38th International Conference, CAV 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I, 2026

   BIB PDF Abs

   We introduce a generic certificate format for verifying liveness properties in hardware model checking. The format relies purely on propositional predicates and does not involve explicit counters. Our certificates can be efficiently validated using a fixed number of SAT checks. The proposed format is compatible with state-of-the-art liveness checking algorithms. We present certificate generation for several representative techniques, including rLive, liveness-to-safety reduction, and k-liveness, as well as for a preprocessing method based on stabilizing constraint extraction. Experimental results on benchmarks from the Hardware Model Checking Competition demonstrate that our approach is practically effective with very low certification overhead, and our certificate checker successfully validated all generated certificates.

2. CaDiCaL 3.0: Proofs, Algorithms, Implied Literals, and Robust Scheduling

   Florian Pollitt, Mathias Fleury, Katalin Fazekas, and 2 more authors

   To appear

   In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026), 2026

   BIB
3. Hardware Model Checking Certification with Certifaiger and Cerbtora

   Nils Froleyks and Emily Yu

   In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR) 2026, Part of FLoC 2026, Lisbon, Portugal, July 26–29, 2026, 2026

   BIB PDF Abs

   Certificates are machine-checkable witnesses that help increase confidence in verification results by providing independently verifiable evidence beyond a simple yes/no answer. In this short paper, we present two certificate checkers for hardware model checking, Certifaiger and Cerbtora, which target bit-level and word-level verification of hardware designs, respectively. Certifaiger has been adopted in recent editions of the Hardware Model Checking Competition, but not described in the literature before. Cerbtora extends the same theoretical framework to the word level, in which certificates are expressed in the same modeling language as the design under test and are validated using efficient automated reasoning engines. We describe the architecture and main components of both tools and evaluate them on competition benchmarks.

4. Certifying Constraints in Hardware Model Checking

   Nils Froleyks, Emily Yu, Armin Biere, and 1 more author

   In Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18–22, 2026, Proceedings, 2026

   BIB PDF Abs

   Model checking is a powerful automated reasoning technique for verifying hardware designs, ensuring that they function correctly before deployment. However, modern model checkers are complex software systems with hundreds of thousands of lines of code, making them prone to errors. To increase confidence in verification results, recent efforts in hardware verification focus on requiring model checkers to produce machine-checkable proofs according to a standardized format that can be independently validated. Yet, implementing proof generation across different verification algorithms presents a unique challenge. In hardware model checking, constraints play an essential role, as they encode assumptions about the environment and help simplify analysis. This paper addresses the challenge by developing a certification approach that ensures verification results remain trustworthy when constraints are present. We introduce certificate generation methods for three classes of constraints that can be extracted from the models. Furthermore, to support a broader range of constraints and more complex reset logic for industrial use, we also provide alternative Quantified Boolean Formula checks in the proof format with a single quantifier alternation. Lastly, we present a certificate generation method for k-induction with uniqueness constraints, an important model checking technique. We implement these in a certification toolkit, and provide empirical evaluation on competition benchmarks, demonstrating their effectiveness.

2025

1. Deep Integration of SAT Solving and Model Checking

   Nils Froleyks

   PhD Thesis

   Johannes Kepler Universität Linz, 2025

   BIB PDF Abs

   Once just considered the archetypal intractable problem, Boolean satisfiability (SAT) has flourished into one of the most effective tools for automated reasoning. One of its most successful applications is model checking, where SAT solvers are used to verify the correctness of systems by checking whether certain properties hold. This thesis investigates how to deepen the integration between SAT solving and model checking to improve performance and increase trust in the results. We begin by presenting the state-of-the-art incremental SAT solver CaDiCaL 2.0. We extend its assumption-based interface with clause assumptions, and demonstrate how this enhancement accelerates IC3-based model checking. Building on CaDiCaL, we introduce a new backbone extraction tool, CadiBack. A formula’s backbone—the set of literals true in every satisfying assignment—can benefit various SAT-based applications, including verification, state space approximation, and fault localization. As part of this work, we present a polynomial-time backbone extraction algorithm and evaluate it as a preprocessor for CadiBack. Additionally, we formalize ternary simulation through the lens of abstract interpretation and propose a technique to improve accuracy using backbone extraction. We then address how to achieve a similar level of trust in model checking as is commonly vested in SAT solvers. To this end, we develop a certification approach for hardware model checking. Specifically, we present certificate constructions for the preprocessing techniques of phase abstraction and constraint extraction. Our efforts culminate in the Hardware Model Checking Competition 2024, which marks the introduction of mandatory certificates for all participating tools. The results convincingly show the practical efficiency and effectiveness of our approach. Finally, this thesis further explores competitions as a scientific method for advancing solver technology. Drawing on the author’s experience co-organizing several SAT and hardware model checking competitions, we examine what insights into solver innovation can be gained from these events.

2. Introducing Certificates to the Hardware Model Checking Competition

   Nils Froleyks, Emily Yu, Mathias Preiner, and 2 more authors

   In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, 2025

   BIB PDF Abs DOI

   Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.

3. Challenging Certificates from Model Checking

   Nils Froleyks, Emily Yu, and Armin Biere

   SAT Competition Benchmark Description

   2025

   BIB

2024

1. CaDiCaL 2.0

   Armin Biere, Tobias Faller, Katalin Fazekas, and 3 more authors

   In CAV, 2024

   BIB PDF Abs

   The SAT solver CaDiCaL provides a rich feature set with a clean library interface. It has been adopted by many users, is well documented and easy to extend due to its effective testing and debugging infrastructure. In this tool paper we give a high-level introduction into the solver architecture and then go briefly over implemented techniques. We describe basic features and novel advanced usage scenarios. Experiments confirm that CaDiCaL despite this flexibility has state-of-the-art performance both in a stand-alone as well as incremental setting.

2. Certifying Phase Abstraction

   Nils Froleyks, Emily Yu, Armin Biere, and 1 more author

   In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, 2024

   BIB PDF Abs DOI

   Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.

3. Clausal Equivalence Sweeping

   Armin Biere, Katalin Fazekas, Mathias Fleury, and 1 more author

   In Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, 2024

   BIB PDF Abs DOI

   The state-of-the-art to combinational equivalence checking is based on SAT sweeping. It recursively establishes equivalence of internal nodes of two circuits to prove equivalence of their outputs. The approach follows the topological order from inputs to outputs and makes use of simulation to refine the set of potentially equivalent nodes to reduce the number of SAT solver queries. This non-uniform hybrid reasoning, using both the circuit structure and a clausal encoding, is complex to orchestrate. In earlier work, clausal encoding was avoided using a dedicated circuit-aware SAT solver. Instead, we propose to perform SAT sweeping directly on the clausal encoding of the complete equivalence checking problem within the SAT solver, but again relying on a second, dedicated, internal SAT solver. Both SAT solvers work on a clausal representation. This allows to transparently make use of all the advanced reasoning capabilities of the SAT solver, particularly pre- and inprocessing techniques.

4. Clausal Congruence Closure

   Armin Biere, Katalin Fazekas, Mathias Fleury, and 1 more author

   In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, Pune, India, 2024

   BIB PDF Abs DOI

   Many practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance.

5. Ternary Simulation as Abstract Interpretation

   Nils Froleyks, Emily Yu, and Armin Biere

   In MBMV 2024; 27. Workshop, 2024

   BIB PDF Abs

   We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.

6. Hardware Model Checking Competition 2024

   Armin Biere, Nils Froleyks, and Mathias Preiner

   In Proceedings 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD’24), 2024

   BIB DOI
7. Hardware Equivalence Checking Problems

   Armin Biere, Tobias Faller, Katalin Fazekas, and 3 more authors

   SAT Competition Benchmark Description

   2024

   BIB
8. CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024

   Armin Biere, Tobias Faller, Katalin Fazekas, and 3 more authors

   In Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, 2024

   BIB PDF Abs

   In this short system description we describe our three sequential SAT solvers CaDiCaL, IsaSAT and Kissat submitted to the main track of the SAT competition 2024 as well as an update to Gimsatul submitted to the parallel track.

2023

1. BIG Backbones

   Nils Froleyks, Emily Yu, and Armin Biere

   In Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023

   BIB PDF DOI
2. Towards Compositional Hardware Model Checking Certification

   Emily Yu, Nils Froleyks, Armin Biere, and 1 more author

   In Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023

   BIB PDF Abs DOI

   In this paper, we revisit and formalize temporal decomposition, as one of the most basic, widely-used and effective preprocessing techniques in hardware model checking. The main contribution is a certification framework for hardware model checking using temporal decomposition. Our approach enables generation of a single inductive invariant in a compositional way using inductive invariant certificates provided by existing certifying model checkers on the result of preprocessing a model through temporal decomposition. We implement and evaluate the method on hardware model checking competition benchmarks. The experiments confirm the effectiveness of temporal decomposition. The proposed certification approach makes it feasible to generate a generic proof for model checking and preprocessing.

3. The SAT Museum

   Armin Biere, Mathias Fleury, Nils Froleyks, and 1 more author

   In Proceedings of the 14th International Workshop on Pragmatics of SAT Co-Located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italy, July 4, 2023

   BIB PDF Abs

   The virtual SAT Solver Museum is an effort towards preserving historical SAT solvers, by collecting and porting their source code to modern compilers and evaluating them on representative benchmark sets on the same hardware. This allows us to compare historic and modern solvers in the same environment. Our results clearly show a remarkable improvement of SAT solver performance in the last 30 years.

4. CadiBack: Extracting Backbones with CaDiCaL

   Armin Biere, Nils Froleyks, and Wenxi Wang

   In SAT, 2023

   BIB PDF Abs

   The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.

2022

1. Stratified Certification for K-Induction

   Emily Yu, Nils Froleyks, Armin Biere, and 1 more author

   In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022

   BIB PDF Abs DOI

   Our recently proposed certification framework for bit-level k-induction-based model checking has been shown to be quite effective in increasing the trust of verification results even though it partially involved quantifier reasoning. In this paper we show how to simplify the approach by assuming reset functions to be stratified. This way it can be lifted to word-level and in principle to other theories where quantifier reasoning is difficult. Our new method requires six simple SAT checks and one polynomial-time check, allowing certification to remain in co-NP while the previous approach required five SAT checks and one QBF check. Experimental results show a substantial performance gain for our new approach. Finally, we present and evaluate our new tool Certifaiger-wl which is able to certify k-induction-based word-level model checking.

2. Unique Reconfiguration Sequence

   Nils Froleyks, Emily Yu, and Armin Biere

   SAT Competition Benchmark Description

   2022

   BIB
3. Hardware Model Checking Certificates

   Emily Yu, Nils Froleyks, Armin Biere, and 1 more author

   SAT Competition Benchmark Description

   2022

   BIB
4. ReconfAIGERation entering Core Challenge 2022

   Nils Froleyks, Emily Yu, and Armin Biere

   2022

   BIB

2021

1. Single Clause Assumption without Activation Literals to Speed-up IC3

   Nils Froleyks and Armin Biere

   In Formal Methods in Computer Aided Design, FMCAD, 2021

   BIB PDF Abs DOI

   We extend the well-established assumption-based interface of incremental SAT solvers to clauses, allowing the addition of a temporary clause that has the same lifespan as literal assumptions. Our approach is efficient and easy to im- plement in modern CDCL-based solvers. Compared to previous approaches, it does not come with any memory overhead and does not slow down the solver due to disabled activation literals, thus eliminating the need for algorithms like IC3 to restart the SAT solver. All clauses learned under literal and clause assumptions are safe to keep and not implicitly invalidated for containing an activation literal. These changes increase the quality of learned clauses, resulting in better generalization for IC3. We implement the extension in the SAT solver CaDiCaL and evaluate it with the IC3 implementation in the model checker ABC. Our experiments on the benchmarks from a recent hardware model checking competition show a speedup for the average SAT call and a reduction in number of calls per verification instance, resulting in a substantial improvement in model checking time.

2. SAT Competition 2020

   Nils Froleyks, Marijn Heule, Markus Iser, and 2 more authors

   Artificial Intelligence, 2021

   BIB PDF Abs DOI

   The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide a detailed account on the 2020 instantiation of the SAT Competition, including the new competition tracks and benchmark selection procedures, overview of solving strategies implemented in top-performing solvers, and a detailed analysis of the empirical data obtained from running the competition.

3. AI Assisted Design of Sokoban Puzzles Using Automated Planning

   Tomás Balyo and Nils Froleyks

   In ArtsIT, Interactivity and Game Creation - Creative Heritage. New Perspectives from Media Arts and Artificial Intelligence. 10th EAI International Conference, ArtsIT 2021, Virtual Event, December 2-3, 2021, Proceedings, 2021

   BIB PDF Abs DOI

   Designing interesting and challenging levels for a puzzle game is a very difficult and time consuming task. It is often possible to develop random puzzle generators that can produce solvable levels. However, in order to obtain appealing levels, usually a human designer needs to be involved. In this paper we propose a new generic method for assisting human designers to create solvable levels for a puzzle game by using Automated Planning. We will demonstrate our method on the well-known Japanese puzzle game Sokoban.

2020

1. Hardware Model Checking Competition 2020

   Armin Biere, Nils Froleyks, and Mathias Preiner

   In Formal Methods in Computer-Aided Design, FMCAD, 2020

   BIB
2. Proceedings of SAT Competition 2020: Solver and benchmark descriptions

   Tomáš Balyo, Nils Froleyks, Marijn JH Heule, and 3 more authors

   2020

   BIB

2019

1. PASAR - Planning as Satisfiability with Abstraction Refinement

   Nils Christian Froleyks, Tomás Balyo, and Dominik Schreiber

   In Proceedings of the Twelfth International Symposium on Combinatorial Search, SOCS 2019, Napa, California, 16-17 July 2019, 2019

   BIB PDF Abs DOI

   One of the classical approaches to automated planning is the reduction to propositional satisfiability (SAT). Recently, it has been shown that incremental SAT solving can increase the capabilities of several modern encodings for SAT-based planning. In this paper, we present a further improvement to SAT-based planning by introducing a new algorithm named PASAR based on the principles of counterexample guided abstraction refinement (CEGAR). As an abstraction of the original problem, we use a simplified encoding where interference between actions is generally allowed. Abstract plans are converted into actual plans where possible or otherwise used as a counterexample to refine the abstraction. Using benchmark domains from recent International Planning Competitions, we compare our approach to different state-of-the-art planners and find that, in particular, combining PASAR with forward state-space search techniques leads to promising results.

2. PASAR Entering the Sparkle Planning Challenge 2019

   Nils Froleyks, Tomáš Balyo, and Dominik Schreiber

   2019

   BIB
3. PASAR – Planning as Satisfiability with Abstraction Refinement

   Nils Froleyks

   Master’s Thesis

   Sep 2019

   BIB PDF Abs

   We present a new algorithm for the satisficing (non-optimal) classical planning prob- lem. The presented planner participated in the Sparkle Planning Challenge 2019 and won a considerable share (22.13%) of the first prize. We combine SAT-based planning with forward state space search using the principles of counterexample-guided abstraction refinement (CEGAR). A state-of-the-art SAT solver is used to solve an abstraction of the planning task at hand. As an abstraction, we use an incomplete encoding where interference between actions is ignored. With a graph-theoretic test we determine whether the solution found by the SAT solver can be directly transformed into a plan. If it can be transformed, we realize an encoding allowing the application of many actions in parallel (exist-step semantics) in a very compact manner, without imposing a fixed order on the actions. If the transformation is not possible, we use the solution to define a heuristic function that is used during a state space search. If the search fails to find a plan within a very short timeout, the abstraction is refined. To increase the synergy between SAT solving and forward search, both can learn new actions and add them to the problem. This allows the SAT solver to make big jumps in the search space, while the forward search benefits from the SAT solver’s ability to solve combinatorially hard problems. Using benchmark domains from recent international planning competitions, we com- pare our approach with various state-of-the-art planners from the fields of SAT-based planning and heuristic search. On almost all tested domains we can match the per- formance of the best tested solvers and on some domains we outperform the entire competition.

2017

1. Using an Algorithm Portfolio to Solve Sokoban

   Nils Christian Froleyks and Tomás Balyo

   In Proceedings of the Tenth International Symposium on Combinatorial Search, SOCS 2017, 16-17 June 2017, Pittsburgh, Pennsylvania, USA, 2017

   BIB PDF Abs DOI

   The game of Sokoban is an interesting platform for algorithm research. It is hard for humans and computers alike. Even small levels can take a lot of computation for all known algorithms. In this paper we will describe how a search based Sokoban solver can be structured and which algorithms can be used to realize each critical part. We implement a variety of those, construct a number of different solvers and combine them into an algorithm portfolio. The solver we construct this way can outperform existing solvers when run in parallel, that is, our solver with 16 processors outperforms the previous sequential solvers.

2. Using an Algorithm Portfolio to Solve Sokoban

   Nils Froleyks

   Bachelor’s Thesis

   Feb 2017

   BIB PDF Abs

   The game of Sokoban is an interesting platform for algorithm research. It is hard for humans and computers alike. Even with its simple rules and small average level sizes there are levels that take a lot of computation for all known algorithms. In this thesis we will combine different Sokoban solvers with different domain specific enhancements into one portfolio. This portfolio can then be run in parallel on one problem until one solver finds a solution. Additionally the solvers in the portfolio can exchange data to speed up computation. We will validate the approach of algorithm portfolios for designing a parallel Sokoban solver.