The formal verification seminar is organized by FM@BIU -- the Formal Methods Group at Bar Ilan University.
We will meet on a bi-weekly basis, starting November 2024, with talks on various topics in formal methods and verification.
We meet on Sundays at 12:00.
Location: CS Building (503), seminar room 226.
Zoom: https://biu-ac-il.zoom.us/j/89046499161
December 7, 2025, Doron Peled, BIU: Monitoring Partial Order Executions
Abstract :
Runtime Verification (RV) allows monitoring the behaviors of a system while checking them against a formal specification. The executions of distributed systems are often modeled using interleaving semantics, where events of different processes are interleaved in a total order. However, certain behavioral properties are difficult to express using interleaving semantics, whereas they can be naturally expressed in terms of partial order semantics. We study the problem of runtime verification for distributed systems based on the global states structure associated with a partial order execution. We present two algorithms for RV with branching temporal specifications and study the complexity of this problem. The first algorithm is for a global temporal logic with past operators we term PaCTL (for Past CTL). It involves constructing the branching structure of global states. We then show a second, more efficient algorithm, for a subset of this logic that we term PaBTL. This algorithm does not require constructing the branching structure. We present implementations for both algorithms with experimental results.
November 23, 2025, Hillel Kugler, BIU: Formal Verification of Kidney Development and Repair
Abstract :
The inference of Gene Regulatory Networks (GRNs) from single-cell data allows for mechanistic characterization of the different cell states and their dynamics in complex biological processes. We use the Reasoning Engine for Interaction Networks, a computational tool based on formal verification, to characterize GRN ensembles in the context of acute kidney injury (AKI). We will explain the biological background, the modeling approach and findings in this study, and outline an ambitious research plan to construct a whole tissue model of kidney development and repair.
Joint work with Eitan Tannenbaum, Dana Markiewitz and Tomer Kalisky, paper appeared recently ACM Conference on Bioinformatics, Computational Biology, and Health Informatics (ACM-BCB 2025)
November 9, 2025, Yoni Zohar, BIU. My Attempts To Save Politeness
Abstract:
Theory combination in Satisfiability Modulo Theories (SMT) deals with combining algorithms for proving formulas over integers, bit-vectors, data structures, and more.
Among the most important combination methods is the polite combination method, which only requires one of the theories to admit some property, while the other theory only has to be decidable.
When polite combination was introduced, it was claimed that the required property is "politeness", a notion I will formally and intuitively describe in my talk. But, later, it was shown that the correctness proof had a bug, and for the proof to work, a stronger property is needed, namely "strong politeness".
This led to the following question: can politeness still be considered a property that is relevant to theory combination?
In this talk I will describe several attempts made by myself and others to answer this question positively, thus saving the politeness property.
No background in theory combination or SMT is assumed, though politeness is expected.
October 26, 2025, Kalev Alpernas, NVIDIA. Formal Verification of Software in the Real World
Abstract:
Formal verification of hardware designs has moved in the past two decades from a niche practice to a staple of the chip design verification flow, aided in part by the fantastic advances in SAT solving technology. Formal verification of software, unfortunately, has yet to see a similar transformation. In this talk, I will present our approach to formal verification of software, including a discussion of the software model checker developed in-house by our team, and some of our successes and failures in getting buy-in from the firmware and software development teams at NVIDIA.
I will close with a short discussion on formal verification of software in a world of AI produced code.
June 8, 2025, Michelle Aluf-Medina, BIU: Formal Verification of Network-Based Biocomputation Circuits
Abstract:
Network-Based Biocomputation Circuits (NBCs) are a new paradigm for solving complex computational problems by utilizing the inherent parallelism of biological agents to traverse designed networks simultaneously. We utilize formal methods and tools to investigate design limitations and detect design flaws before manufacturing physical circuits. Potential manufacturing defects as well as the stochastic nature of biological agents have significant implications on the performance of NBCs. Thus, it is crucial to verify and analyze designed circuits, as well as to study the effects of agents’ stochastic dynamics on circuit behavior. By using these formal methods and tools, conclusions are drawn on correctness of various NBC designs and their efficiency, thereby providing insights into the potential behavior of larger circuits. In addition, thresholds for stochastic behavior within the given NBC instances have been examined as well. Analysis has been conducted using symbolic and probabilistic verification, which has further been analyzed in conjunction with NBC circuit simulation results.
May 25, 2025, Ariel Grunfeld, BGU: Monadic Combinatory Algebras
Abstract:
Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped lambda-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, we put forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics.
April 27, 2025, Omri Isac, HUJI: Neural Network Verification with Proof Production
Abstract:
Deep neural networks (DNNs) are increasingly being employed in safety-critical systems, and there is an urgent need to guarantee their correctness. Consequently, the verification community has devised multiple techniques and tools for verifying DNNs. When DNN verifiers discover an input that triggers an error, that is easy to confirm; but when they report that no error exists, there is no way to ensure that the verification tool itself is not flawed. As multiple errors have already been observed in DNN verification tools, the applicability of DNN verification is questioned.
In this talk, I will present a mechanism for enhancing Simplex-based DNN verifiers with proof production capabilities. We will discuss 1) creating such a mechanism based on a constructive adaptation of the well-known Farkas’ lemma and mechanisms for handling piecewise-linear functions; 2) how to reliably check these proofs; and 3) How proof production could be leveraged to improve the performance of DNN verifiers, using conflict clauses.
March 30, 2025, Dor Atzmon, BIU: Planning Paths for Multiple Moving Agents
Abstract:
In recent years, finding a path for a moving agent has become relevant to many real-world applications, including autonomous driving cars, moving robots, and flying drones. Finding the optimal (shortest) path can be calculated by Heuristic Search algorithms, such as the well-known A* algorithm. These algorithms use heuristics, which estimate the distance to the destination, to intelligently guide the search and quickly return a solution. In automated warehouses and many other applications, multiple agents exist, requiring multiple paths. Such agents, embodied in the world, may need to avoid collisions, which occur when two agents are simultaneously at the same location. In my talk, I will discuss the problem of finding a non-colliding set of paths for multiple moving agents, known as Multi-Agent Path Finding, and a few of its variants.
March 16, 2025, Omer Rappoport, Technion: CHC Satisfiability Modulo Multiple Theories
Abstract:
Constrained Horn Clauses (CHCs) is a fragment of First-Order Logic (FOL) that has gained significant attention in verification in recent years, as many verification problems can be reduced to CHC satisfiability. For instance, verifying the partial correctness of a program can be naturally formulated as CHC satisfiability modulo a background theory, such as Linear Integer Arithmetic. However, since CHCs are FOL formulas, they are typically defined over a single fixed background theory. This restriction poses inherent limitations: some theories are computationally more challenging than others, and not all theories can be combined seamlessly.
To address this, we introduce Multi-Theory CHC-SAT, a generalization of the CHC-SAT problem. In this approach, programs are partitioned into fragments, each translated into a CHC set over its own background theory. The dependencies between fragments are preserved through interface constraints, ensuring consistency across theories. This enables a modular and more flexible approach to CHC satisfiability, allowing different fragments of a program to be verified using the most suitable theory.
In this talk, I will present the Multi-Theory CHC-SAT problem, discuss an algorithm for solving it, and demonstrate its application to bit-precise software verification.
January 23, 2025, Shachar Itzhaky, Technion: Hyperproperty Verification as CHC Satisfiability
Abstract:
Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a total alignment of different executions that facilitates simpler inductive invariants.
We show how this treatment is achieved via a reduction from the verification problem of \forall*\exists* hyperproperties to Constrained Horn Clauses (CHCs). Our starting point is a set of universally quantified formulas in first-order logic (modulo theories) that encode the verification of \forall*\exists* hyperproperties over infinite-state transition systems. The first-order encoding uses uninterpreted predicates to capture the (1) witness function for existential quantification over traces, (2) alignment of executions, and (3) corresponding inductive invariant. Such an encoding was previously proposed for k-safety properties. Unfortunately, finding a satisfying model for the resulting first-order formulas is beyond reach for modern first-order satisfiability solvers. Previous works tackled this obstacle by developing specialized solvers for the aforementioned first-order formulas. In contrast, we show that the same problems can be encoded as CHCs and solved by existing CHC solvers. CHC solvers take advantage of the unique structure of CHC formulas and handle the combination of quantifiers with theories and uninterpreted predicates more efficiently.
Our key technical contribution is a logical transformation of the aforementioned sets of first-order formulas to equi-satisfiable sets of CHCs. The transformation to CHCs is sound and complete, and applying it to the first-order formulas that encode verification of hyperproperties leads to a CHC encoding of these problems. We implemented the CHC encoding in a prototype tool and show that, using existing CHC solvers for solving the CHCs, the approach already outperforms state-of-the-art tools for hyperproperty verification by orders of magnitude.
January 19, 2025, Avraham Raviv, BIU: Formal Verification of DNN-based Computer Vision Tasks
Abstract:
Deep Neural Networks (DNNs) have become integral to computer vision (CV) tasks, yet their use in safety-critical applications raises concerns about reliability and robustness. While existing formal verification efforts focus predominantly on image classification, object detection and other CV tasks remain largely unexplored. This work pioneers the formal verification of DNN-based object detection, introducing a novel formulation, implementation, and initial results. Our approach sets the stage for extending verification to broader CV applications, ensuring safer and more trustworthy AI systems.
January 5, 2025, Hadar Frenkel, BIU: Temporal Causality in Reactive Systems
Abstract:
Counterfactual reasoning is an approach to infer the cause of an observed effect by comparing a given scenario in which the suspected cause and the effect are present, to the hypothetical scenarios where the suspected cause is not present. The seminal works of Halpern and Pearl have provided a definition of counterfactual causality for finite settings. In this talk, we propose an approach to check causality for reactive systems, i.e., systems that interact with their environment over a possibly infinite duration. First, we focus on finding causes for violations of hyperproperties. Hyperproperties, unlike trace properties, can relate multiple traces and thus express complex security properties. Here, the suspected cause is represented by a finite set of events occurring on the set of traces. Then, we lift Halpern and Pearl's definition to the case where the causes themselves (as well as effects) are omega-regular properties, and not only sets of events. We give automata-based construction for our approach and show that the problem of checking whether a given property qualifies as a cause can be encoded as a hyperproperty model-checking problem.
December 8, 2024, Hillel Kugler, BIU: Formal Verification and Synthesis of Gene Regulatory Networks
Abstract:
Gene regulatory networks (GRNs) control the dynamics of gene expression and determine cellular decision-making in biological systems. These networks can be modeled as graphs consisting of vertices representing transcription factors (TFs) and target genes (TGs), as well as edges describing regulatory interactions. Boolean networks are a popular formalism for modeling GRNs, where the value of each component is abstracted to be active (1) or inactive (0). We discuss methods for verification and synthesis of Boolean networks and outline practical applications to real world biological systems and highlight several main challenges in the field.
November 24, 2024, Doron Peled , BIU: Runtime Verification: theory and practice
Abstract:
Abstract: Runtime verification RV is used to monitor the executions of a system against some formal specification and provide a verdict about the satisfaction of it. This is a "light" formal method, as it checks one execution at a time, rather than dealing with all the executions of the system (e.g., as in Theorem Proving or Model Checking).
The challenge is to provide an efficient "on-line" algorithm that can compete with the speed of the observed execution.
Runtime verification for temporal properties (propositional, first order LTL) will be presented. A tool called "deja-vu" developed in collaboration with NASA for RV will be presented. At the end, the generation of runtime monitors automatically using ChatGPT will be presented.
November 10, 2024, Yoni Zohar , BIU: Scalable Bit-Blasting with Abstractions
Abstract:
The dominant state-of-the-art approach for solving bit-vector formulas in Satisfiability Modulo Theories (SMT) is bit-blasting, an eager reduction to propositional logic. Bit-blasting is surprisingly efficient in practice, but does not generally scale well with increasing bit-widths, especially when bit-vector arithmetic is present. In this talk, I'll describe a novel CEGAR-style abstraction-refinement procedure for the theory of fixed-size bit-vectors that significantly improves the scalability of bit-blasting. This includes lemma schemes for various arithmetic bit-vector operators and an abduction-based framework for synthesizing refinement lemmas. An extension of the state-of-the-art SMT solver Bitwuzla with this abstraction-refinement approach was implemented and shows significant improvement on a variety of benchmark sets, including industrial benchmarks that arise from smart contract verification.
Based on a paper from CAV'24 with co-authors Aina Niemetz and Mathias Preiner.