Characteristic formulae for the verification of imperative programs
From MaRDI portal
Publication:5176992
DOI10.1145/2034773.2034828zbMath1323.68366OpenAlexW4247464325MaRDI QIDQ5176992
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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (24)
A formalization of programs in first-order logic with a discrete linear order ⋮ Symbolic execution proofs for higher order store programs ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Refinement to Imperative/HOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Temporary Read-Only Permissions for Separation Logic ⋮ Verified Characteristic Formulae for CakeML ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Refinement to imperative HOL ⋮ From Sets to Bits in Coq ⋮ Specifying and verifying higher-order Rust iterators ⋮ Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Formalizing the Edmonds-Karp Algorithm ⋮ Cogent: uniqueness types and certifying compilation ⋮ A framework for the verification of certifying computations ⋮ Implementing and reasoning about hash-consed data structures in Coq
Uses Software
This page was built for publication: Characteristic formulae for the verification of imperative programs
