CAS 707 “Formal Specification Techniques” 2019: Candidates for Project-Presentations

Probabilistic Hoare Logic and EasyCrypt

https://www.easycrypt.info/trac/

Task: Explain pHL; explain EasyCrypt; sketch an example application

AFP entry: Verifying Imperative Programs using Auto2

by Bohua Zhan

Date: Tue, 22 Jan 2019 18:00:19 +0100

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.

Task: Explain/describe the framework and approach; implement and verify some procedures on doubly-linked and/or XOR-linked lists.

AFP entry about DOM: https://www.isa-afp.org/entries/Core_DOM.html

Date: Mon, 7 Jan 2019 15:14:42 +0000

A Formal Model of the Document Object Model by Achim D. Brucker and Michael Herzberg

In this AFP entry, we formalize the core of the Document Object Model (DOM). At its core, the DOM defines a tree-like data structure for representing documents in general and HTML documents in particular. It is the heart of any modern web browser. Formalizing the key concepts of the DOM is a prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of security concepts in modern web browsers. We present a formalization of the core DOM, with focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to verify the functional correctness of the most important functions defined in the DOM standard. Moreover, our formalization is 1) extensible, i.e., can be extended without the need of re-proving already proven properties and 2) executable, i.e., we can generate executable code from our specification.

Task: Describe and explain the formalisation; formulate an application.

VeriFast

https://people.cs.kuleuven.be/~bart.jacobs/verifast/

Task: Explain/describe the framework and approach; implement and verify some procedures on doubly-linked and/or XOR-linked lists.

AFP: A Reduction Theorem for Store Buffers
Read From Total Store Order to Sequential Consistency: A Practical Reduction Theorem by Ernie Cohen and Norbert Schirmer.

https://www.isa-afp.org/entries/Store_Buffer_Reduction.html