An Assertional Proof of the Stability and Correctness of Natural Mergesort

DOI10.1145/2814571zbMath1367.68080OpenAlexW2220441938MaRDI QIDQ5277907

Paqui Lucio, K. Rustan M. Leino

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2814571

zbMATH Keywords

verificationstabilitysortingtheorem provingformal methodssoftware engineeringDafnyNatural Mergesort

Mathematics Subject Classification ID

Searching and sorting (68P10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

An assertional proof of red-black trees using Dafny

Uses Software

• Coq
• Dafny
• Isabelle/HOL
• Why3
• Spec#
• z3
• VCC
• Boogie
• WhyML
• BVD
• AutoProof

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof pearl: A mechanized proof of GHC's mergesort
• Proof pearl: The KeY to correct and stable sorting
• Automating Induction with an SMT Solver
• Dafny: An Automatic Program Verifier for Functional Correctness
• Why3 — Where Programs Meet Provers

This page was built for publication: An Assertional Proof of the Stability and Correctness of Natural Mergesort