Proving Quicksort Correct in Event-B

DOI10.1016/j.entcs.2009.12.017zbMath1342.68114OpenAlexW2031664756MaRDI QIDQ2994490

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)

Uses Software

• Rodin
• Quicksort
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verification of sequential and concurrent programs
• The derivation of systolic computations
• On the Purpose of Event-B Proof Obligations
• The B-Book
• Proof of a recursive program: Quicksort

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