System Verification Lab

Research Group

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.

The SVL research group focuses on reliable computing, parallel computing, and quantum computing. In the past, our team has pioneered parallel algorithms based on depth-first search, applying these techniques broadly to verify the correctness of software and hardware systems. In addition, we proposed a technique called divide & quantum, which enables small quantum computers to handle large problems, while preserving speedup, by using techniques from distributed computing.

In a recent breakthrough, we have leveraged powerful automated reasoning techniques for quantum circuit analysis and optimization. A key insight behind our advancements is a novel knowledge representation approach for quantum information. With this approach, we identified critical limitations in classical data structures for representing highly-entangled quantum states and operators. This is surprising, since such states not only arise in many applications, but the corresponding class of circuits (the so-called stabilizer or Clifford circuits) can also be efficiently simulated by classical computers.

To overcome these challenges, we introduced LIMDD, a new type of decision diagram which is based on the so-called stabilizer formalism that captures a ubiquitous subset of quantum states featuring high entanglement structure. In addition, we pioneered a model counting (#SAT) approach for quantum circuit analysis and optimization, which enables the use of powerful #SAT solvers for this new domain. These innovations significantly enhance the efficiency and scalability of quantum computing techniques with the goal of advancing towards quantum supremacy.

Publications

System Verification Lab

A knowledge compilation map for quantum information

Trade-offs between classical and quantum space using spooky pebbling

Enriching diagrams with algebraic operations

Automated reasoning in quantum circuit compilation

Optimizing Causal Interventions in Hybrid Bayesian Networks

Equivalence checking of quantum circuits by model counting

Optimizing Causal Interventions in Hybrid Bayesian Networks: A Discretization, Knowledge Compilation, and Heuristic Optimization Approach

Simulating quantum circuits by model counting

Compact Parallel Hash Tables on the GPU

Balancing Computational Cost and Accuracy in Inference of Continuous Bayesian Networks

Advancing Quantum Computing with Formal Methods

Disentangling the Gap Between Quantum and #SAT

Hybrid divide-and-conquer approach for tree search algorithms

A decision diagram operation for reachability

Efficient implementation of LIMDDs for quantum circuit simulation

ParaGnosis: A tool for parallel knowledge compilation

LIMDD: A decision diagram for simulation of quantum computing including stabilizer states

Incremental property directed reachability

Fast equivalence checking of quantum circuits of Clifford gates

Optimizing quantum space using spooky pebble games

Introduction to the special issue for SPIN 2021

The Power of Disjoint Support Decompositions in Decision Diagrams