Yakir Vizel

Publication Activity (10 Years)

Years Active: 2007-2024
Publications (10 Years): 26

Top Topics

Inductive Reasoning

Formal Specification

Top Venues

Publications

Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperty Verification as CHC Satisfiability. ESOP (2) (2024)
Joachim Bard, Swen Jacobs, Yakir Vizel
Automatic and Incremental Repair for Speculative Information Leaks. VMCAI (2) (2024)
Joachim Bard, Swen Jacobs, Yakir Vizel
Automatic and Incremental Repair for Speculative Information Leaks. CoRR (2023)
Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher
Condition Synthesis Realizability via Constrained Horn Clauses. NFM (2023)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperty Verification as CHC Satisfiability. CoRR (2023)
Omer Rappoport, Orna Grumberg, Yakir Vizel
Structure-Guided Solution of Constrained Horn Clauses. ATVA (2023)
Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel
Bounded Model Checking for LLVM. FMCAD (2022)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying verified code. Innov. Syst. Softw. Eng. 18 (3) (2022)
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel
IC3 with Internal Signals. FMCAD (2021)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying Verified Code. ATVA (2021)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. CoRR (2021)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying Verified Code. CoRR (2021)
Roderick Bloem, Swen Jacobs, Yakir Vizel
Efficient Information-Flow Verification Under Speculative Execution. ATVA (2019)
Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. ACM Trans. Design Autom. Electr. Syst. 24 (1) (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CAV (1) (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CoRR (2019)
Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
Interpolating Strong Induction. CAV (2) (2019)
Hari Govind V. K., Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
Interpolating Strong Induction. CoRR (2019)
Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, Sharad Malik
Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37 (8) (2018)
Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. CoRR (2018)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. ATVA (2018)
Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik
Lazy Self-composition for Security Verification. CAV (2) (2018)
Yakir Vizel, Alexander Nadel, Sharad Malik
Solving Constraints over Bit-Vectors with SAT-based Model Checking. SMT (2017)
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
IC3 - Flipping the E in ICE. VMCAI (2017)
Pareesa Ameneh Golnari, Yavuz Yetim, Margaret Martonosi, Yakir Vizel, Sharad Malik
PPU: A Control Error-Tolerant Processor for Streaming Applications with Formal Guarantees. ACM J. Emerg. Technol. Comput. Syst. 13 (3) (2017)
Yakir Vizel, Alexander Nadel, Sharad Malik
Solving linear arithmetic with SAT-based model checking. FMCAD (2017)
Yakir Vizel, Georg Weissenbacher, Sharad Malik
Boolean Satisfiability Solvers and Their Applications in Model Checking. Proc. IEEE 103 (11) (2015)
Pramod Subramanyan, Yakir Vizel, Sayak Ray, Sharad Malik
Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. FMCAD (2015)
Yakir Vizel, Alexander Nadel, Vadim Ryvchin
Efficient generation of small interpolants in CNF. Formal Methods Syst. Des. 47 (1) (2015)
Yakir Vizel, Arie Gurfinkel, Sharad Malik
Fast Interpolating BMC. CAV (1) (2015)
Ameneh Golnari, Yakir Vizel, Sharad Malik
Error-Tolerant Processors: Formal Specification and Verification. ICCAD (2015)
Arie Gurfinkel, Yakir Vizel
DRUPing for interpolates. FMCAD (2014)
Yakir Vizel, Arie Gurfinkel
Interpolating Property Directed Reachability. CAV (2014)
Yakir Vizel, Vadim Ryvchin, Alexander Nadel
Efficient Generation of Small Interpolants in CNF. CAV (2013)
Yakir Vizel, Orna Grumberg, Sharon Shoham
Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS (2013)
Yakir Vizel, Orna Grumberg, Sharon Shoham
Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD (2012)
Yakir Vizel, Orna Grumberg
Interpolation-sequence based model checking. FMCAD (2009)
Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar
Deeper Bound in BMC by Combining Constant Propagation and Abstraction. ASP-DAC (2007)