Software 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
• Fast equivalence checking of quantum circuits of Clifford gates

  ATVA

  

  PDF

  

  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
• Model Checking Software - 27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings

  Lecture Notes in Computer Science
  vol:12864

  

  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
• Hybrid divide-and-conquer approach for tree search algorithms

  CoRR
  vol:abs/2007.07040

  

  Cite
• 2019

  Optimal compression of combinatorial state spaces

  Innov. Syst. Softw. Eng.
  15: pp. 235–251

  

  Cite
• 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
• Stubborn Transaction Reduction (with Proofs)

  CoRR
  vol:abs/1802.02685

  

  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

  Guard-based partial-order reduction

  Int. J. Softw. Tools Technol. Transf.
  18: pp. 427–448

  

  Cite
• 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
• Dynamic Reductions for Model Checking Concurrent Software

  CoRR
  vol:abs/1611.09318

  

  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

  Scalable multi-core model checking

  

  Cite
• 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
• Parallel Recursive State Compression for Free

  CoRR
  vol:abs/1104.3119

  

  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
• Boosting Multi-Core Reachability Performance with Shared Hash Tables

  CoRR
  vol:abs/1004.2772

  

  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