Projects (PS)

A Compiler for the Register Machine from Hell

In this project you will implement and verify a compiler for the Register Machine from Hell (RMfH).

BIGNAT - Specification and Verification

In this project you will build and verify an implementation for BIGNAT, an abstract data type representing natural numbers of arbitrary size.

Matching First-Order Terms - Soundness and Completeness

In this project you will implement and verify a matching algorithm.

Propositional Logic - Soundness and Completeness

In this project you will formally prove soundness and completeness of a specific set of natural deduction rules for propositional logic.

The Euclidean Algorithm - Inductively

In this project you will develop and verify an inductive specification of the Euclidean algorithm.

Tries

In this project you will implement and verify several functions on and variations of tries.

Tseitin Transformation - Verification and Optimization

In this project you will implement several transformations of propositional formulas into equisatisfiable CNFs and formally prove results about their complexity and that the resulting CNFs are indeed equisatisfiable to the original formula.

Projects by Yutaka Nagashima

More details on the projects mentioned during the guest lecture on April 3 are available here.