|Formal Methods & Tools|
|Computer Science (EWI)|
|University of Twente|
P.O. Box 217|
|λxyz firstname.lastname@example.org a.w laarman utwente|
In April 2009, I started as a PhD at the Formal Methods and Tools group, of the University of Twente (see for a project description: MCMC). Under the guidance of Prof. Dr. Jaco van de Pol, I work on solving the software verification problem more efficiently. As our society grows more dependent on software, it is critical that we guarantee its correct behavior. We solve this problem by employing more powerful parallel computers to comb through all possible sequences of operations of such safety-critical software, an approach called model checking. To implement our ideas in practice, we maintain our own language-independent model checker LTSmin.
My formal education is in Computer Science, with a specialization on Software Engineering and in particular Model Driven Engineering (MDE). My Master's thesis aimed at defing a uniform modeling architecture with an explicit notion of instantiation, grounded in ontology. The result is the metalanguage OGML. Currently, I argue for a stronger foundation for metamodeling in metamathematics. I believe that such a sound foundation will enable a synergy of the different modeling formalisms, improving their traceability and co-operability. This would enable a tue multi-lingual perspective on the whole software development cycle, as opposed to the poorly integrated set of tools and ad-hoc scripts that software developers currently use.
With my PhD project, I intend to parallelize the automata theoretic approach to model checking. My interests in this field are broad, and already I have (co)developed and proven correct several (parallel) algorithms and data structures for a diverse set of approaches to the model checking problem, among others: LTL model checking, partial-order reduction, parallel reachability, state compression, timed automata and symbolic exploration using BDDs.
I also have a strong interest in SAT/SMT-solving. From a practical perspective, I'm interested applying solvers for various subtasks of verification, for example, to derive better dependency/commutativity relations for partial-order reduction. From a theoretical perspective, I would like to exploit the logical foundations of to accommodate over-approximations in the solvers.