Event Category: Colloquium

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

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

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

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

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