Alfons Laarman |
| Assistant Professor |
| Leiden University |
| Faculty of Science |
| The Leiden Institute of Advanced Computer Science (LIACS) |
| Theory group |
|
Snellius building, room 140 Niels Bohrweg 1 2333 CA, Leiden The Netherlands |
| λxyz. x@y.z alfons laarman com |
Research Interests
About
In April 2009, I started as PhD candidate 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 successfully 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.
Previously, I worked 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 extended VVT with dynamic reduction methods that prune redundant parallel interleavings.
In June 2017, I started as assistant professor at Leiden University.
News
| 1 Jun, 2017 | Looking for a PhD candidate on parallel algorithms and verification, mail me if interested. (A detailed job description will follow.) |
| 25 May, 2017 | Invited at PCR'17 to give a talk on parallel satisfiability. |
| Jan 16, 2017 | Will give a talk at VMCAI on Dynamic Reductions for Model Checking Concurrent Software. |
| 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 audience at the CTIT Symposium 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-independent 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 metamodeling frame work that makes explicit the notion of instantiation. It employs a nested hierarchy to consistently represent instantiation accross 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
2017
| bib | Günther, H., Laarman, A.W., Sokolova, A. and Weissenbacher, G.. (2017) Dynamic Reductions for Model Checking Concurrent Software. In: VMCAI 2017. LNCS. Springer. |
| slides | |
2016
| bib | Bloemen, V., Laarman, A.W. and van de Pol, J.C.. (2016) Multi-Core On-The-Fly SCC Decomposition. In: PPOPP 2016. IEEE. Springer. |
| bib | Günther, H., Laarman, A.W. and Weissenbasher, G.. (2016) Vienna Verification Tool: IC3 for Parallel Software (Competition Contribution). In: TACAS 2016. LNCS 9636. Springer. |
2015
| bib | Kant, G., Laarman, A.W., Meijer, J., van de Pol, J.C., Blom, S.C.C. and van Dijk, T. (2015) LTSmin: High-Performance, Language-Independent Model Checking. In: TACAS 2015. LNCS 9035. Springer. |
2014
| bib | Laarman, A.W., Pater, E., van de Pol, J.C. and Hansen, H., (2014/2015) Guard-based Partial-Order Reduction (extended version). STTT (accepted for publication). Springer. |
| bib | Laarman, A.W. and Wijs, A., (2014) Partial-Order Reduction for Multi-Core LTL Model Checking. In: HVC 2014. LNCS 8855. Springer. |
| slides | |
| bib | Laarman, A.W., (2014) Scalable Multi-Core Model Checking. PhD Thesis. 9 May 2014, University of Twente. |
| slides | |
2013
| bib | Laarman, A.W., Pater, E. and van de Pol, J.C. (2013) Guard-based Partial Order Reduction. In: SPIN 2013. LNCS 7976. Springer. |
| slides | |
| bib | 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: CAV 2013. LNCS 8044. Springer. |
| slides | |
| bib | Laarman, A.W. and Faragó, D. (2013) Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. In: NFM 2013. LNCS 7976. Springer. |
| slides | |
2012
| bib | van Dijk, T., Laarman, A.W. and van de Pol, J.C. (2012) Multi-core and/or Symbolic Model Checking. In: AVOCS 2012. ECEASST 53. EASST. |
| slides | |
| 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 | |
| bib | van Dijk, T., Laarman, A.W. and van de Pol, J.C. (2012) Multi-core BDD Operations for Symbolic Reachability. In: PDMC 2012. ENTCS 296. Elsevier. |
| slides | |
| 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 | |
| bib | 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: FORMATS 2012. LNCS Springer. |
| slides | |
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 | |
| 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 | |
| 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. |
| 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 | |
| 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 | |
| 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 | |
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 | |
| 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. |
2009
| bib | Laarman, A.W. and Kurtev, I. (2009) Ontological Metamodeling with Explicit Instantiation. In: SLE 2009. pp. 174-183. LNCS 5969. Springer. |
| bib | Laarman, A.W. (2009) An Ontology-Based Metalanguage with Explicit Instantiation. Master's thesis. 29 March 2009,. University of Twente. |
| slides | |
| 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 | |
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 | |