@hackage qute0.1.0

This library provides formal semantics for the QBE intermediate language by providing modular monadic semantics implemented using an abstract monad. The package refers to this abstract monad as the Language.QBE.Simulator.State.Simulator monad. It provides several primitives that are used by the Language.QBE.Simulator to abstractly describe the semantics of QBE instructions. The Language.QBE.Simulator.State.Simulator can then be instantiated with concrete semantics. For example, the Language.QBE.Simulator.Default.State module provides an instantiation using a Control.Monad.State monad. This instantiation, and the Language.QBE.Simulator.State.Simulator itself, are parameterized over the representation of QBE instruction operand values.

To abstractly describe operations on values passed to QBE instructions, this library additionally provides an expression language abstraction in the Language.QBE.Simulator.Expression module. Further, an implementation of this expression language based on fixed-width integer values is available in the Language.QBE.Simulator.Default.Expression module.

A separate qute-symex package provides an implementation of the expression abstraction and the Language.QBE.Simulator.State.Simulator monad for formal reasoning about a software under test using symbolic execution. Similar dynamic software testing techniques can be implemented using this library. Additionally, there is some preliminary support for static analysis as well through the Language.QBE.Analysis.CFG module.

More information on the underlying idea and vision behind Qute is available in a separate paper.