Publications

A full publication list can be found on my DBLP profile.

  1. Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel and Eytan Singher “Condition Synthesis Realizablity via Constrained Horn Clauses”, in proceedings of NFM 2023.
  2. Siddharth Priya, Xiang Zhou, Yuyan Bao, Yusen Su, Yakir Vizel and Arie Gurfinkel “Bounded Model Checking for LLVM" in proceedings of FMCAD 2022.
  3. [BEST PAPER AWARD] Rohit Dureja, Arie Gurfinkel, Alexander Iivri, Yakir Vizel “IC3 with Internal Signals”, in proceedings of FMCAD 2021.
  4. Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel “Verifying Verified Code”, in proceedings of ATVA 2021.
  5. Roderick Bloem, Swen Jacobs, Yakir Vizel, "Efficient Information-Flow Verification Under Speculative Execution." In the proceedings of ATVA 2019.
  6. Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel, "Property Directed Self Composition." In the proceedings of CAV (1), 2019.
  7. Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel, "Interpolating Strong Induction." In the proceedings of CAV (2), 2019.
  8. Arie Gurfinkel, Sharon Shoham, Yakir Vizel, "Quantifiers on Demand." In the proceedings of ATVA, 2018.
  9. Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik, "Lazy Self-composition for Security Verification." In the proceedings of CAV (2), 2018.
  10. Yakir Vizel, Alexander Nadel, Sharad Malik, "Solving linear arithmetic with SAT-based model checking." In the proceedings of FMCAD, 2017.
  11. Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik, "IC3 - Flipping the E in ICE." In the proceedings of VMCAI, 2017.
  12. Pramod Subramanyan, Yakir Vizel, Sayak Ray, Sharad Malik, "Template-based Synthesis of Instruction-Level Abstractions for SoC Verification." In the proceedings of FMCAD, 2015.
  13. Ameneh Golnari, Yakir Vizel, Sharad Malik, "Error-Tolerant Processors: Formal Specification and Verification." In the proceedings of ICCAD, 2015.
  14. Yakir Vizel, Arie Gurfinkel, Sharad Malik, "Fast Interpolating BMC." In the proceedings of CAV (1), 2015.
  15. Arie Gurfinkel, Yakir Vizel, "DRUPing for interpolates." In the proceedings of FMCAD, 2014.
  16. Yakir Vizel, Arie Gurfinkel, "Interpolating Property Directed Reachability." In the proceedings of CAV, 2014.
  17. Orna Grumberg, Sharon Shoham, Yakir Vizel, "SAT-based Model Checking: Interpolation, IC3, and Beyond." In the proceedings of Software Systems Safety, 2014.
  18. Yakir Vizel, Vadim Ryvchin, Alexander Nadel, "Efficient Generation of Small Interpolants in CNF." In the proceedings of CAV, 2013.
  19. Yakir Vizel, Orna Grumberg, Sharon Shoham, "Intertwined Forward-Backward Reachability Analysis Using Interpolants." In the proceedings of TACAS, 2013.
  20. Yakir Vizel, Orna Grumberg, Sharon Shoham, "Lazy abstraction and SAT-based reachability in hardware model checking." In the proceedings of FMCAD, 2012.
  21. Yakir Vizel, Orna Grumberg, "Interpolation-sequence based model checking." In the proceedings of FMCAD, 2009.
  22. Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Vardi, Yakir Vizel, Yael Zbar, "Deeper Bound in BMC by Combining Constant Propagation and Abstraction." In the proceedings of ASP-DAC, 2007.