Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an "off-the-shelf" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool.

<p> Constraint Handling Rules ( CHRs) are a high level language extension to introduce user-defined constraints into a host language. Application of CHRs to reformulate functional dependencies (FDs) in the Haskell type system gives us a more precise definition of this concept, and a better understanding of FD behavior. But to preserve the confluence and termination properties of CHRs generated from FDs, some restrictions on the syntax of FDs and type class definitions have been imposed which confines the expressiveness power of Haskell type system. </p> <p> In this thesis we use this problem as a motivation to find a solution for the confluence and non-termination problem in CHRs. We build a formal framework for CHRs and model their different aspects mathematically to study how non-confluence and non-termination happens. Based on this formalization we introduce prioritized CHRs as a solution for the confluence problem. To solve the non-termination problem, we propose a method to detect non-termination in the constraint solver. We define a repetition candidate as a special type of derivation and prove that a derivation having this property can cause non-terminating rule applications in the system. Finally we define a deduction tree structure for a set of rules that can be used to find all the possible repetition candidates for a set of constraint rules. </p> / Thesis / Master of Science (MSc)