## Flip van Spaendonck: Modelling Object-Oriented Code

In my previous colloquium talk, I gave a brief overview of how we automatically transform object-oriented C++ code into labeled transition systems using our novel State-Space Transformation & Generation tool (SSTraGen). In this talk, we skip the transformation step, and instead, take a more detailed look at the precise semantics used for capturing the various *…continue reading*

## Tim Willemse: On the minimisation of transition systems

There is a wealth of equivalence relations on labelled transition systems; see, e.g., Van Glabbeek’s linear-time branching-time spectrum. Some of these equivalences have found their way in tool sets such as mCRL2, where they are used either to compare two transition systems, or to reduce the size of a transition system. The latter is often *…continue reading*

## Matthias Volk: How to estimate software failure rates?

Calculating the reliability of safety-critical systems requires knowledge of the failure rates of individual system components. While failure rates for physical components are well understood, the estimation of failure rates for software components remains an open question. In this talk, we will discuss first ideas and possible steps towards estimating and predicting software failures using *…continue reading*

## Kevin Jilissen: Establishing well-typedness of SysML type definitions and activity diagrams

SysML is widely used in industry to model complex systems. The lack of formal semantics and the support for modeller-defined semantics result in little to no support from tooling to ensure the model is well-typed. In this presentation, semantics are introduced with inference rules using Scope Graphs which enable the establishment of well-typedness of tunnel *…continue reading*

## Jan Friso Groote: Rewriting with 64-bit digits in mCRL2

Rewriting of numbers is often done with the Peano rewrite rules, but this is terribly slow and cumbersome. In mCRL2 the standard built in numbers are based on a binary encoding, using constructors @c0 for zero and @cDub for duplication. This is much faster. But when many calculations are done, the manipulation of these binary *…continue reading*

## Jan Heemstra: Hardware accelerated intelligent theorem proving

We present a connection-based tableaux theorem prover that performs inferences entirely on the GPU. Benchmarks on the m40 dataset show it performs worse than other provers in terms of proving power. In terms of inferences per second, however, it is on par with or even surpasses state-of-the-art provers on similarly priced and dated hardware, despite *…continue reading*

## Simone Tini: Measuring Robustness in Cyber-Physical Systems under Sensor Attacks

We propose a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions,quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is with respect *…continue reading*

## Myrthe Spronck: Completeness Criteria in Modal mu-Calculus Formulae

When verifying liveness properties on transition systems, it is often necessary to discard spurious counterexamples. This can be done through the application of completeness criteria: assumptions on which paths represent realistic executions of the modelled system. To support verification of properties under completeness criteria, we have developed template modal mu-calculus formulae that can be instantiated *…continue reading*

## Jeroen Keiren: An Expressive Timed Modal Mu-Calculus for Timed Automata

In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such *…continue reading*

## Clemens Dubslaff: Explaining Control Strategies: Trees or Diagrams?

Decision trees (DTs) are widely used to represent control strategies, e.g., for machine learning classifiers or formal verification results. Decisions in DTs are based on expressive predicates, but they seem to not fully exploit their potential towards concise representations. One reason is in their tree structure, leading to isomorphic subtrees not being merged. Reduced ordered *…continue reading*