Saturating sorting without sorts

DOI10.29007/RG9ZMaRDI QIDQ7025197zbMATH OpenFDO

Authors Pamina Georgiou, Márton Hajdu, Laura Kovács

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/RG9Z

zbMATH Keywords

automated inductive reasoningautomated reasoningautomated software verificationautomated theorem provingfirst-order theorem provingformal methodsrecursive programssorting algorithmssuperposition calculus

Mathematics Subject Classification ID

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

Cites work

• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
• Array Abstractions from Proofs
• Axiomatizing permutation equivalence
• Coming to terms with quantified reasoning
• Dafny: an automatic program verifier for functional correctness
• Efficient Verified Implementation of Introsort and Pdqsort
• Getting saturated with induction
• Ground joinability and connectedness in the superposition calculus
• Handbook of automated reasoning. In 2 vols
• Lifting abstract interpreters to quantified logical domains
• Proof of a recursive program: Quicksort
• Proving JDK's dual pivot quicksort correct
• Quicksort
• Quicksort revisited. Verifying alternative versions of quicksort
• The Isabelle Framework
• Why3 -- where programs meet provers

This page was built for publication: Saturating sorting without sorts

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