Proving Quicksort Correct in Event-B

DOI10.1016/J.ENTCS.2009.12.017zbMATH Open1342.68114OpenAlexW2031664756MaRDI QIDQ2994490FDOQ2994490

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

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

zbMATH Keywords

refinementprogram verificationRodin tool

Mathematics Subject Classification ID

Searching and sorting (68P10)

Cites Work

• Proof of a recursive program: Quicksort
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modeling in Event B. System and software engineering.
• The B-Book
• On the Purpose of Event-B Proof Obligations
• Title not available (Why is that?)
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Title not available (Why is that?)
• Verification of sequential and concurrent programs
• The derivation of systolic computations

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

Uses Software

• Rodin
• Quicksort
• Circus

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)