Characteristic formulae for the verification of imperative programs

DOI10.1145/2034773.2034828MaRDI QIDQ5176992zbMATHOpenAlexFDO

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

zbMATH Keywords

total correctnessinteractive verificationcharacteristic formula

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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

Cited in

(27)

• A formalization of programs in first-order logic with a discrete linear order
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Symbolic execution proofs for higher order store programs
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• PML2: integrated program verification in ML
• Refinement to Imperative/HOL
• Formalizing the Edmonds-Karp algorithm
• Verified characteristic formulae for CakeML
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Program verification through characteristic formulae
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Specifying and verifying higher-order Rust iterators
• Cogent: uniqueness types and certifying compilation
• Temporary read-only permissions for separation logic
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• A FOOLish encoding of the next state relations of imperative programs
• Implementing and reasoning about hash-consed data structures in Coq
• A framework for the verification of certifying computations
• Specifying imperative ML-like programs using dynamic logic
• From Sets to Bits in Coq
• Refinement to imperative HOL
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Trustworthy Graph Algorithms (Invited Talk)
• An observationally complete program logic for imperative higher-order functions

Describes a project that uses

Uses Software

• Coq
• CFML

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)