In this presentation, I will recap the concepts of AuDaLa and give the design of a parallel sorting algorithm, Insertion Sort, which requires the use of write-write data races. I will prove this algorithm correct, during which I will discuss finding data races in AuDaLa, creating contracts for AuDaLa steps and basic lemmas to help …continue reading

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

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

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

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

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

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

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

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

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