Learning inductive invariants by sampling from frequency distributions

DOI10.1007/s10703-020-00349-xzbMath1506.68054OpenAlexW3100075217MaRDI QIDQ2225478

Samuel J. Kaufman, Rastislav Bodík, Grigory Fedyukovich

Publication date: 8 February 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-020-00349-x

zbMATH Keywords

software verificationinvariant synthesissyntax-guided synthesis

Mathematics Subject Classification ID

Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

RustHorn: CHC-Based Verification for Rust Programs ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Unbounded procedure summaries from bounded environments ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Preface of the special issue on the conference on formal methods in computer-aided design 2017

Uses Software

• FLATA
• z3
• Princess
• UFO
• Eldarica
• Ivy
• c2i
• Houdini
• Spacer
• RAHFT
• LiquidHaskell
• Ivy
• TreeAutomizer

Cites Work

• SMT-based model checking for recursive programs
• From invariant checking to invariant inference using randomized search
• Property-directed incremental invariant generation
• Refinement types for Haskell
• Understanding IC3
• Generalized Property Directed Reachability
• From Under-Approximations to Over-Approximations and Back
• SAT-Based Model Checking without Unrolling
• Program verification as probabilistic inference
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Synthesis of Recursive ADT Transformations from Reusable Templates
• Abstractions from proofs
• Automated Discovery of Simulation Between Programs
• Property Directed Equivalence via Abstract Simulation
• Synchronizing Constrained Horn Clauses
• Nested interpolants
• Synthesis of Circular Compositional Program Proofs via Abduction
• Lazy Abstraction with Interpolants
• Computer Aided Verification
• Syntax-guided termination analysis
• Exploiting synchrony and symmetry in relational verification
• HoIce: an ICE-based non-linear Horn clause solver
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Learning inductive invariants by sampling from frequency distributions