Alfons Laarman

Researcher (PhD)

P.O. Box 217
7500 AE
Enschede
The Netherlands

About

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.

Research Interests

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.

Publications

2013

Laarman, A.W., Pater, E. and van de Pol, J.C. (2013) Guard-based Partial Order Reduction. In: SPIN 2013, 8 July 2013, NY, USA. LNCS Springer. Accepted for publication.

Laarman, A.W., Olesen, M. Chr., Dalsgaard, A.E., Larsen, K.G. and van de Pol, J.C. (2013) Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction. In: Proceedings of the 25th International Conference on Computer Aided Verification, CAV 2013, 13-19 July 2013, Saint Petersburg, Russia. LNCS Springer. Accepted for publication.

Laarman, A.W. and Faragó, D. (2013) Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFS_FIFO. In: NASA Formal Methods, NFM 2013, 14-16 Sept 2013, California, USA. LNCS Springer. Accepted for publication.

2012

van Dijk, T., Laarman, A.W. and van de Pol, J.C. (2012) Multi-core and/or Symbolic Model Checking. In: Automated Verification of Critical Systems, AVOCS 2012, 18-20 Sept 2012, Bamberg, Germany. Electronic Communications of the EASST EASST.

van der Berg, F.I. and Laarman, A.W. (2012) SpinS: Extending LTSmin with Promela through SpinJa. In: Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, 17 Sept 2012, London, UK. Electronic Notes in Theoretical Computer Science Elsevier.

van Dijk, T., Laarman, A.W. and van de Pol, J.C. (2012) Multi-core BDD Operations for Symbolic Reachability. In: Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, 17 Sept 2012, London, UK. Electronic Notes in Theoretical Computer Science. Elsevier.

Evangelista, S., Laarman, A.W., Petrucci, L. and van de Pol, J.C. (2012) Improved Multi-Core Nested Depth-First Search. In: Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, 3-6 Oct 2012, Thiruvananthapuram (Trivandrum), Kerala. Lecture Notes in Computer Science Springer Verlag.

Dalsgaard, A.E., Laarman, A.W., Larsen, K.G., Olesen, M. Chr. and van de Pol, J.C. (2012) Multi-Core Reachability for Timed Automata. In: Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012, 18-20 Sep 2012, London, UK. Lecture Notes in Computer Science Springer Verlag.

2011

Laarman, A.W., Langerak R., van de Pol, J.C., Weber, M. and Wijs, A. (2011) Multi-Core Nested Depth-First Search. In: Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, 11-14 Oct 2011, Tapei, Taiwan. pp. 321-335. Lecture Notes in Computer Science 6996. Springer Verlag. ISBN 978-3-642-24372-1

Laarman, A.W. and van de Pol, J.C. (2011) Variations on Multi-Core Nested Depth-First Search. (Invited) In: Proceedings of the 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, 14 Jul 2011, Snowbird, Utah. pp. 13-28. Electronic Proceedings in Theoretical Computer Science 72. EPTCS. ISSN 2075-2180

Laarman, A.W., van de Pol, J.C. and Weber, M. (2011) Parallel Recursive State Compression for Free. Technical Report arXiv:1104.3119, ArXiv, Ithaca, NY. ISSN not assigned

Laarman, A.W., van de Pol, J.C. and Weber, M. (2011) Multi-Core LTSmin: Marrying Modularity and Scalability. In: Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, 18-20 Apr 2011, Pasadena, CA, USA. pp. 506-511. Lecture Notes in Computer Science 6617. Springer Verlag. ISSN 0302-9743 ISBN 978-3-642-20397-8

Laarman, A.W., van de Pol, J.C. and Weber, M. (2011) Parallel Recursive State Compression for Free. In: Proceedings of the 18th International SPIN Workshop, SPIN 2011, 14-15 Jul 2011, Snow Bird, Utah. pp. 38-56. Lecture Notes in Computer Science 6823. Springer Verlag. ISSN 0302-9743 ISBN 978-3-642-22305-1

van der Vegt, S. and Laarman, A.W. (2011) A Parallel Compact Hash Table. In: Proceedings of Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2011, 14-16 Oct 2011, Lednice, Czech Republic. pp. 191-204. Lecture Notes in Computer Science 7119. Springer Verlag. ISBN 978-3-642-25929-6
2010

Laarman, A.W. and Kurtev, I. (2010) Ontological Metamodeling with Explicit Instantiation. In: 2nd Int. Conf. on Software Language Engineering (SLE), 5-6 Oct 2009, Denver, CO, USA. pp. 174-183. LNCS 5969. Springer Verlag. ISBN 978-3-642-12106-7

Laarman, A.W., van de Pol, J.C. and Weber, M. (2010) Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, 20 Oct - 23 Oct 2010, Lugano, Switzerland. pp. 247-256. IEEE Computer Society. ISBN 978-1-4577-0734-6

Laarman, A.W., van de Pol, J.C. and Weber, M. (2010) Boosting Multi-Core Reachability Performance with Shared Hash Tables. Technical Report arXiv:1004.2772, ArXiv, Ithaca, NY.
2009

Laarman, A.W. (2009) An Ontology-Based Metalanguage with Explicit Instantiation. Master's thesis, University of Twente.

Laarman, A.W. (2009) Achieving QVTO & ATL Interoperability: An Experience Report on the Realization of a QVTO to ATL Compiler. In: 1st International Workshop on Model Transformation with ATL, MtATL 2009, 8-9 Jul 2009, Nantes, France. pp. 119-133. CEUR Workshop Proceedings. Sun SITE Central Europe. ISSN 1613-0073
2006

Laarman, A.W. (2006) Improving a Modular Verification Technique for Aspect Oriented Programming. In: 5th Twente Student Conference on Information Technology, 26 Jun 2006, Enschede, The Netherlands. pp. 37-40. Twente Student Conference on IT 5. Twente University Press. ISSN 1574-0293