Automatic Deductive Verification of Event Sequence Properties

Safety-critical systems often require the verification of trace-based properties. Traditional state-based deductive verification is advantageous for scalable software verification as it modularizes the behavior of methods in pre- and postcondition contracts, but has limitations regarding the specification and verification of trace-based properties that happen during the execution of a method. In this paper, we focus on event sequence properties, where an event is a method call that happens under a certain condition. Our goal is to provide a lightweight specification and automatic verification mechanism for trace-based event sequence properties based on Java Dynamic Logic. Our approach is inherently state-based and can leverage the advantages of scalability and (semi-)automated tool support. We characterize event sequence properties in terms of predicates, extend the notion of Java Dynamic Logic states, and provide a sound calculus. We introduce a new update type to trace whether certain events happened during the symbolic execution of statements. We implement our extension of Java Dynamic Logic in the deductive verifier KeY and show the feasibility on examples extracted from the VerifyThis competition.