IC3 - Flipping the E in ICE

Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

תקציר

Induction is a key element of state-of-the-art verification techniques. Automatically synthesizing and verifying inductive invariants is at the heart of Model Checking of safety properties. In this paper, we study the relationship between two popular approaches to synthesizing inductive invariants: SAT-based Model Checking (SAT-MC) and Machine Learning-based Invariant Synthesis (MLIS). Our goal is to identify and formulate the theoretical similarities and differences between the two frameworks. We focus on two flagship algorithms: IC3 (an instance of SAT-MC) and ICE (an instance of MLIS). We show that the two frameworks are very similar yet distinct. For a meaningful comparison, we introduce RICE, an extension of ICE with relative induction and show how IC3 can be implemented as an instance of RICE. We believe this work contributes to the understanding of inductive invariant synthesis and will serve as a foundation for further improvements to both SAT-MC and MLIS algorithms.

שפה מקוריתאנגלית
כותר פרסום המארחVerification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
עורכיםAhmed Bouajjani, David Monniaux
עמודים521-538
מספר עמודים18
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - 2017
אירוע18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, צרפת
משך הזמן: 15 ינו׳ 201717 ינו׳ 2017

סדרות פרסומים

שםLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
כרך10145 LNCS

כנס

כנס18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
מדינה/אזורצרפת
עירParis
תקופה15/01/1717/01/17

ASJC Scopus subject areas

  • ???subjectarea.asjc.2600.2614???
  • ???subjectarea.asjc.1700.1700???

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'IC3 - Flipping the E in ICE'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי