Email Gateway (Aug 22 2022 at 18:58): Email Gateway (Aug 22 2022 at 18:58):From: Manuel Eberl <eberlm@in.tum.de>
There is another entry by Bohua:
Verifying Imperative Programs using Auto2
by Bohua Zhan
This entry contains the application of auto2 to verifying functional and
imperative programs. Algorithms and data structures that are verified
include linked lists, binary search trees, red-black trees, interval
trees, priority queue, quicksort, union-find, Dijkstra's algorithm, and
a sweep-line algorithm for detecting rectangle intersection. The
imperative verification is based on Imperative HOL and its separation
logic framework. A major goal of this work is to set up automation in
order to reduce the length of proof that the user needs to provide, both
for verifying functional programs and for working with separation logic.
https://www.isa-afp.org/entries/Auto2_Imperative_HOL.html
Cheers,
Manuel
Last updated: Apr 19 2024 at 12:27 UTC