This project contains analysis modules related to the eXtended Control Flow Automata (XCFA) formalism. Its main purpose is to enable the algorithms to operate over XCFA models.
The following analyses are available:
- Declarative: Handling multi-threaded programs using a declarative approach. See this paper for further information.
- Interleavings: Handling multi-threaded programs using an interleavings-based approach, i.e., discovering all relevant overlapping executions of the program. See this paper for further information.
- Singlethread: Only handling single-threaded programs encoded in the XCFA formalism. This is a reimplementation of the CFA analysis project here.