Deeper Bound in BMC by Combining Constant Propagation and Abstraction. - Roy Armoni; Limor Fix; Ranan Fraer; Tamir Heyman; Moshe Y. Vardi; Yakir Vizel; Yael Zbar (ASP-DAC, 2007)

Interpolation-sequence based model checking. - Yakir Vizel; Orna Grumberg (FMCAD, 2009)

Lazy abstraction and SAT-based reachability in hardware model checking. - Yakir Vizel; Orna Grumberg; Sharon Shoham (FMCAD, 2012)

Intertwined Forward-Backward Reachability Analysis Using Interpolants. - Yakir Vizel; Orna Grumberg; Sharon Shoham (TACAS, 2013)

Interpolating Property Directed Reachability. - Yakir Vizel; Arie Gurfinkel (CAV, 2014)

DRUPing for interpolates. - Arie Gurfinkel; Yakir Vizel (FMCAD, 2014)

SAT-based model checking using interpolation and IC3. - Yakir Vizel (2014)

SAT-based Model Checking: Interpolation, IC3, and Beyond. - Orna Grumberg; Sharon Shoham; Yakir Vizel (Software Systems Safety, 2014)

Fast Interpolating BMC. - Yakir Vizel; Arie Gurfinkel; Sharad Malik (CAV (1), 2015)

Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. - Pramod Subramanyan; Yakir Vizel; Sayak Ray; Sharad Malik (FMCAD, 2015)

Error-Tolerant Processors: Formal Specification and Verification. - Ameneh Golnari; Yakir Vizel; Sharad Malik (ICCAD, 2015)

Efficient generation of small interpolants in CNF. - Yakir Vizel; Alexander Nadel; Vadim Ryvchin (Formal Methods Syst. Des., 2015)

Boolean Satisfiability Solvers and Their Applications in Model Checking. - Yakir Vizel; Georg Weissenbacher; Sharad Malik (Proc. IEEE, 2015)

Solving linear arithmetic with SAT-based model checking. - Yakir Vizel; Alexander Nadel; Sharad Malik (FMCAD, 2017)

Solving Constraints over Bit-Vectors with SAT-based Model Checking. - Yakir Vizel; Alexander Nadel; Sharad Malik (SMT, 2017)

IC3 - Flipping the E in ICE. - Yakir Vizel; Arie Gurfinkel; Sharon Shoham; Sharad Malik (VMCAI, 2017)

PPU: A Control Error-Tolerant Processor for Streaming Applications with Formal Guarantees. - Pareesa Ameneh Golnari; Yavuz Yetim; Margaret Martonosi; Yakir Vizel; Sharad Malik (ACM J. Emerg. Technol. Comput. Syst., 2017)

Quantifiers on Demand. - Arie Gurfinkel; Sharon Shoham; Yakir Vizel (ATVA, 2018)

Lazy Self-composition for Security Verification. - Weikun Yang; Yakir Vizel; Pramod Subramanyan; Aarti Gupta; Sharad Malik (CAV (2), 2018)

Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. - Pramod Subramanyan; Bo-Yuan Huang 001; Yakir Vizel; Aarti Gupta; Sharad Malik (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

Efficient Information-Flow Verification Under Speculative Execution. - Roderick Bloem; Swen Jacobs; Yakir Vizel (ATVA, 2019)

Interpolating Strong Induction. - Hari Govind Vediramana Krishnan; Yakir Vizel; Vijay Ganesh 001; Arie Gurfinkel (CAV (2), 2019)

Property Directed Self Composition. - Ron Shemer; Arie Gurfinkel; Sharon Shoham; Yakir Vizel (CAV (1), 2019)

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. - Bo-Yuan Huang 001; Hongce Zhang; Pramod Subramanyan; Yakir Vizel; Aarti Gupta; Sharad Malik (ACM Trans. Design Autom. Electr. Syst., 2019)

IC3 with Internal Signals. - Rohit Dureja; Arie Gurfinkel; Alexander Ivrii; Yakir Vizel (FMCAD, 2021)

Bounded Model Checking for LLVM. - Siddharth Priya; Yusen Su; Yuyan Bao; Xiang Zhou; Yakir Vizel; Arie Gurfinkel (FMCAD, 2022)

Verifying verified code. - Siddharth Priya; Xiang Zhou; Yusen Su; Yakir Vizel; Yuyan Bao; Arie Gurfinkel (Innov. Syst. Softw. Eng., 2022)

Structure-Guided Solution of Constrained Horn Clauses. - Omer Rappoport; Orna Grumberg; Yakir Vizel (ATVA, 2023)

Condition Synthesis Realizability via Constrained Horn Clauses. - Bat-Chen Rothenberg; Orna Grumberg; Yakir Vizel; Eytan Singher (NFM, 2023)

Hyperproperty Verification as CHC Satisfiability. - Shachar Itzhaky; Sharon Shoham; Yakir Vizel (ESOP (2), 2024)

Automatic and Incremental Repair for Speculative Information Leaks. - Joachim Bard; Swen Jacobs; Yakir Vizel (VMCAI (2), 2024)

Property Directed Reachability with Extended Resolution. - Andrew Luka; Yakir Vizel (CAV (1), 2025)

Revisiting DRUP-Based Interpolants with CaDiCaL 2.0. - Basel Khouri; Yakir Vizel (TACAS (2), 2025)