Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Imperfect and Timed Systems

Imperfect and Timed Systems

Verification often relies on idealized assumptions about systems, like 100% uptime of a network, that do not hold in practice and therefore invalidate verification results. We developed a model that captures the imperfection of systems but yet allows for hard verification results. The idea is to work with safe thresholds on the system availability.


Roland Meyer



DFG: Automatic Verification and Analysis of Complex Systems (SFB AVACS)