Simpler proofs with decentralized invariants

DOI10.1016/J.JLAMP.2021.100645MaRDI QIDQ2043795zbMATH OpenOpenAlexWikidataFDO

Authors Jean-Christophe Filliâtre

Publication date 3 August 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-02518570/file/main.pdf

zbMATH Keywords

invariantsinductionautomated theorem proversdeductive verification

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Structural Invariants
• Model checking in bits and pieces
• Recursive proofs for inductive tree data-structures
• Computer Aided Verification
• Data abstraction: a general framework to handle program verification of data structures

Cites work

• scientific article; zbMATH DE number 3767009 (Why is no real title available?)
• scientific article; zbMATH DE number 1178976 (Why is no real title available?)
• Dafny: an automatic program verifier for functional correctness
• Efficiency of a Good But Not Linear Set Union Algorithm
• Formal study of functional orbits in finite domains
• Local reasoning for global invariants. I: Region logic
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

Cited in

(2)

• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• A tribute to José Manuel Valença

Describes a project that uses

Uses Software

• Dafny
• Why3
• z3
• VeriFast
• CVC4
• VACID-0

This page was built for publication: Simpler proofs with decentralized invariants

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