Alfons Laarman
My main research interests are formal verification, automated reasoning, quantum computing and parallel computing. Verification is crucial to ensure the correctness of digital systems, but it requires rigorous, formal approaches and compute power for automated reasoning. My research therefore is on parallel and quantum algorithms for speeding up verification and reasoning. In a mutually reinforcing way, I also investigate the use of automated reasoning to efficiently represent quantum information and analyze quantum computations. I implement the resulting algorithms and data structures in various software tools.
I lead the System Verification Lab (SVL) which is part of the Theory Cluster and the interdepartmental Applied Quantum Algorithms (aQa) institute.
Members:
Joon Hyung Lee (Postdoc)
Jan Martens (Postdoc)
Muhammad Osama (Postdoc)
Marc Farreras I Bartra (PhD candidate)
Jingyi Mei (PhD candidate)
Dimitrios Thanos (PhD candidate)
Sebastiaan Brand (PhD candidate)
Arend-Jan Quist (PhD candidate)
Alexandro Villoria Gonzalez (PhD candidate)
Steef Hegeman (PhD candidate)
Alumni:
Tim Coopmans (Postdoc, now assistant professor at TU Delft)
Lieuwe Vinkhuijzen (PhD candidate)
Hans Dieter Hiep (PhD candidate)
Giso Dal
See also Google Scholar.
- 2024
A knowledge compilation map for quantum information
arXiv preprint arXiv:2401.01322
Cite -
Trade-offs between classical and quantum space using spooky pebbling
arXiv preprint arXiv:2401.10579
Cite -
Enriching diagrams with algebraic operations
International Conference on Foundations of Software Science and Computation Structures
pp. 121–143
Cite -
Automated reasoning in quantum circuit compilation
International Symposium on Model Checking Software
pp. 106–134
Cite -
Optimizing Causal Interventions in Hybrid Bayesian Networks
Cite -
Equivalence checking of quantum circuits by model counting
International Joint Conference on Automated Reasoning
pp. 401–421
Cite -
Optimizing Causal Interventions in Hybrid Bayesian Networks: A Discretization, Knowledge Compilation, and Heuristic Optimization Approach
International Conference on Information Processing and Management of Uncertainty in Knowledge-Based Systems
pp. 245–256
Cite -
Simulating quantum circuits by model counting
International Conference on Computer Aided Verification
pp. 555–578
Cite -
Compact Parallel Hash Tables on the GPU
European Conference on Parallel Processing
pp. 226–241
Cite -
Balancing Computational Cost and Accuracy in Inference of Continuous Bayesian Networks
International Conference on Probabilistic Graphical Models
pp. 361–381
Cite -
Advancing Quantum Computing with Formal Methods
International Symposium on Formal Methods
pp. 420–446
Cite -
Disentangling the Gap Between Quantum and #SAT
International Colloquium on Theoretical Aspects of Computing
pp. 17–40
Cite - 2023
Hybrid divide-and-conquer approach for tree search algorithms
Quantum
7: pp. 959
Cite -
A decision diagram operation for reachability
Formal Methods
pp. 514–532
Cite -
Efficient implementation of LIMDDs for quantum circuit simulation
International Symposium on Model Checking Software
pp. 3–21
Cite -
ParaGnosis: A tool for parallel knowledge compilation
International Symposium on Model Checking Software
pp. 22–37
Cite -
LIMDD: A decision diagram for simulation of quantum computing including stabilizer states
Quantum
7: pp. 1108
Cite -
Incremental property directed reachability
International Conference on Formal Engineering Methods
pp. 208–227
Cite -
Fast equivalence checking of quantum circuits of Clifford gates
International Symposium on Automated Technology for Verification and Analysis
pp. 199–216
PDF
Cite -
Optimizing quantum space using spooky pebble games
International Conference on Reversible Computation
pp. 134–149
Cite -
Introduction to the special issue for SPIN 2021
International Journal on Software Tools for Technology Transfer
25: pp. 75–76
Cite - 2022
The Power of Disjoint Support Decompositions in Decision Diagrams
NASA Formal Methods Symposium
pp. 790–799
Cite - 2021
A compositional approach to probabilistic knowledge compilation
Int. J. Approx. Reason.
138: pp. 38–66
Cite - 2020
Symbolic Model Checking with Sentential Decision Diagrams
Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020
12153: pp. 124–142
Cite - 2019
-
A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings
11388: pp. 535–554
Cite - 2018
-
Stubborn Transaction Reduction
NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
10811: pp. 280–298
Cite -
Parallel Probabilistic Inference by Weighted Model Counting
International Conference on Probabilistic Graphical Models, PGM 2018
72: pp. 97–108
Cite -
Parallel Model Checking Algorithms for Linear-Time Temporal Logic
Handbook of Parallel Constraint Reasoning
pp. 457–507
Cite - 2017
Dynamic Reductions for Model Checking Concurrent Software
Verification, Model Checking, and Abstract Interpretation VMCAI 2017
10145: pp. 246–265
Cite - 2016
-
Multi-core on-the-fly SCC decomposition
Symposium on Principles and Practice of Parallel Programming, PPoPP 2016
pp. 8:1–8:12
Cite -
Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference TACAS 2016
9636: pp. 954–957
Cite - 2015
LTSmin: High-Performance Language-Independent Model Checking
Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015
9035: pp. 692–707
Cite - 2014
-
Partial-Order Reduction for Multi-core LTL Model Checking
Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings
8855: pp. 267–283
Cite - 2013
SpinS: Extending LTSmin with Promela through SpinJa
Electron. Notes Theor. Comput. Sci.
296: pp. 95–105
Cite -
Multi-Core BDD Operations for Symbolic Reachability
Electron. Notes Theor. Comput. Sci.
296: pp. 127–143
Cite -
Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction
Computer Aided Verification - 25th International Conference, CAV 2013
8044: pp. 968–983
Cite -
Improved on-the-Fly Livelock Detection
NASA Formal Methods, 5th International Symposium, NFM 2013
7871: pp. 32–47
Cite -
Guard-Based Partial-Order Reduction
Model Checking Software - 20th International Symposium, SPIN 2013
7976: pp. 227–245
Cite - 2012
Multi-core and/or Symbolic Model Checking
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
vol:53
Cite -
Improved Multi-Core Nested Depth-First Search
Automated Technology for Verification and Analysis ATVA 2012
7561: pp. 269–283
Cite -
Multi-core Reachability for Timed Automata
Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012
7595: pp. 91–106
Cite - 2011
Multi-core Nested Depth-First Search
Automated Technology for Verification and Analysis ATVA 2011
6996: pp. 321–335
Cite -
A Parallel Compact Hash Table
Mathematical and Engineering Methods in Computer Science MEMICS 2011
7119: pp. 191–204
Cite -
Multi-Core LTSmin: Marrying Modularity and Scalability
NASA Formal Methods - Third International Symposium, NFM 2011
6617: pp. 506–511
Cite -
Parallel Recursive State Compression for Free
Model Checking Software, SPIN 2011
6823: pp. 38–56
Cite -
Variations on Multi-Core Nested Depth-First Search
Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011
72: pp. 13–28
Cite - 2010
Boosting multi-core reachability performance with shared hash tables
International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010
pp. 247–255
Cite - 2009
Ontological Metamodeling with Explicit Instantiation
Software Language Engineering, Second International Conference, SLE 2009
5969: pp. 174–183
Cite