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.z alfons laarman com


Research Interests

Formal Methods: Verification, Model Checking and Concurrency Theory.
Parallel Computing: Algorithms, Data Structures, Multi-Core and Distributed Systems.
Software Engineering: Model Driven Engineering and Domain Specific Languages.

About

Phd Thesis

In April 2009, I started as PhD candiate at the Formal Methods and Tools group of the University of Twente under the guidance of Prof. Dr. Jaco van de Pol. Working on the parallelization of model checking, I developed and proved correct several parallel algorithms and concurrent data structures. I then succesfully combined these parallel solutions with: the automata-theoretic approach to LTL model checking, partial-order reduction, state compression, timed automata and symbolic exploration using BDDs. I implemented these approaches in the language-independent model checker LTSmin, demonstrating significant gains with respect to other state-of-the-art model checkers.

Currently, I work with DPhil Georg Weissenbacher, at the TU Vienna on the project Heisenbugs. In order to detect these bugs in software, we developed the Vienna verification Tool (VVT). VVT combines the powerful Property Directed Reachability algorithm with abstraction to generate invariants that imply the correctness of the software under verification. To support parallel software, we are currently extending VVT with dynamic reduction methods that prune redundant parallel interleavings.

News

Okt 12, 2016 Was awarded the Austrian FWF Lise Meitner grant for a 2-year research project!
Okt 11, 2016 Invited by Jesper Larsson Träff to talk on "Multi-Core SCC Decomposition" at TU Wien.
Okt 4, 2016 Invited by Aske Plaat to talk on "Multi-Core Model Checking" at Leiden University.
July 13, 2016 Right before my DMCD talk, the NWO called me to relay the news that I was awarded the VENI grant! A perfect timing, now I can announce the 3-year project in my talk.
July 13, 2016 Will give an invited talk on "Multi-Core Model Checking" at the Dutch Model Checking Day 2016.
July 7, 2016 Will give an invited talk on "IC3/PDR" at Passau University.
July 14, 2016 Kim Larsen invited me to talk on "Data structures for Multi-Core Model Checking" in Aalburg.
Apr 7, 2016 Wil give a talk on Vienna verification Tool at ETAPS in Eindhoven.
Nov 9, 2014 Will give a talk on Multi-Core Partial-Order Reduction at HVC 2014 in Haifa, Israel.
June 14, 2014 Invited by Ana Sokolova to talk on "Data structures and Algorithms for Multi-Core Model Checking" in Salzburg.
May 13, 2014 Joined Helmut Veith's FORSYTE group at the TU Vienna. Will work on the project Heisenbugs with Georg Weissenbacher.

May 9, 2014

PhD defence is scheduled at 9th of May 2014, right after the DMCD 2014.
.
Mar 14, 2014 Registration for the Dutch Model Checking Day 2014 (DMCD 2014) is open.
Nov 14, 2013 Will give an invited talk on "Scalable Multi-Core Model Checking" at the TU Vienna.
May 14, 2013 Gave a talk on "Livelock Detection" at NASA's FM' in Moffet Field, CA.
There is even a video this time (skip to 58:30).
Oct 5, 2012 Will give a talk on CNDFS at ATVA 2011 in India.
Sept 17, 2012 Will show some good experimental results in my talk on "SpinS" at PDMC 2012 in London.
July 14, 2011 Will give a talk on "Parallel Tree Compression" at SPIN 2011 in Salt Lake City.
June 7, 2011 Will give an invited talk for a general audiance at the CTIT Symposion in Enschede.
Apr 20, 2011 Will give a talk on "Multi-Core LTSmin" at NASA's FM symposium in Pasadena.
May 6, 2011 Will give a talk on "Multi-Core Nested Depth-First Search" at ATVA 2011 in Taipei.
May 6, 2011 Will give a talk on "Boosting Reachability Performance with Shared Hash Tables" at FMCAD 2010 in Lugano, Switzerland.
Apr 21, 2010 Will give an invited talk on "Parallel Model Checking" at the IPA Spring Days.

Tools

LTSmin A language-indepedent model checker that attacks the state-space explosion using various techniques, inter alia: symbolic exploration using BDDs, partial-order reduction, multi-core parallelism, distributed parallelism and state compression.
VVT The Vienna Verification Toolkit encodes LLVM bitcode, the intermediate format of the LLVM compiler, as a symbolic transition relation. It implements property directed Reachability (PDR), aka IC3, to construct invariants implying the verification property.
SpinS This is Promela frontend for LTSmin, which is implemented in Java and which generates efficient C code.
OGML Ontology Grounded MetaLanguage (OGML) is a metamodleing frame work that makes explicit the notion of instantiation. It employes a nested hierarchy to consistently represent instantiation accorss all levels of the metamodeling hierarchy.

Students

Vincent Bloemen Vincent wrote his master thesis on On-The-Fly Parallel Decomposition of Strongly Connected Components. His thesis was awarded the UTwente thesis award 2015/2016. We submitted his work to the PPOPP'16 conference. Robert E. Tarjan, the original inventor of the SCC algorithm that we parallelized, has improved his data structures to work with our algorithm. Vincent currently works as PhD candidate in the FMT group at UTwente.
Tom van Dijk Tom wrote his master thesis on The parallelization of binary decision diagram operations for model checking. We published his work at PDMC 2012 and AVOCS 2012. Tom currently works as postdoc in Armin Biere's' group at the Johannes Kepler University in Linz.
Steven van der Vegt For his bachelor thesis, Steven invented a concurrent version of Cleary's compact hash table. Together we proved his data structure correct and submitted a paper for the MEMICS conference. Steven subsequently went on his motorbike to present the work in Czech Republic.
Elwin Pater We published Elwin's work on Guard-based Partial Order Reduction at SPIN 2013 and STTT 2014.
Freark van der Berg Freark wrote his master thesis on Model Checking LLVM using LTSmin. We published his earlier work on SpinS at PDMC 2012. Freark currently works as PhD candidate in the FMT group at UTwente.
Simon de Vries Simon wrote his bachelor thesis on Growing Bonsai Trees.
Ronald Burgman Ronald wrote his master thesis on Partial-order reduction in a dynamic context.

Publications

2016

2015

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