Works:
- Towards the pervasive formal verification of multi-core operating systems and hypervisors implemented in C
- Instantiating uninterepreted functional units and memory system : functional verification of the VAMP
- TLB virtualization in the context of hypervisor verification
- On determinism versus non-determinism and related problems