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
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, 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
