BIU Formal Verification Seminar

The Next Talk is... 

October 26, 2025, Kalev Alpernas, NVIDIA. Title TBD

Future Talks

Past Talks

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.