Specification Verification of Hoare's Quicksort Algorithm in CafeOBJ

Specification Verification of Hoare's Quicksort Algorithm in CafeOBJ

Kokichi Futatsugi
Date: 
2019/01/10 (Thu) 16:00 to 17:30
Place: 
IS Collaboration room 7
Group: 
Research Center for Software Verification

================================
Title:
Specification Verification of Hoare's Quicksort Algorithm
in CafeOBJ

by Kokichi Futatsugi (AIST/JAIST/NII)


Abstract:

Sorting is modeled as an operation on sequences of elements with an
order relation, and Hoare's quicksort algorithm is specified as a
transition system in CafeOBJ specification/verification system.  The
correctness of the sort algorithm is specified as a leads-to property
of the transition system, and a proof score is developed to prove the
property.

The proof score makes use of built-in search predicates extensively to
prove basic leads-to properties, which are formulated with transition
rules as inference rules for proving the target leads-to property
inductively.  The proof score developed has a potential to make proofs
of a wide variety of leads-to properties possible.
===================================

Contact
nao-aoki@jaist.ac.jp