Abstract:
In this technical report the symbolic execution engine 'Mulib' will be outlined in its architecture, main algorithms, and design decisions. Mulib employs a rather new approach of program transformation (see Section 2) and thus, technical details on the implementation of such a system are thought to be insightful. Mulib first and foremost implements the runtime semantics of the Constraint-Logic Object-Oriented Programming (CLOOP) language Muli. Muli employs symbolic execution as a technique to, e.g., solve constraint-satisfaction problems and generate test cases.