Photo of Dr. Yakir Vizel

Dr. Yakir Vizel

Contact information
Homepage:
http://www.cs.technion.ac.il/~yvizel/
Email:
yvizelcs.technion.ac.il
Research interests
Formal verification of hardware and software systems; Model Checking; SAT/SMT solving; Abstraction techniques; Security Verification; Hardware-Software Co-Verification; Machine learning for verification.
Selected publications
  • Bo{-}Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta and Sharad Malik.
    Instruction-Level Abstraction {(ILA):} {A} Uniform Specification for System-on-Chip (SoC) Verification.
    CoRR, abs/1801.01114, 2018 [bibtex]
  • Pareesa Ameneh Golnari, Yavuz Yetim, Margaret Martonosi, Yakir Vizel and Sharad Malik.
    {PPU:} {A} Control Error-Tolerant Processor for Streaming Applications with Formal Guarantees.
    {JETC}, 13(3):43:1--43:29, 2017 [bibtex]
  • Yakir Vizel, Alexander Nadel and Sharad Malik.
    Solving linear arithmetic with SAT-based model checking.
    In 2017 Formal Methods in Computer Aided Design, {FMCAD} 2017, Vienna, Austria, October 2-6, 2017, 47--54, 2017 [bibtex]
  • Yakir Vizel, Arie Gurfinkel, Sharon Shoham and Sharad Malik.
    {IC3} - Flipping the {E} in {ICE}.
    In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, {VMCAI} 2017, Paris, France, January 15-17, 2017, Proceedings, 521--538, 2017 [bibtex]
  • Yakir Vizel, Alexander Nadel and Vadim Ryvchin.
    Efficient generation of small interpolants in {CNF}.
    Formal Methods in System Design, 47(1):51--74, 2015 [bibtex]
  • Yakir Vizel, Georg Weissenbacher and Sharad Malik.
    Boolean Satisfiability Solvers and Their Applications in Model Checking.
    Proceedings of the {IEEE}, 103(11):2021--2035, 2015 [bibtex]
  • Yakir Vizel, Arie Gurfinkel and Sharad Malik.
    Fast Interpolating {BMC}.
    In Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}, 641--657, 2015 [bibtex]
  • Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik.
    Template-based Synthesis of Instruction-Level Abstractions for SoC Verification.
    In Formal Methods in Computer-Aided Design, {FMCAD} 2015, Austin, Texas, USA, September 27-30, 2015., 160--167, 2015 [bibtex]
  • Ameneh Golnari, Yakir Vizel and Sharad Malik.
    Error-Tolerant Processors: Formal Specification and Verification.
    In Proceedings of the {IEEE/ACM} International Conference on Computer-Aided Design, {ICCAD} 2015, Austin, TX, USA, November 2-6, 2015, 286--293, 2015 [bibtex]
  • Yakir Vizel and Arie Gurfinkel.
    Interpolating Property Directed Reachability.
    In Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 260--276, 2014 [bibtex]
  • Arie Gurfinkel and Yakir Vizel.
    DRUPing for interpolates.
    In Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland, October 21-24, 2014, 99--106, 2014 [bibtex]
  • Orna Grumberg, Sharon Shoham and Yakir Vizel.
    SAT-based Model Checking: Interpolation, IC3, and Beyond.
    In Software Systems Safety, 17--41, 2014 [bibtex]
  • Yakir Vizel, Vadim Ryvchin and Alexander Nadel.
    Efficient Generation of Small Interpolants in {CNF}.
    In Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, 330--346, 2013 [bibtex]
  • Yakir Vizel, Orna Grumberg and Sharon Shoham.
    Intertwined Forward-Backward Reachability Analysis Using Interpolants.
    In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, {TACAS} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings, 308--323, 2013 [bibtex]
  • Yakir Vizel, Orna Grumberg and Sharon Shoham.
    Lazy abstraction and SAT-based reachability in hardware model checking.
    In Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge, UK, October 22-25, 2012, 173--181, 2012 [bibtex]
  • Yakir Vizel and Orna Grumberg.
    Interpolation-sequence based model checking.
    In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, {FMCAD} 2009, 15-18 November 2009, Austin, Texas, {USA}, 1--8, 2009 [bibtex]
  • Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel and Yael Zbar.
    Deeper Bound in {BMC} by Combining Constant Propagation and Abstraction.
    In Proceedings of the 12th Conference on Asia South Pacific Design Automation, {ASP-DAC} 2007, Yokohama, Japan, January 23-26, 2007, 304--309, 2007 [bibtex]