RustHorn: CHC-Based Verification for Rust Programs

DOI10.1007/978-3-030-44914-8_18OpenAlexW3100536147MaRDI QIDQ5041108

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Verifying Whiley programs with Boogie

Uses Software

• Coq
• Spec#
• VCC
• Cyclone
• Viper
• Lean
• SeaHorn
• Spacer
• MoCHi
• GitHub
• Rust
• Rust2Viper
• Crust
• RustBelt

Cites Work

• Unnamed Item
• Unnamed Item
• Fields of logic and computation II. Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday
• SMT-based model checking for recursive programs
• The existence of refinement mappings
• Automated technology for verification and analysis. 16th international symposium, ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018. Proceedings
• Learning inductive invariants by sampling from frequency distributions
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Iris
• Lazy Abstraction with Interpolants for Arrays
• The Lean Theorem Prover (System Description)
• The Semantics of Predicate Logic as a Programming Language
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Quantified Heap Invariants for Object-Oriented Programs
• Combinators for bi-directional tree transformations
• Permission accounting in separation logic
• Thread modularity at many levels: a pearl in compositional verification
• On sentences which are true of direct unions of algebras
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• ICE-based refinement type discovery for higher-order functional programs
• Quantifiers on demand
• HoIce: an ICE-based non-linear Horn clause solver