Loop verification with invariants and contracts
From MaRDI portal
Publication:2152642
DOI10.1007/978-3-030-94583-1_4zbMath1498.68074arXiv2010.05812OpenAlexW4205272345MaRDI QIDQ2152642
Publication date: 8 July 2022
Full work available at URL: https://arxiv.org/abs/2010.05812
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- An elementary and unified approach to program correctness
- Isabelle/HOL. A proof assistant for higher-order logic
- A unifying view on SMT-based software verification
- Hoare-style logic for unstructured programs
- Automating induction for solving Horn clauses
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Circular Coinduction: A Proof Theoretical Foundation
- Verifying Array Programs by Transforming Verification Conditions
- Horn Clause Solvers for Program Verification
- Dafny: An Automatic Program Verifier for Functional Correctness
- Reverse Hoare Logic
- Refinement of Trace Abstraction
- Inferring Loop Invariants Using Postconditions
- The specification statement
- A tutorial on the universality and expressiveness of fold
- Loop invariants
- Program verification through characteristic formulae
- Transforming Programs into Recursive Functions
- Intertwined Forward-Backward Reachability Analysis Using Interpolants
- Automated Reasoning with Analytic Tableaux and Related Methods
- An axiomatic basis for computer programming
- Computer Aided Verification
- Verified analysis of random binary tree structures
- HoIce: an ICE-based non-linear Horn clause solver
- Quantified invariants via syntax-guided synthesis
This page was built for publication: Loop verification with invariants and contracts
