en: [tImɒθiː bɜːʳk] or fr: [timɔte buʀk] (Tim, [tIm] or [tiːm]); email@example.com; c/o ENS, Paris...
My research focuses on rigorous approaches to modelling, programming, and verifying embedded control systems. My motivation is not formal techniques as an end in themselves, but rather as a means to clarify the principles behind and to better engineer embedded systems. I always try to work with practical examples, like the control system of a robotic wheelchair (a long time ago), an infrared sensor, a microkernel operating system (as part of a large group), a microprinter component, or a wireless routing protocol. Focusing on practice means working with programming languages that can be compiled and executed. Rigour mandates languages based on precise and tractable models. Finally, modelling and analyzing realistic programming languages, their compilers, and the applications created with them requires computer assistance, and ideally interactive theorem provers.
- Three weeks until the EMSOFT submission deadline.
- Talk in the Functional Programming group at Chalmers.
- Talk in the Formal Methods group at Chalmers.
- Talk at MODPROD 2015.
- Paper accepted at Compiler Construction 2015.
- Talk at SYNCHRON 2014.
- Sundials/ML, an OCaml interface to Sundials, is released.
- AODV invariant proof available in the AFP.
- Paper accepted at ATVA.