Program verification through characteristic formulae

DOI10.1145/1863543.1863590MaRDI QIDQ5176951zbMATH OpenOpenAlexFDO

Authors 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

characteristic formulafunctional programtotal correctness

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Characteristic formulae for the verification of imperative programs
• scientific article; zbMATH DE number 868107
• scientific article; zbMATH DE number 4024753
• Verification of procedural programs
• Program verification by coinduction
• scientific article; zbMATH DE number 3907752
• Problem-oriented program verification
• Extraction and verification of programs by analysis of formal proofs

Cited in

(21)

• Loop verification with invariants and contracts
• CFML
• A formalization of programs in first-order logic with a discrete linear order
• A Coq library for internal verification of running-times
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Temporary read-only permissions for separation logic
• Verified characteristic formulae for CakeML
• An observationally complete program logic for imperative higher-order functions
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Cogent: uniqueness types and certifying compilation
• Characteristic formulae for the verification of imperative programs
• Why3 -- where programs meet provers
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• PML2: integrated program verification in ML
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• From program logics towards language logics
• On the relationship between Dijkstra monads and higher-order fixpoint logic
• SMLtoCoq: automated generation of Coq specifications and proof obligations from SML programs with contracts
• NuITP: accelerating the inductive verification of equational programs through symbolic simplification
• Inductive predicates via least fixpoints in higher-order separation logic

Describes a project that uses

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176951)