Program verification through characteristic formulae

DOI10.1145/1863543.1863590zbMath1323.68202OpenAlexW2013532785MaRDI QIDQ5176951

Arthur Charguéraud

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

zbMATH Keywords

total correctnesscharacteristic formulafunctional program

Mathematics Subject Classification ID

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

• Coq

This page was built for publication: Program verification through characteristic formulae