System Verification Lab

LIMDD-sim is a parallel quantum circuit simulator based on local-invertable map decision diagrams (LIMDDs) developed by the SVL group in order to support Clifford circuits (and beyond) in decision diagams. Previous decision diagrams can become exponentially sized for certain stabilizer states (which are generated by Clifford circuits). In contrast, a LIMDD can represent any stabilizer state in quadratic size in the number of qubits, similar to stabilizer formalism by Gottesman and Aaronson. Moreover, LIMDDs are universal.

The LIMDD-sim implementation is a collaboration with Robert Wille's team from TUM. It is based on the simulator DDSim, which is part of Münich Quantum Toolkit.

Liptonizer is an LLVM transform pass that instruments parallel LLVM intermediate represenation (IR) code with information to establish transactions. These transactions can be executed atomically, limiting the number of costly interleavings when analyzing the program's behavior, while crucially preserving the program's original behavior (with respect to its assertions).

Liptonizer adds predefined tags to the IR to demark the beginning and end of atomic sections (transactions). The instrumentation also adds branches to enable dynamic transactions: Depending on the values of program variables, the transaction is sometimes extended or terminated earlier.

LTSmin is a language-independent high-performance model checker. It verifies correctness of real-time systems (timed automata), probabilistic systems (MAPA specifications), state machines (PROMELA and DVE), process algebras (mCRL2) and PropB. Properties can specified as invariants, LTL, CTL or modal mu-calculus.

LTSmin is based on a partitioned next-state interface (PINS), which enables semi-symbolic model checking, i.e., learning transition relations on-the-fly while executing the system through an interpreter. The semi-symbolic algorithms start with an empty transition relations in a decision diagram. By querying local (partitioned) transitions the relations are gradually learned. Due to locality, the learning process often only takes a small part of the verification time: Eventually the exploration of the system's behavior happens fully symbolically.

My team contributed many new features to the LTSmin implementation: a multi-core backend, parallel LTL algorithms, state compression, transaction reduction, timed automata, partial order reduction, support for sentential decision diagrams, a new saturation algortihm and support for Promela.

Q-Sylvan is a parallel quantum circuit simulator based on affine-algebraic decision diagrams (AADDs) developed by PhD candidate Sebastiaan Brand. The tool internally represents quantum states (and gates/sub-circuits) as decision diagrams. The benefit of these decision diagrams is that they often use much less memory than encoding the corresponding vectors and matrices as arrays. Circuits can be specified through a dedicated C interface or with in OpenQASM, an extension implemented by master student Martijn Swenne.

SigRefMC is a tool for computing the bisimulation reduction of a system symbolically. It is based on the SigRefMC developed in Twente by Tom van Dijk, but extended by master student Richard Huybers with a relational approach. We showed in a VMCAI publication that the relational approach is superior to the signature-based partition refinement (SigRef). To support the relational approach, Richard defined and implemented new decision diagram operations.

SpinS is a Promela frontend for the LTSmin model checker written in Java. It supports most Promela constructs and includes a large set of real-world Promela models. Because the resulting state counts in LTSmin is equal to those obtained by the SPIN model checker, the frontend enables a fair comparison between the two model checkers. Extensive experimentation shows that LTSmin saves memory, runtime and has better parallel scalability.

VVT is a SMT-based model checker that uses abstraction and refinement with property directed reachability (the CTIGAR algorithm). It verifies safety properties of systems in LLVM intermediate represenation. This means it supports any language that compiles to LLVM, such as C and C++. The tool competed in the Software Verification Competition (SVCOMP) 2016 and scored the fourth place in the concurrency category of SVCOMP, beaten only by BMC-based tools (which are unsound for programs with loops).

I contributed dynamic transaction reduction to VVT (see the Liptonizer tool). In contrast to static approaches, the dynamic approach can extend atomic sections based on local commutativity of program instructions. So even when the program-under-verificiation accesses global data ---read by other threads--- these instructions can sometimes still be aggregated into one transaction because of the current state of the program (for instance if all threads passed an initialization phase and subsequently only read global data).