Learning inductive invariants by sampling from frequency distributions
From MaRDI portal
Recommendations
- Rethinking statistical learning theory: learning using statistical invariants
- Learning inference by induction
- Data-Driven Invariant Learning for Probabilistic Programs
- Inductive inference of approximations
- Probabilistic inductive inference: A survey
- Inductive learning and defeasible inference
- Inductive inference systems for learning classes of algorithmically generated sets and structures
- A continuous approach to inductive inference
- Dynamics of inductive inference in a unified framework
Cites work
- Abstractions from proofs
- Automated discovery of simulation between programs
- Exploiting synchrony and symmetry in relational verification
- From invariant checking to invariant inference using randomized search
- From under-approximations to over-approximations and back
- Generalized property directed reachability
- HoIce: an ICE-based non-linear Horn clause solver
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- scientific article; zbMATH DE number 1693447 (Why is no real title available?)
- scientific article; zbMATH DE number 7444022 (Why is no real title available?)
- Interpolation and SAT-based model checking.
- Lazy Abstraction with Interpolants
- Nested interpolants
- Program verification as probabilistic inference
- Property directed equivalence via abstract simulation
- Property-directed incremental invariant generation
- Refinement types for Haskell
- SAT-Based Model Checking without Unrolling
- SMT-based model checking for recursive programs
- Synchronizing constrained Horn clauses
- Syntax-guided termination analysis
- Synthesis of circular compositional program proofs via abduction
- Synthesis of recursive ADT transformations from reusable templates
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Understanding IC3
Cited in
(10)- Preface of the special issue on the conference on formal methods in computer-aided design 2017
- 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
- RustHorn: CHC-based verification for Rust programs
- Efficiently learning safety proofs from appearance as well as behaviours
- Quantified invariants via syntax-guided synthesis
- The \textsc{Golem} Horn solver
- Maximizing branch coverage with constrained Horn clauses
Describes a project that uses
Uses Software
This page was built for publication: Learning inductive invariants by sampling from frequency distributions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225478)
