Program verification through characteristic formulae
From MaRDI portal
Publication:5176951
DOI10.1145/1863543.1863590zbMath1323.68202OpenAlexW2013532785MaRDI QIDQ5176951
Publication date: 5 March 2015
Published in: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1863543.1863590
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (13)
A formalization of programs in first-order logic with a discrete linear order ⋮ Loop verification with invariants and contracts ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation ⋮ Unnamed Item ⋮ 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 ⋮ A Coq Library for Internal Verification of Running-Times ⋮ CFML ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Cogent: uniqueness types and certifying compilation
Uses Software
This page was built for publication: Program verification through characteristic formulae
