Zero Overhead Runtime Monitoring

Runtime monitoring aims at ensuring program safety by monitoring the program's behaviour during execution and taking appropriate action before a program violates some property. Runtime monitoring is in particular important when an exhaustive formal verification fails. While the approach allows for a safe execution of programs, it may impose a significant runtime overhead. In this paper, we propose a novel technique combining verification and monitoring which incurs no overhead during runtime at all. The technique proceeds by using the inconclusive result of a verification run as the basis for transforming the program into one where all potential points of failure are replaced by HALT statements. The new program is safe by construction, behaviourally equivalent to the original program except for unsafe behaviour, and has the same performance characteristics.