Simpler proofs with decentralized invariants

DOI10.1016/J.JLAMP.2021.100645OpenAlexW3127480495WikidataQ113870956 ScholiaQ113870956MaRDI QIDQ2043795FDOQ2043795

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

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

zbMATH Keywords

invariantsinductionautomated theorem proversdeductive verification

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Dafny: An Automatic Program Verifier for Functional Correctness
• Efficiency of a Good But Not Linear Set Union Algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Local Reasoning for Global Invariants, Part I

Cited In (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

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)