Characteristic formulae for the verification of imperative programs
DOI10.1145/2034773.2034828zbMATH Open1323.68366OpenAlexW4247464325MaRDI QIDQ5176992FDOQ5176992
Authors: Arthur Charguéraud 
Publication date: 5 March 2015
Published in: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2034773.2034828
Recommendations
- Program verification through characteristic formulae
- Verification conditions for source-level imperative programs
- scientific article; zbMATH DE number 2217740
- Integrated approach to analysis and verification of imperative programs
- Verification of imperative programs by constraint logic program transformation
- Programmable verifiers in imperative programming
- scientific article; zbMATH DE number 3907752
- Verifying programs in the calculus of inductive constructions
- Theories for mechanical proofs of imperative programs
- A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cited In (26)
- Title not available (Why is that?)
- From Sets to Bits in Coq
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Cogent: uniqueness types and certifying compilation
- A formalization of programs in first-order logic with a discrete linear order
- Refinement to imperative HOL
- Formalizing the Edmonds-Karp Algorithm
- Symbolic execution proofs for higher order store programs
- A framework for the verification of certifying computations
- An observationally complete program logic for imperative higher-order functions
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Verified Characteristic Formulae for CakeML
- Trustworthy Graph Algorithms (Invited Talk)
- Implementing and reasoning about hash-consed data structures in Coq
- Refinement to Imperative/HOL
- Program verification through characteristic formulae
- Title not available (Why is that?)
- Specifying imperative ML-like programs using dynamic logic
- Specifying and verifying higher-order Rust iterators
- Temporary Read-Only Permissions for Separation Logic
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Uses Software
This page was built for publication: Characteristic formulae for the verification of imperative programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176992)
