A learning-based approach to synthesizing invariants for incomplete verification engines

DOI10.1007/s10817-020-09570-zzbMath1468.68074arXiv1712.05581OpenAlexW3043358392MaRDI QIDQ2208307

Shambwaditya Saha, Pranav Garg, Daniel Neider, Daejun Park, P. Madhusudan

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1712.05581

zbMATH Keywords

undecidable theoriesmachine learningsoftware verificationinvariant synthesisincomplete decision procedures

Mathematics Subject Classification ID

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

Related Items (1)

SAT-based invariant inference and its relation to concept learning

Uses Software

• Dafny
• z3
• SIMPLIFY
• VCC
• Boogie
• InvGen
• HIP
• GPUVerify
• c2i
• Houdini
• IronFleet

Cites Work

• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• From invariant checking to invariant inference using randomized search
• Property-directed inference of universal invariants or proving their absence
• Invariant synthesis for incomplete verification engines
• Spatial Interpolants
• Learning refinement types
• Dafny: An Automatic Program Verifier for Functional Correctness
• SAT-Based Model Checking without Unrolling
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• A Data Driven Approach for Algebraic Loop Invariants
• Synthesis of Circular Compositional Program Proofs via Abduction
• Compositional Shape Analysis by Means of Bi-Abduction
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Computer Aided Verification
• ICE-based refinement type discovery for higher-order functional programs

This page was built for publication: A learning-based approach to synthesizing invariants for incomplete verification engines