Efficient generation of inductive validity cores for safety properties

Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

Abstract

Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, and can also be used to measure completeness of a set of requirements over a model. In this paper, we present a new algorithm to efficiently compute the inductive validity core (IVC) within a model necessary for inductive proofs of safety properties for sequential systems. The algorithm is based on the UNSAT core support built into current SMT solvers and a novel encoding of the inductive problem to try to generate a minimal inductive validity core. We prove our algorithm is correct, and describe its implementation in the JKind model checker for Lustre models. We then present an experiment in which we benchmark the algorithm in terms of speed, diversity of produced cores, and minimality, with promising results.

Original languageEnglish (US)
Title of host publicationFSE 2016 - Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering
EditorsZhendong Su, Thomas Zimmermann, Jane Cleland-Huang
PublisherAssociation for Computing Machinery
Pages314-325
Number of pages12
ISBN (Electronic)9781450342186
DOIs
StatePublished - Nov 1 2016
Event24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016 - Seattle, United States
Duration: Nov 13 2016Nov 18 2016

Publication series

NameProceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering
Volume13-18-November-2016

Conference

Conference24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016
CountryUnited States
CitySeattle
Period11/13/1611/18/16

Keywords

  • IC3/PDR
  • K-Induction
  • Requirements Completeness
  • Traceability

Fingerprint Dive into the research topics of 'Efficient generation of inductive validity cores for safety properties'. Together they form a unique fingerprint.

Cite this