Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Concurrency Theory
Units: 24 units
Background
The Edinburgh Concurrency Workbench (CWB) is an automated tool which caters for the manipulation and analysis of concurrent systems. In particular, the CWB allows for various equivalence, preorder and model checking using a variety of different process semantics. For example, with the CWB it is possible to:
- define behaviours given either in an extended version of CCS [Milner] or in SCCS, and perform various analyses on these behaviours, such as analysing the state space of a given process, or checking various semantic equivalences and preorders;
- define propositions in a powerful modal logic and check whether a given process satisfies a specification formulated in this logic;
- play Stirling-style model-checking games to understand why a process does or does not satisfy a formula;
- derive automatically logical formulae which distinguish nonequivalent processes;
- interactively simulate the behaviour of an agent, thus guiding it through its state space in a controlled fashion.
The original CWB (latest version is 7.1) was implemented in Standard ML (SML) and (in theory) can still be built by Standard ML of New Jersey (SML/NJ), but it hasn’t been maintained for many years.
Research Questions and Tasks
This project is an opportunity for students who wants to learn the HOL4 theorem-proving system. The main aim here is to rescue/realise an important heritage software by porting its original source code to HOL4 (also written in SML). The underlying CCS datatype will be based on the existing CCS formalization found in HOL’s official examples [Chun]. While CWB outputs that two CCS agents are (strong or weak) bisimilar, the new implementation shall output the same result as a corresponding theorem, therefore is a verified implementaion of the bisimulation checking algorithms underlying CWB.
This will include the following tasks:
- Get the original CWB software built from source code and run normally (on Linux, e.g.) as a reference implementation;
- Port CWB source code from SML/NJ to Moscow ML and Poly/ML (the two SML implementations for building HOL4) and make it work in unverified way;
- Re-implement CWB using HOL’s existing CCS formalizations as underlying datatype and realise at least CWB’s existing strong and weak bisimulation checking algorithms in HOL, i.e. an verified implementation.
- Port CWB’s related examples also to HOL as unit tests.
The development should follow modern techniques and guidelines for HOL4, e.g. [HOLTutorial] and [HOL4]. Ideally, the project will be submitted to HOL4 official as part of its core theories.
NOTE: The student will get some basic training through a mini course to get familar with interactive theorem proving (ITP) techniques (and HOL4 in particular).
References
- [HOLTutorial] The HOL System LOGIC
- [HOL4] The HOL System DESCRIPTION
- [Milner] Milner, R.: Communication and Concurrency. Prentice Hall International Series in Computer Science (1989).
- [Chun] Tian, C., Sangiorgi, D.: Unique solutions of contractions, CCS, and their HOL formalisation. Inf. Comput. 275, 104606 (2020). doi:https://doi.org/10.1016/j.ic.2020.104606
Requirements:
Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; some programming experiences in ML language family (SML, OCaml, or even Haskell).