| dc.description.abstract | When analysing programs statically, one quickly runs into issues of too many states and too many transitions, which combine to make the state-space very large. Commutativity analysis is one strategy for reducing the state-space, by identifying pairs of transitions that result in the same state regardless of execution order. This thesis presents an investigation into the suitability of SMT solvers for determining the commutativity of methods in an active object language. ABS, as an active object language, has cooperative scheduling and strong encapsulation, which makes it possible to work with methods as atomic units. Analysis of these methods should be able to identify commuting methods and reduce the state space. Satisfiability Modulo Theories (SMT) solvers allow programmers to declare problems rather than constructing solutions themselves. Modern solvers are highly optimized for speed, and able to solve very complex problems. This makes their use very compelling as part of larger analyses. A new addition to the ABS compiler has been written to output a type checked syntax tree as JSON. A program has been developed in Haskell to take JSON from the ABS compiler and generate code for an SMT solver, and these all combine to determine whether methods within a class commute. We demonstrate how to leverage an SMT solver to find commuting methods in ABS, and conclude it to be a promising tool for this kind of analysis. | eng |