Room 423, Wolfson Building, Parks Road, Oxford OX1 3QD
My research interests cover the areas of hardware design and formal verification, computer architecture, verification
of (on-chip) communication protocols/architectures, model checking, and theorem proving.
I am focusing on verified on-chip communication protocols for multicore/SoC architectures, my PhD project. The main goals
include the development of a generic framework for incremental model derivation and formal verification, and the application
of this framework to industrial-scale case studies, such as the ARM AMBA high-performance bus protocol and the PCI Express
protocol.The work is formalised using higher order logic and the Isabelle theorem prover.
Previous work includes
digital circuit design and formal verification of scheduling correctness for an automotive communication system.
I am currently a PhD student at the University of Oxford. My research focuses on verified on-chip communication protocols
for high-performance multicore or System-on-Chip architectures. The project is sponsored by the Engineering and Physical Sciences
Research Council (EPSRC) and the Intel Corporation.
Before joining the verification group in Oxford, I obtained
my M.Sc (Honour's Degree) in Computer Science at Saarland University, Germany at the chair for Computer Architecture and Parallel
Computing of Prof. Wolfgang Paul.
A Framework for Incremental Modelling and Verification of On−Chip Protocols
Proceedings of the Tenth Conference on Formal Methods in Computer Aided Design (FMCAD'10).
8 pages‚ to appear
Details | BibTeX
Incremental and Verified Modelling of the PCI Express Protocol
In IEEE Transactions on Computer−aided Design of Integrated Circuits and Systems.
14 pages‚ to appear
Details | BibTeX
A Refinement Approach to Design and Verification of On−Chip Communication Protocols
Peter Böhm and Tom Melham
Proceedings of the Eighth Conference on Formal Methods in Computer−Aided Design (FMCAD'08).
IEEE Computer Society.
Details | BibTeX |