48 citations · 51 across the 9 of their papers we have counts for
11 papers
Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning
Omer Rappoport, Orna Grumberg, Yakir Vizel
Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors () is fundamental to bit-precise program verification. However…
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
Romy Peled, Daniel Kroening, Michael Tautschnig +1
Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and th…
Property Directed Reachability with Extended Resolution
Andrew Luka, Yakir Vizel
Property Directed Reachability (\textsc{Pdr}), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While \textsc{Pdr} is…
Revisiting DRUP-based Interpolants with CaDiCaL 2.0
Basel Khouri, Yakir Vizel
We present our implementation of DRUP-based interpolants in CaDiCaL 2.0, and evaluate performance in the bit-level model checker Avy using the Hardware Model Checking Competition b…
Automatic and Incremental Repair for Speculative Information Leaks
Joachim Bard, Swen Jacobs, Yakir Vizel
We present CureSpec, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative ex…
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, su…
Verifying Verified Code
Siddharth Priya, Xiang Zhou, Yusen Su +3
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explo…
Quantifiers on Demand
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theo…
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…
Property Directed Self Composition
Ron Shemer, Arie Gurfinkel, Sharon Shoham +1
We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self co…
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification
Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan +3
Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to th…