Introduce native symbolic execution of concurrent code

This prototype gives a research application of SMT Kit at Oxford.
The tool uses C++11 language features such as trailing-return-types
and meta-programming to implement native symbolic execution of C++
code. We use partial orders (e.g. CAV'13) to find concurrency bugs
with SMT solvers.

The current implementation already supports all arithmetic types
but new features are underway including partial order models of
collection data types such as stacks and arrays.