Proving Quicksort Correct in Event-B

DOI10.1016/J.ENTCS.2009.12.017MaRDI QIDQ2994490zbMATH OpenOpenAlexFDO

Authors Stefan Hallerstede

Publication date 1 August 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.12.017

zbMATH Keywords

refinementprogram verificationRodin tool

Mathematics Subject Classification ID

Searching and sorting (68P10)

Recommendations

• Quicksort revisited. Verifying alternative versions of quicksort
• scientific article; zbMATH DE number 7453193
• An intuitive and simple bounding argument for Quicksort
• Proving JDK's dual pivot quicksort correct
• A correctness proof of sorting by means of formal procedures
• A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
• Quicksort revisited
• Efficient Verified Implementation of Introsort and Pdqsort
• Extracting imperative programs from proofs: In-place Quicksort

Cites work

• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 2090152 (Why is no real title available?)
• scientific article; zbMATH DE number 2227867 (Why is no real title available?)
• Modeling in Event B. System and software engineering.
• On the Purpose of Event-B Proof Obligations
• Proof of a recursive program: Quicksort
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• The B-Book
• The derivation of systolic computations
• Verification of sequential and concurrent programs

Cited in

(5)

• Experiments in program verification using Event-B
• Qualitative Probabilistic Modelling in Event-B
• Modeling numerical programs with Event-B
• Automating Event-B invariant proofs by rippling and proof patching
• On the Purpose of Event-B Proof Obligations

Describes a project that uses

Uses Software

• Circus
• Quicksort
• Rodin

This page was built for publication: Proving Quicksort Correct in Event-B

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