In the setting of model checking, the concept of symmetry reduction is quite straightforward; to obtain a reduced model, we can put symmetric states together. However, there are several nuances that have to be spelled out. Which structures are used to define our model? What is a state? And what precisely is a symmetry? The …continue reading

I present our work on modeling an autonomous driving controller system using Stark. We explore a range of traffic scenarios, from a simple case with two cars on a single lane to complex multi-lane environments with multiple vehicles. Throughout these scenarios, we specify robustness properties and formally verify safety guarantees. Finally, we leverage Stark to …continue reading

This talk is a continuation of the talk I gave at the FSA colloquium of 4 November 2021, where I showed how a system that consists of a collection of synchronously communicating automata can be learned in a compositional fashion. However, this requires a priori knowledge of the alphabet of each component, making the approach …continue reading

Nested quantifiers, such as ∀ int x, int y; 0 ≤ x < 5 ∧ 0 ≤ y < 3 ⇒ a[5y+x]>0, pose challenges for verification tools based on SMT solvers. An SMT solver cannot simply determine a[13]>0 using the quantifier, since it has trouble finding the correct values for x and y, in this …continue reading

Willemse and Wesselink extended the PBES solvers in the mCRL2 toolset to support extracting evidence (witnesses and counterexamples) in the form a subsystems of a labelled transition system. This extension requires adding additional information to the PBES. Stramaglia has previously shown a two-step approach to solving a PBES with additional information: we first solve its …continue reading

The Prinses Marijke Sluizen in Tiel form a part of the Dutch waterways connecting the river Rhine with the Amsterdam-Rijn kanaal, allowing intense ship traffic while protecting the hinterland against flooding when water in the Rhine is high. We made a behavioural model of a controller of this sluice complex including failure of sensors and …continue reading

During the past five years, we’ve been developing yet another implementation of Binary Decision Diagrams (BDDs). What sets our implementation apart from others is its non-recursive algorithms. This allows it to efficiently compute on BDDs larger than the RAM of your machine – this potentially pushes the limits of symbolic model checking. In this talk, …continue reading

In the context of geometric representations of spatial objects, we explore a modelchecking approach based on polyhedra. To this end we introduce the notion of a polyhedral poset model as counterpart of a polyhedron model endowed with so-called simplicial bisimilarity. The latter equivalence captures the the spatial logic SLCS-eta, which has in particular a path …continue reading

Analyzing configurable systems using formal techniques, such as feature causality [1], allows for further insights towards why certain configurations exhibit a particular effect. Typically, the valid configuration space is exponential with respect to the number of features, and thus optimizations on feature cause computation would be beneficial. In the previous talk, we have discussed some …continue reading

Knowledge compilation refers to translating a data structure into another one to enable better algorithmic properties for specific tasks. For instance, model counting (#SAT) and uniform random sampling are likely to be not efficiently solvable for formulas in conjunctive normal form (CNF). However, compiling a CNF into deterministic decompositional negation normal form (d-DNNF) enables an …continue reading