תמונה של דר' יקיר ויזל

דר' יקיר ויזל

יצירת קשר
דף בית:
http://www.cs.technion.ac.il/~yvizel/
דואר אלקטרוני:
yvizelcs.technion.ac.il
תחומי עניין במחקר
אימות פורמלי של חומרה ותוכנה; אלגוריתמי SAT/SMT; שיטות אבסטרקציה; אימות תכונות אבטחה; אימות משולב של מערכות חומרה-תוכנה; שימוש בלמידה לצורך אימות אוטומטי.
פרסומים נבחרים
  • Pramod Subramanyan, Bo{-}Yuan Huang, Yakir Vizel, Aarti Gupta and Sharad Malik.
    Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
    {IEEE} Trans. on {CAD} of Integrated Circuits and Systems, 37(8):1692--1705, 2018 [bibtex]
  • Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad Malik.
    Lazy Self-composition for Security Verification.
    In Computer Aided Verification - 30th International Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {II}, 136--156, 2018 [bibtex]
  • 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]