RustHorn: CHC-based verification for Rust programs
From MaRDI portal
Recommendations
- Probabilistic Horn clause verification
- Relational verification through Horn clause transformation
- Dafny: an automatic program verifier for functional correctness
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Solving Horn clauses on inductive data types without induction
Cites work
- scientific article; zbMATH DE number 1304000 (Why is no real title available?)
- scientific article; zbMATH DE number 2090840 (Why is no real title available?)
- Automated technology for verification and analysis. 16th international symposium, ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018. Proceedings
- Combinators for bi-directional tree transformations: a linguistic approach to the view update problem
- Fields of logic and computation II. Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday
- HoIce: an ICE-based non-linear Horn clause solver
- ICE-based refinement type discovery for higher-order functional programs
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Lazy abstraction with interpolants for arrays
- Learning inductive invariants by sampling from frequency distributions
- On sentences which are true of direct unions of algebras
- Permission accounting in separation logic
- Quantified Heap Invariants for Object-Oriented Programs
- Quantifiers on demand
- SMT-based model checking for recursive programs
- The Lean theorem prover (system description)
- The Semantics of Predicate Logic as a Programming Language
- The existence of refinement mappings
- Thread modularity at many levels: a pearl in compositional verification
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Viper: a verification infrastructure for permission-based reasoning
Cited in
(11)- Verifying Whiley programs with Boogie
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Solving constrained Horn clauses over algebraic data types
- Efficient modular SMT-based model checking of pointer programs
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Reasoning About Data Trees Using CHCs
- Formally understanding Rust's ownership and borrowing system at the memory level
- Automatic program instrumentation for automatic verification
- Ownership guided C to Rust translation
- The \textsc{Golem} Horn solver
- Specifying and verifying higher-order Rust iterators
Describes a project that uses
Uses Software
This page was built for publication: RustHorn: CHC-based verification for Rust programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041108)
