@inproceedings{22006, abstract = {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.}, author = {Chalupa, Marek and Henzinger, Thomas A and Sarac, Naci E and Yu, Zhengqi}, booktitle = {27th International Symposium on Formal Methods}, isbn = {9783032262196}, issn = {1611-3349}, keywords = {Signal first-order logic, Robustness-based quantitative semantics, Online runtime monitoring}, location = {Tokyo, Japan}, pages = {214--233}, publisher = {Springer Nature}, title = {{Quantitative monitoring of Signal First-Order logic}}, doi = {10.1007/978-3-032-26220-2_11}, volume = {16557}, year = {2026}, } @inproceedings{21091, abstract = {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.}, author = {Henzinger, Thomas A and Kueffner, Konstantin and Yu, Zhengqi}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {54--72}, publisher = {Springer Nature}, title = {{Formal verification of neural certificates done dynamically}}, doi = {10.1007/978-3-032-05435-7_4}, volume = {16087}, year = {2025}, } @inproceedings{19668, abstract = {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.}, author = {Yu, Zhengqi and Zikelic, Dorde and Henzinger, Thomas A}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {25}, pages = {26409--26417}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Neural control and certificate repair via runtime monitoring}}, doi = {10.1609/aaai.v39i25.34840}, volume = {39}, year = {2025}, } @inproceedings{20189, abstract = {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.}, author = {Froleyks, Nils and Yu, Zhengqi and Preiner, Mathias and Biere, Armin and Heljanko, Keijo}, booktitle = {37th International Conference on Computer Aided Verification}, isbn = {9783031986673}, issn = {1611-3349}, location = {Zagreb, Croatia}, pages = {281--295}, publisher = {Springer Nature}, title = {{Introducing certificates to the hardware model checking competition}}, doi = {10.1007/978-3-031-98668-0_14}, volume = {15931}, year = {2025}, } @inproceedings{20256, abstract = {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.}, author = {Henzinger, Thomas A and Kresse, Fabian and Mallik, Kaushik and Yu, Zhengqi and Zikelic, Dorde}, booktitle = {7th Annual Learning for Dynamics & Control Conference}, issn = {2640-3498}, location = {Ann Arbor, MI, United States}, pages = {804--816}, publisher = {ML Research Press}, title = {{Predictive monitoring of black-box dynamical systems}}, volume = {283}, year = {2025}, } @inproceedings{20296, abstract = {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.}, author = {Kresse, Fabian and Yu, Zhengqi and Lampert, Christoph and Henzinger, Thomas A}, booktitle = {2nd International Conferenceon Neuro-Symbolic Systems}, issn = {2640-3498}, location = {Philadephia, PA, United States}, publisher = {ML Research Press}, title = {{Logic gate neural networks are good for verification}}, volume = {288}, year = {2025}, } @inproceedings{17413, abstract = {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.}, author = {Froleyks, Nils and Yu, Zhengqi and Biere, Armin and Heljanko, Keijo}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, isbn = {9783031634970}, issn = {1611-3349}, location = {Nancy, France}, pages = {284--303}, publisher = {Springer Nature}, title = {{Certifying phase abstraction}}, doi = {10.1007/978-3-031-63498-7_17}, volume = {14739}, year = {2024}, } @inproceedings{17053, 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.}, author = {Froleyks, Nils and Yu, Zhengqi and Biere, Armin}, booktitle = {27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems}, isbn = {9783800762682}, location = {Kaiserslautern, Germany}, pages = {148--151}, publisher = {VDE Verlag}, title = {{Ternary simulation as abstract interpretation (Work in Progress)}}, year = {2024}, }