System Verification Lab
The System Verification Lab (SVL) is part of the Leiden Intitute for Advanced Computer Science (LIACS) and a partner in the Applied Quantum Algorithms (aQa) initiative.
SVL develops verification techniques for the engineering of safe and secure systems. Verification is crucial to ensure the correctness of digital systems. However, it requires rigorous and formal automate reasoning algortihms, which need ample computing resources. SVL tackles this challenge by using the resources of parallel and quantum computings. We implement the resulting algorithms and data structures in various software tools.
Publications
- 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
Model Checking Software: SPIN Symposium
Cite -
Optimizing Quantum Space using Spooky Pebble Games
Reversible Computing
Cite -
Introduction to the special issue for SPIN 2021
International Journal on Software Tools for Technology Transfer
25: pp. 75–76
Cite -
Model Checking Software
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 -
LIMDD A Decision Diagram for Simulation of Quantum Computing Including Stabilizer States
CoRR
vol:abs/2108.00931
PDF
Cite - 2020
Symbolic Model Checking with Sentential Decision Diagrams
Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings
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
Optimal Storage of Combinatorial State Spaces
NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
10811: pp. 261–279
Cite -
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, 11-14 September 2018, Prague, Czech Republic
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 - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings
10145: pp. 246–265
Cite - 2016
-
Multi-core on-the-fly SCC decomposition
Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 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, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
9636: pp. 954–957
Cite - 2015
LTSmin: High-Performance Language-Independent Model Checking
Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings
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, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
8044: pp. 968–983
Cite -
Improved on-the-Fly Livelock Detection
NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings
7871: pp. 32–47
Cite -
Guard-Based Partial-Order Reduction
Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings
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 - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings
7561: pp. 269–283
Cite -
Multi-core Reachability for Timed Automata
Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings
7595: pp. 91–106
Cite - 2011
Multi-core Nested Depth-First Search
Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings
6996: pp. 321–335
Cite -
A Parallel Compact Hash Table
Mathematical and Engineering Methods in Computer Science - 7th International Doctoral Workshop, MEMICS 2011, Lednice, Czech Republic, October 14-16, 2011, Revised Selected Papers
7119: pp. 191–204
Cite -
Multi-Core LTSmin: Marrying Modularity and Scalability
NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
6617: pp. 506–511
Cite -
Parallel Recursive State Compression for Free
Model Checking Software - 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings
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, Snowbird, Utah, USA, July 14, 2011
72: pp. 13–28
Cite - 2010
Boosting multi-core reachability performance with shared hash tables
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23
pp. 247–255
Cite - 2009
Ontological Metamodeling with Explicit Instantiation
Software Language Engineering, Second International Conference, SLE 2009, Denver, CO, USA, October 5-6, 2009, Revised Selected Papers
5969: pp. 174–183
Cite