Efficient Verified Implementation of Introsort and Pdqsort

DOI10.1007/978-3-030-51054-1_18OpenAlexW3038320931MaRDI QIDQ5049010

Peter Lammich

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_18

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM

Uses Software

• Boost C++ Libraries
• Boost
• Quicksort
• Rust
• Archive Formal Proofs
• heapsort

Cites Work

• Unnamed Item
• Unnamed Item
• Proving JDK's dual pivot quicksort correct
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• Permission accounting in separation logic
• KeY: A Formal Method for Object-Oriented Systems
• Proof of a recursive program: Quicksort

This page was built for publication: Efficient Verified Implementation of Introsort and Pdqsort