Enhancing a Theorem Prover written in Haskell

A theorem prover “reasonEq” , written in Haskell, is currently under development. It is intended to support reasoning about the meaning and correctness of programs. It supports an easy to use proof style for predicate calculus known as “equational reasoning” – very similar to the kind of algebraic reasoning used in most mathematics found in … Read more

Expanding Transactional Programming

[Available] Develop a library for simplifying the development of concurrent programs. Transactions have greatly simplified how database programs are constructed. Communicating transactions aim to do the same for programs that require some kind of concurrent consensus. Communicating transactions have been developed as a language feature that can extend concurrent programming languages. However a (limited) version of this construct may also … Read more

Automata Inference

[Multiple Projects Available] Automata inference/Automata learning. A Project in this area may explore algorithms that infer finite state automata out of a number of traces, with a view to be used as a verification tool. For example such a tool can verify whether a software process implements a particular protocol.┬áThere are already a number of … Read more

Program Equivalence Algorithms and Tools

[Multiple Projects Available] Explore and implement program equivalence algorithms and tools. Systems often comprise multiple concurrent processes which exchange messages over channels. Correctness of these systems is often described in terms of equivalence to another, prototype system (the spec). One particularly powerful notion of equivalence between such systems is bisimulation. Projects in this area may explore, … Read more

Verification of Concurrent Programs

[Multiple Projects Available] Verification of concurrent Golang programs using Uppaal tool:  Projects in this area may build upon an existing prototype framework/tool to (1) build a database of concurrency bugs which have already been identified and fixed in open source go repositories and use the framework to verify their fixes; (2) search for unknown bugs in … Read more