Alfons Laarman

Researcher (postdoc)
Formal Methods in Systems Engineering (FORSYTE)
Institute for Information Systems 184/4
Faculty of Informatics
Technical University of Vienna
 
Favoritenstrasse 9-11
1040 Wien
Austria
 
λxyz x.y@ewi.z.nl a.w laarman utwente

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.

PhD: Multi-Core Model Checking

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.

Research Interests

Formal Methods, Verification, Logics and Model Checking.

(Parallel) Algorithms and Data Structures.

Software Engineering, Programming languages, Model Driven Engineering, DSLs, Model Transformation and Language Workbenches.

News

Publications

2014

bib Laarman, A.W., (2014) Scalable Multi-Core Model Checking. PhD Thesis. 9 May 2014, University of Twente.
slides
pdf

2013

2012

bib van der Berg, F.I. and Laarman, A.W. (2012) SpinS: Extending LTSmin with Promela through SpinJa. In: PDMC 2012. ENTCS 296. Elsevier.
slides
pdf
bib Evangelista, S., Laarman, A.W., Petrucci, L. and van de Pol, J.C. (2012) Improved Multi-Core Nested Depth-First Search. In: ATVA 2012. LNCS 7561. Springer.
slides
pdf

2011

bib Laarman, A.W. and van de Pol, J.C. (2011) Variations on Multi-Core Nested Depth-First Search. (Invited) In: PDMC 2011. pp. 13-28. ENTCS 72. EPTCS.
slides
pdf
bib Laarman, A.W., Langerak R., van de Pol, J.C., Weber, M. and Wijs, A. (2011) Multi-Core Nested Depth-First Search. In: ATVA 2011. pp. 321-335. LNCS 6996. Springer.
slides
pdf
  bib   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.
pdf
bib Laarman, A.W., van de Pol, J.C. and Weber, M. (2011) Multi-Core LTSmin: Marrying Modularity and Scalability. In: NFM 2011. pp. 506-511. LNCS 6617. Springer.
slides
pdf
bib Laarman, A.W., van de Pol, J.C. and Weber, M. (2011) Parallel Recursive State Compression for Free. In: SPIN 2011. pp. 38-56. LNCS 6823. Springer.
slides
pdf
bib van der Vegt, S. and Laarman, A.W. (2011) A Parallel Compact Hash Table. In: MEMICS 2011. pp. 191-204. LNCS 7119. Springer.
slides
pdf

2010

bib Laarman, A.W., van de Pol, J.C. and Weber, M. (2010) Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: FMCAD 2010, pp. 247-256. IEEE Computer Society.
slides
pdf
  bib   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.
pdf

2009

bib Laarman, A.W. and Kurtev, I. (2009) Ontological Metamodeling with Explicit Instantiation. In: SLE 2009. pp. 174-183. LNCS 5969. Springer.
slides
pdf
bib Laarman, A.W. (2009) An Ontology-Based Metalanguage with Explicit Instantiation. Master's thesis. 29 March 2009,. University of Twente.
slides
pdf
bib Laarman, A.W. (2009) Achieving QVTO & ATL Interoperability: An Experience Report on the Realization of a QVTO to ATL Compiler. In: MtATL 2009. pp. 119-133. CEUR Workshop Proceedings. Sun SITE Central Europe.
slides
pdf

2006

bib Laarman, A.W. (2006) Improving a Modular Verification Technique for Aspect Oriented Programming. In: TSCIT 2006. pp. 37-40. TSCIT 5. Twente University Press.
slides
pdf