Yakir Vizel

49 papers A* 2A 2B 13Journal 17Unranked 11
YearRankTypeTitle / Venue / Authors
2025 J jnl
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
CoRR
Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel
2025 J jnl
Preface of the special issue on the Conference on Computer-Aided Verification 2022.
Formal Methods Syst. Des.
Sharon Shoham, Yakir Vizel
2025 — conf
Property Directed Reachability with Extended Resolution.
CAV (1)
Andrew Luka, Yakir Vizel
2025 J jnl
Property Directed Reachability with Extended Resolution.
CoRR
Andrew Luka, Yakir Vizel
2025 — conf
Revisiting DRUP-Based Interpolants with CaDiCaL 2.0.
TACAS (2)
Basel Khouri, Yakir Vizel
2025 J jnl
Revisiting DRUP-based Interpolants with CaDiCaL 2.0.
CoRR
Basel Khouri, Yakir Vizel
2024 — conf
Automatic and Incremental Repair for Speculative Information Leaks.
VMCAI (2)
Joachim Bard, Swen Jacobs, Yakir Vizel
2024 — conf
Hyperproperty Verification as CHC Satisfiability.
ESOP (2)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2023 J jnl
Automatic and Incremental Repair for Speculative Information Leaks.
CoRR
Joachim Bard, Swen Jacobs, Yakir Vizel
2023 — conf
Condition Synthesis Realizability via Constrained Horn Clauses.
NFM
Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher
2023 J jnl
Hyperproperty Verification as CHC Satisfiability.
CoRR
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2023 B conf
Structure-Guided Solution of Constrained Horn Clauses.
ATVA
Omer Rappoport, Orna Grumberg, Yakir Vizel
2022 B conf
Bounded Model Checking for LLVM.
FMCAD
Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel
2022 — ed.
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I
CAV (1)
Sharon Shoham, Yakir Vizel
2022 — ed.
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II
CAV (2)
Sharon Shoham, Yakir Vizel
2022 J jnl
Verifying verified code.
Innov. Syst. Softw. Eng.
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021 B conf
IC3 with Internal Signals.
FMCAD
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel
2021 J jnl
Quantifiers on Demand.
CoRR
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2021 B ed.
Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings
VMCAI
Fritz Henglein, Sharon Shoham, Yakir Vizel
2021 B conf
Verifying Verified Code.
ATVA
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021 J jnl
Verifying Verified Code.
CoRR
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2019 B conf
Efficient Information-Flow Verification Under Speculative Execution.
ATVA
Roderick Bloem, Swen Jacobs, Yakir Vizel
2019 J jnl
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification.
ACM Trans. Design Autom. Electr. Syst.
Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
2019 — conf
Interpolating Strong Induction.
CAV (2)
Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
2019 J jnl
Interpolating Strong Induction.
CoRR
Hari Govind V. K., Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
2019 — conf
Property Directed Self Composition.
CAV (1)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2019 J jnl
Property Directed Self Composition.
CoRR
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2018 J jnl
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification.
CoRR
Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
2018 — conf
Lazy Self-composition for Security Verification.
CAV (2)
Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik
2018 B conf
Quantifiers on Demand.
ATVA
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2018 J jnl
Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, Sharad Malik
2017 B conf
IC3 - Flipping the E in ICE.
VMCAI
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
2017 J jnl
PPU: A Control Error-Tolerant Processor for Streaming Applications with Formal Guarantees.
ACM J. Emerg. Technol. Comput. Syst.
Pareesa Ameneh Golnari, Yavuz Yetim, Margaret Martonosi, Yakir Vizel, Sharad Malik
2017 — conf
Solving Constraints over Bit-Vectors with SAT-based Model Checking.
SMT
Yakir Vizel, Alexander Nadel, Sharad Malik
2017 B conf
Solving linear arithmetic with SAT-based model checking.
FMCAD
Yakir Vizel, Alexander Nadel, Sharad Malik
2015 J jnl
Boolean Satisfiability Solvers and Their Applications in Model Checking.
Proc. IEEE
Yakir Vizel, Georg Weissenbacher, Sharad Malik
2015 J jnl
Efficient generation of small interpolants in CNF.
Formal Methods Syst. Des.
Yakir Vizel, Alexander Nadel, Vadim Ryvchin
2015 A conf
Error-Tolerant Processors: Formal Specification and Verification.
ICCAD
Ameneh Golnari, Yakir Vizel, Sharad Malik
2015 — conf
Fast Interpolating BMC.
CAV (1)
Yakir Vizel, Arie Gurfinkel, Sharad Malik
2015 B conf
Template-based Synthesis of Instruction-Level Abstractions for SoC Verification.
FMCAD
Pramod Subramanyan, Yakir Vizel, Sayak Ray, Sharad Malik
2014 B conf
DRUPing for interpolates.
FMCAD
Arie Gurfinkel, Yakir Vizel
2014 A* conf
Interpolating Property Directed Reachability.
CAV
Yakir Vizel, Arie Gurfinkel
2014 — ch.
SAT-based Model Checking: Interpolation, IC3, and Beyond.
Software Systems Safety
Orna Grumberg, Sharon Shoham, Yakir Vizel
2014 — —
SAT-based model checking using interpolation and IC3.
Yakir Vizel
2013 A* conf
Efficient Generation of Small Interpolants in CNF.
CAV
Yakir Vizel, Vadim Ryvchin, Alexander Nadel
2013 A conf
Intertwined Forward-Backward Reachability Analysis Using Interpolants.
TACAS
Yakir Vizel, Orna Grumberg, Sharon Shoham
2012 B conf
Lazy abstraction and SAT-based reachability in hardware model checking.
FMCAD
Yakir Vizel, Orna Grumberg, Sharon Shoham
2009 B conf
Interpolation-sequence based model checking.
FMCAD
Yakir Vizel, Orna Grumberg
2007 — conf
Deeper Bound in BMC by Combining Constant Propagation and Abstraction.
ASP-DAC
Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar