Simpler proofs with decentralized invariants

DOI10.1016/j.jlamp.2021.100645OpenAlexW3127480495WikidataQ113870956 ScholiaQ113870956MaRDI QIDQ2043795

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)

Related Items (2)

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Formal study of functional orbits in finite domains
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Dafny: An Automatic Program Verifier for Functional Correctness
• Efficiency of a Good But Not Linear Set Union Algorithm
• Local Reasoning for Global Invariants, Part I

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