# Topics

Students CAN pick a project which is NOT on this list.
In this task, you should verify a fixpoint theorem. Specifically, your proof
should mainly follow Bourbaki-Witt's proof skeleton and apply your theorem
to at least three denotational semantics.
Slot remaining: No.
In this task, you should verify a fixpoint theorem. Specifically, your proof
should mainly follow Knaster-Tarski's proof skeleton and apply your theorem
to at least one denotational semantics.
Slot remaining: No.
You should first prove a general theorem which can be used to prove
equivalence between two recursively defined semantics. Then, you need to prove
the equivalence among three recursively defined denotational semantics: the
normal one, the one with time, and the one with traces. In the end, you should
connect small step semantics with each of them.
Slot remaining: No.
In this task, you should establish a relation among one denotational
semantics and two small step semantics for programs with control flow.
We showed a simple programming language sample and their semantics in class.
You may add more commands like C-like switch and/or other loops.
Slot remaining: No.
In this task, you should establish a relation among the denotational
semantics and the Hoare logic for programs with control flow. We showed a
simple programming language sample and their semantics in class. You should
prove the logic sound and prove the logic complete under the expressiveness
assumption.
Slot remaining: No.
In this task, you should establish a relation between the denotational
semantics and the small step semantics for programs with function call.
We showed a simple programming language sample and their semantics in class.
You may add more features like function arguments and return values.
Slot remaining: No.
In this task, you should first prove a general theorem which can be used to
prove an equivalence between two recursively defined semantics for programs
with function calls. Then, you need to prove the equivalence among three
denotational program semantics.
Slot remaining: No.
In this task, you should establish a relation among the denotational
semantics and the Hoare logic for programs with function call. We showed a
simple programming language sample and their semantics in class. You should
prove the logic sound.
Slot remaining: No.
You should define a lambda calculus with reference and IO, including its
syntax, small step semantics and a next-state function. Then, you need to
prove that the next-state function and the small step semantics coincide.
In the end, you need to write a simple tactic to let it "run" some simple
program.
Slot remaining: No.
You should define an extension of Imp with addresses, fork and join,
including its syntax, small step semantics, a next-step function (based on a
scheduler). Then, you need to prove that the next-state function and the
small step semantics coincide. In the end, you need to write a simple tactic
to let it "run" some simple program.
Slot remaining: No.
Design a compiler optimization of expressions, which fold constants and
also takes addition and multiplication's commutativity, associativity, etc.
into consideration. Prove its correctness via denotational semantics.
Slot remaining: No.
Consider the constant folding function fold_constants_aexp we learnt in
class. We can easily extend it to bexp and com. You should define a
simulation relation and prove the program transformation correct via small
step semantics.
Slot remaining: No.
Consider the optimization which eliminates unused assignments. Your task is
to define a simulation relation and prove this optimization correct via
small step semantics.
Slot remaining: Yes.
Consider the optimization which eliminates unused assignments. Your task is
prove this optimization correct via denotational semantics.
Slot remaining: Yes.
You need to learn Strassenâ€™s algorithm for matrix multiplication (chapter
4.2 of Cormen's <<Introduction to Algorithms>>. You should find a
formalization of matrices (or define one by yourself), formalize the
Strassen algorithm and prove it functionally correct in Coq.
You only need to define this algorithm as a Coq function or a Coq relation.
You can define it denotationally or via small steps. You do not need to
implement it in a programming language like C. You do not need to verify its
implementation in any programming language.
Slot remaining: No.
You need to read Chapter 10.2, 10.3 and 10.3.1 of <<Parameterized
Algorithm>> by Marek Cygan. You should formalize the algorithm for coloring
counting using fast Mobius transformation. Its correctness is theorem 10.16
in the book. You should prove that algorithm's correctness in Coq.
You only need to define this algorithm as a Coq function or a Coq relation
(small step description of this algorithm). You do not need to implement it
in a programming language like C. You do not need to verify its
implementation in any programming language.
Slot remaining: No.
Discrete Fourier transformation can be used to compute big number's
multiplication. FFT is a well-known efficient algorithm to calculate
discrete fourier transformation. Your should learn how this algorithm works
and prove its correctness in Coq. You need to either define this algorithm
using complex numbers (you may find some library in Coq's standard library
or other Coq's user's contribution) or via an abstract ring with some extra
properties.
You only need to define this algorithm as a Coq function or a Coq relation
(small step description of this algorithm). You do not need to implement it
in a programming language like C. You do not need to verify its
implementation in any programming language.
Slot remaining: No.
Splay tree is a kind of self-balanced binary search tree. You may learn this
data structure from online resources like:
<<
https://people.eecs.berkeley.edu/~jrs/61b/lec/36
>>
In this task, you should prove the functional correctness of the splay
operation, the key operation of splay trees. We provide a step-wise
description of splay.
Slot remaining: No.
You should verify a doubly linked list library using VST. You may use
programs that we provided, or write those programs-to-verify by yourself.
This library should include the following functions and two extra
applications:
Slot remaining: No.
Splay tree is a kind of self-balanced binary search tree. You may learn this
data structure from online resources like:
<<
https://people.eecs.berkeley.edu/~jrs/61b/lec/36
>>
In this task, you should verify the implementation of the splay operation,
the key operation of splay trees. We provide a step-wise description of
splay and a C implementation example.
Slot remaining: No.
Details to be added.
Slot remaining: Yes.
Details to be added.
Slot remaining: Yes.
You should verify a red-black tree insertion using VST. You should verify
the program that we provide. You may change the definition below if your
version is better.
Hint: you need to learn how to use forward_loop in VST to reason about
a general loop.
Slot remaining: No.

# Bourbaki-Witt fixpoint theorem and its three applications

# Knaster-Tarski fixpoint theorem and one of its application

# Equivalence among 3 denotational semantics and small step semantics

# Small-steps vs. denotations for programs with break and continue

# Denotations vs. Hoare logic for programs with break and continue

# Small-steps vs. denotations for programs with function call

# Equivalence among 3 denotational semantics for programs with calls

# Denotations vs. Hoare logic for programs with function call

# Executable semantics for lambda calculus with reference and IO

# Executable semantics for programs with addresses, fork and join and IO

# Advanced constant folding correctness by denotation equivalence

# Constant folding correctness by simulation

# Unused assignment elimination correctness by simulation

# Unused assignment elimination correctness by denotation equivalence

# Algorithm correctness Strassenâ€™s algorithm for matrix multiplication

# Algorithm correctness of Mobius transformation

# Algorithm correctness of fast Fourier transform (FFT)

# Algorithm correctness of splay operation

# Implementation Correctness of doubly linked list via VST

struct node; struct list; struct node * begin(struct list * ); struct node * end(struct list * ); struct node * next(struct node * ); struct node * rbegin(struct list * ); struct node * rend(struct list * ); struct node * rnext(struct node * ); unsigned int get_val(struct node * ); void insert_before (struct list *, struct node *; unsigned int ) void insert_after (struct list *, struct node *; unsigned int )

# Implementation correctness of splay operation via VST

# Implementation correctness of splay-based operations via VST

# Implementation correctness of threaded BST via VST

# Implementation correctness of red-black tree insertion via VST

(* 2021-05-07 20:38 *)