Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. For this thesis, we take as a starting point a modular semantics for concurrent programming languages designed to support formal reasoning and verification called LAGC Semantics. LAGCs separate local program evaluation from global concurrency and scheduling. Locally, individual statements execute in an abstract/symbolic environment in the form of traces without committing to a particular scheduling policy. Globally, these local traces are composed and concretized, with predicates over the resulting global trace determining which executions are valid under a particular concurrency model. LAGC is currently only a theoretical framework and is lacking an implementation that makes the framework executable, which is the envisioned contribution of this thesis.
The implementation will include:
Declarative characterization of concurrency models through well-formedness predicates
Recommended courses