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
Maximilian Köhl: Most-Specific Verdictors for Imperfectly Observable Systems
The observable behavior of a system usually carries crucial information about its internal state, properties, and potential future behaviors. In this talk, I present a generic automata-theoretic synthesis approach to obtain most-specific verdicts from imperfect observations of an ongoing run of a system. Verdicts can be elements of any join-semilattice ordered by specificity. I show …continue reading
Bas Luttik: On the translation of pi-calculus into mCRL2
In [1], Rob van Glabbeek proved that there does not exist a compositional translation of pi-calculus into CCS that is valid up to strong barbed bisimilarity, but that there does exist a similarly valid compositional transition if the communication facility is of CCS is upgraded to ACP-style communication. In my talk, I will explore whether …continue reading