Invariant Inference with Provable Complexity from the Monotone Theory

Yotam M.Y. Feldman, Sharon Shoham

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

תקציר

Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, but non-trivial upper bounds on the computational complexity of such algorithms are scarce, and limited to simple syntactic forms of invariants. In this paper we achieve invariant inference algorithms, in the domain of propositional transition systems, with provable upper bounds on the number of SAT calls. We do this by building on the monotone theory, developed by Bshouty for exact learning Boolean formulas. We prove results for two invariant inference frameworks: (i) model-based interpolation, where we show an algorithm that, under certain conditions about reachability, efficiently infers invariants when they have both short CNF and DNF representations (transcending previous results about monotone invariants); and (ii) abstract interpretation in a domain based on the monotone theory that was previously studied in relation to property-directed reachability, where we propose an efficient implementation of the best abstract transformer, leading to overall complexity bounds on the number of SAT calls. These results build on a novel procedure for computing least monotone overapproximations.

שפה מקוריתאנגלית
כותר פרסום המארחStatic Analysis - 29th International Symposium, SAS 2022, Proceedings
עורכיםGagandeep Singh, Caterina Urban
מוציא לאורSpringer Science and Business Media Deutschland GmbH
עמודים201-226
מספר עמודים26
מסת"ב (מודפס)9783031223075
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - 2022
אירוע29th International Static Analysis Symposium, SAS 2022 - Auckland, ניו זילנד
משך הזמן: 5 דצמ׳ 20227 דצמ׳ 2022

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

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

כנס

כנס29th International Static Analysis Symposium, SAS 2022
מדינה/אזורניו זילנד
עירAuckland
תקופה5/12/227/12/22

ASJC Scopus subject areas

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

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'Invariant Inference with Provable Complexity from the Monotone Theory'. יחד הם יוצרים טביעת אצבע ייחודית.

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