\textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants

DOI10.1007/978-3-030-32304-2_16MaRDI QIDQ6536295zbMATH OpenFDO

Authors Daniel Neider, Shambwaditya Saha, Pranav Garg, Parthasarathy Madhusudan

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-32304-2_16

zbMATH Keywords

conjunctive formulasHorn-ICE learninginvariant synthesismachine learning

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Learning and adaptive systems in artificial intelligence (68T05)

Recommendations

• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• Invariant Synthesis for Combined Theories
• Property-directed inference of universal invariants or proving their absence
• Property-directed incremental invariant generation
• Automatically inferring loop invariants via algorithmic learning

Cites work

• A data driven approach for algebraic loop invariants
• A Greedy Heuristic for the Set-Covering Problem
• Computer Aided Verification
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• IC3 -- flipping the E in ICE
• ICE-based refinement type discovery for higher-order functional programs
• Interpolation and SAT-based model checking.
• Invariant synthesis for incomplete verification engines
• Reducibility among combinatorial problems
• SAT-Based Model Checking without Unrolling

This page was built for publication: \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536295)