Students CAN pick a project which is NOT on this list.

Bourbaki-Witt fixpoint theorem and its three applications

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.

Knaster-Tarski fixpoint theorem and one of its application

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.

Equivalence among 3 denotational semantics and small step semantics

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.

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

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.

Denotations vs. Hoare logic for programs with break and continue

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.

Small-steps vs. denotations for programs with function call

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.

Equivalence among 3 denotational semantics for programs with calls

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.

Denotations vs. Hoare logic for programs with function call

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.

Executable semantics for lambda calculus with reference and IO

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.

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

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.

Advanced constant folding correctness by denotation equivalence

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.

Constant folding correctness by simulation

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.

Unused assignment elimination correctness by simulation

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.

Unused assignment elimination correctness by denotation equivalence

Consider the optimization which eliminates unused assignments. Your task is prove this optimization correct via denotational semantics. Slot remaining: Yes.

Algorithm correctness Strassen’s algorithm for matrix multiplication

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.

Algorithm correctness of Mobius transformation

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.

Algorithm correctness of fast Fourier transform (FFT)

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.

Algorithm correctness of splay operation

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.

Implementation Correctness of doubly linked list via VST

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:

    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 )

Slot remaining: No.

Implementation correctness of splay operation via VST

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.

Implementation correctness of splay-based operations via VST

Details to be added. Slot remaining: Yes.

Implementation correctness of threaded BST via VST

Details to be added. Slot remaining: Yes.

Implementation correctness of red-black tree insertion via VST

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.