Verification of Concurrent Software based on Partial-Order Semantics
Supervisors
Suitable for
Abstract
Description: A Boolean program is one where all variables are of Boolean type. In the context of formal verification of concurrent software, concurrent Boolean programs (CBPs) are generated by a process of abstracting the original program, in such a way that the original analysis problem reduces now to an equivalent problem on the CBP. The unfolding technique is a well studied verification method for another model of concurrency called Petri nets. Unfoldings represent the behaviour of a Petri net in a compact way, by means of a partial-order enriched with additional information. Not only this this representation is a theoretically neat one, but also very efficient for practical verification. The goal of the project is to apply the unfolding technique to the verification of CBPs, and compare with existing verification techniques for CBPs.
Prerequisites: suitable for students having followed the course "Computer-Aided Formal Verification"