publications

2026

1. Liveness Proofs for Hardware Model Checking

   Nils Froleyks, Emily Yu, Bart Bogaerts, Armin Biere, and Keijo Heljanko

   In International Conference on Computer Aided Verification (CAV), 2026

   *Distinguished Paper Award*

   PDF abstract to appear

   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. Hardware Model Checking Certification with Certifaiger and Cerbtora

   Nils Froleyks and Emily Yu

   In International Joint Conference on Automated Reasoning (IJCAR), 2026

   PDF abstract to appear

   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.

3. Quantitative Monitoring of Signal First-Order Logic

   Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç, and Emily Yu

   In International Symposium on Formal Methods (FM), 2026

   PDF abstract DOI

   Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.

4. Certifying Constraints in Hardware Model Checking

   Nils Froleyks, Emily Yu, Armin Biere, and Keijo Heljanko

   In International Symposium on Formal Methods (FM), 2026

   PDF abstract DOI

   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. Formal Verification of Neural Certificates Done Dynamically

   Thomas A. Henzinger, Konstantin Kueffner, and Emily Yu

   In International Conference on Runtime Verification (RV), 2025

   PDF abstract DOI

   Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.

2. Scalable Interconnect Learning in Boolean Networks

   Fabian Kresse, Emily Yu, and Christoph H. Lampert

   arXiv preprint arXiv:2507.02585, 2025

   PDF abstract DOI

   Learned Differentiable Boolean Logic Networks (DBNs) already deliver efficient inference on resource-constrained hardware. We extend them with a trainable, differentiable interconnect whose parameter count remains constant as input width grows, allowing DBNs to scale to far wider layers than earlier learnable-interconnect designs while preserving their advantageous accuracy. To further reduce model size, we propose two complementary pruning stages: an SAT-based logic equivalence pass that removes redundant gates without affecting performance, and a similarity-based, data-driven pass that outperforms a magnitude-style greedy baseline and offers a superior compression-accuracy trade-off.

3. Predictive Monitoring of Black-Box Dynamical Systems

   Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde Zikelic

   In Learning for Dynamics and Control Conference (L4DC), 2025

   PDF abstract DOI

   We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor’s expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques.

4. Logic Gate Neural Networks are Good for Verification

   Fabian Kresse, Emily Yu, Christoph H. Lampert, and Thomas A. Henzinger

   In International Conference on Neuro-symbolic Systems (NeuS), PMLR 288:90–103 , 2025

   *Disruptive Idea Award*

   PDF abstract DOI

   Learning-based systems are increasingly deployed across various domains, yet the complexity of traditional neural networks poses significant challenges for formal verification. Unlike conventional neural networks, learned Logic Gate Networks (LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like architecture that is inherently more amenable to symbolic verification, while still delivering promising performance. In this paper, we introduce a SAT encoding for verifying global robustness and fairness in LGNs. We evaluate our method on five benchmark datasets, including a newly constructed 5-class variant, and find that LGNs are both verification-friendly and maintain strong predictive performance.

5. Introducing Certificates to the Hardware Model Checking Competition

   Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko

   In International Conference on Computer Aided Verification (CAV), 2025

   *Distinguished Paper Award*

   PDF abstract 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.

6. Neural Control and Certificate Repair via Runtime Monitoring

   Emily Yu, Dorde Zikelic, and Thomas A. Henzinger

   In AAAI Conference on Artificial Intelligence (AAAI), 2025

   *Selected for oral presentation*

   PDF abstract DOI

   Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.

7. Challenging certificates from model checking

   Nils Froleyks, Emily Yu, and Armin Biere

   In SAT Competition: Solver and Benchmark Descriptions, 2025

   PDF abstract

   The Hardware Model Checking Competition 2024 introduced certificates to the bit-level track of the competition in the form of witness circuits. Checking the correctness of a witness circuit entails solving five SAT formulas; if all of them are unsatisfiable, the witness circuit is valid and the safety of the original model is proven. This benchmark description lists 20 benchmarks submitted to the SAT Competition, selected from certificate validation checks generated using CERTIFAIGER and translated to CNF. Many of these checks could not be solved by MINISAT within a 10-hour time limit, while KISSAT 4.0 successfully checked all valid certificates produced during the model checking competition within the same limit.

2024

1. Certifying Phase Abstraction

   Nils Froleyks, Emily Yu, Armin Biere, and Keijo Heljanko

   In International Joint Conference on Automated Reasoning (IJCAR), 2024

   PDF abstract 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.

2. Ternary Simulation as Abstract Interpretation (Work in Progress)

   Nils Froleyks, Emily Yu, and Armin Biere

   In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2024

   PDF abstract

   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.

2023

1. Towards Compositional Hardware Model Checking Certification

   Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko

   In Formal Methods in Computer-Aided Design (FMCAD), 2023

   PDF abstract 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.

2. Stratified Certification for k-induction (Extended Abstract)

   Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko

   In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2023

   PDF abstract

   Our certification framework from CAV’21 for bit-level k-induction-based model checking was shown to be effective in increasing the trust of verification results even though it partially involved quantifier reasoning. In this extended abstract we summarize our follow-up work presented at FMCAD’22. There we showed how to simplify the original approach by assuming reset functions to be stratified. This way we are able to lift it to word-level and in principle to other theories where quantifier reasoning is difficult. Our FMCAD’22 method requires six simple propositional satisfiability (SAT) checks and one polynomial-time check, allowing certification to remain in co-NP while the original approach required five SAT checks and checking one quantified Boolean formula (QBF). Experimental results show a substantial performance gain for the FMCAD’22 approach. We also presented and evaluated our new tool CERTIFAIGER-WL which is able to certify k-induction-based word-level model checking.

3. BIG Backbones

   Nils Froleyks, Emily Yu, and Armin Biere

   In Formal Methods in Computer-Aided Design (FMCAD), 2023

   PDF abstract DOI

   The backbone of a satisfiable formula is the set of literals that hold true in every model. In this paper we introduce Single Unit Resolution Backbone (SURB) which names both a polynomial-time algorithm for backbone extraction and a class of propositional formulas on which it is complete. We show that this class is a superset of the polynomial-time solvable SLUR formulas. The presented algorithm meets a lower bound on time complexity under the strong exponential-time hypothesis. As a second contribution, we present a version that operates on the binary implication graph (BIG) and implement it as a preprocessor in the recently introduced backbone extractor CADIBACK. Experiments on a large number of SAT competition benchmarks show that our implementation results in faster BIG backbone extraction by an order of magnitude. Additionally, incorporating it as a preprocessor enables CADIBACK to identify up to four times as many backbone literals early on.

4. Certifying Hardware Model Checking

   Emily Yu

   2023

   Johannes Kepler Univeristy Linz (PhD Thesis)

   PDF abstract

   This thesis develops certificate formats and checking procedures for hardware model checking, with the goal of making positive verification results independently checkable. It studies certification for k-induction and related preprocessing techniques, designs witness-circuit-based proof artifacts, and reduces validation to SAT- and QBF-style checks that can be performed by external checkers. The thesis also presents tool support and experimental evaluation on hardware model checking benchmarks.

2022

1. Stratified Certification for k-Induction

   Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko

   In Formal Methods in Computer-Aided Design (FMCAD), 2022

   PDF abstract DOI

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

2. Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications

   Francesco Belardinelli, Alessio Lomuscio, Vadim Malvone, and Emily Yu

   Journal of Artificial Intelligence Research (JAIR), 2022

   PDF abstract DOI

   The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic ATL and ATL* under perfect recall and imperfect information is known to be undecidable. To tackle this problem, we investigate a notion of bounded recall under incomplete information. We present a three-valued semantics for ATL* in this setting and analyze the corresponding model checking problem. We show that the three-valued semantics approximates the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS to incorporate bounded recall, illustrate its use, and present experimental results.

3. Hardware Model Checking Certificates

   Emily Yu, Nils Froleyks, Armin Biere, and Mathias Fleury

   In SAT Competition: Solver and Benchmark Descriptions, 2022

   PDF abstract

   This benchmark description presents SAT and QBF instances generated from a certification framework for k-induction-based hardware model checking. The framework generates an inductive invariant as a proof certificate by extending the original model to a k-witness circuit. Certification is reduced to five SAT checks and one one-alternation QBF: two SAT checks and one QBF verify the combinational simulation relation between the original circuit and the k-witness circuit, while three SAT checks validate the inductive invariant. The resulting formulas are generated by the Certifaiger toolkit from AIGER models and k values obtained from model checking.

4. Unique Reconfiguration Sequence

   Nils Froleyks, Emily Yu, and Armin Biere

   In SAT Competition: Solver and Benchmark Descriptions, 2022

   PDF abstract

   This benchmark description presents SAT Competition instances based on the Independent Set Reconfiguration Problem from the Core Challenge 2022. Given an undirected graph and two independent sets, the task is to find a sequence of independent sets between them where consecutive sets differ in one node. The encoding searches for long valid reconfiguration sequences and adds a uniqueness constraint requiring that no independent set occurs more than once. For a fixed makespan, variables encode the current independent set at each step, clauses enforce independence, cardinality constraints enforce one-node changes between adjacent steps, and additional clauses ensure that every set differs from all previous sets. The benchmark set contains satisfiable and unsatisfiable instances covering low makespans, uniqueness failures, and unsolvable reconfiguration cases.

2021

1. Progress in Certifying Hardware Model Checking Results

   Emily Yu, Armin Biere, and Keijo Heljanko

   In International Conference on Computer Aided Verification (CAV), 2021

   PDF abstract DOI

   We present a formal framework to certify k-induction-based model checking results. The key idea is the notion of a k-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present Certifaiger, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.

2020

1. Model Checking Temporal Epistemic Logic under Bounded Recall

   Francesco Belardinelli, Alessio Lomuscio, and Emily Yu

   In AAAI Conference on Artificial Intelligence (AAAI), 2020

   PDF abstract DOI

   We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLK_BR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We also present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

2019

1. A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas

   Emily Yu, Martina Seidl, and Armin Biere

   In Formal Techniques for Safety-Critical Systems (FTSCS), 2019

   PDF abstract DOI

   We present a framework for model checking CTLK specifications by reducing temporal-epistemic reasoning to quantified Boolean formulas. The approach encodes bounded model checking problems for knowledge and time into QBF, enabling verification of multi-agent systems with a QBF solver backend. We describe the encoding and implementation in MCMAS-QBF and illustrate how QBF-based symbolic reasoning can support model checking against CTLK.

2. Certifying Hardware Model Checking Results

   Emily Yu, Armin Biere, and Keijo Heljanko

   In Formal Engineering Methods (ICFEM), 2019

   PDF abstract DOI

   Model checking is used widely as a formal verification technique for safety-critical systems. Certifying the correctness of model checking results helps increase confidence in the verification procedure and can be achieved by additional book-keeping inside existing model checkers. Based on this, we extend an existing BDD-based model checker as well as an IC3-based incremental inductive model checker to generate certificates during the model checking procedure. We also introduce a proof checker that provides a standardized way to validate certificates generated from model checkers in conjunction with a SAT solver, with the goal of establishing a certification process for the hardware model checking competition.

2018

1. Model Checking Temporal Epistemic Logic under Bounded Recall

   Emily Yu

   2018

   Imperial College London (Master Thesis)

   PDF abstract

   This thesis studies model checking for temporal epistemic logic under bounded recall as a decidable approximation of perfect recall. It develops semantic and algorithmic foundations for reasoning about knowledge and time in multi-agent systems when agents remember only a bounded history, and investigates how bounded recall can be used to approximate otherwise intractable perfect-recall verification problems.