SYMBOLIC TEMPORAL VERIFICATION TECHNIQUES WITH EXTENDED REGULAR EXPRESSIONS

Abstract

Existing temporal verification approaches have sacrificed modularity to achieve automation or vice-versa. To exploit the best of both worlds, this thesis presents a new framework to ensure temporal properties via Hoare-style verifiers and term rewriting systems (TRSs), leading to a modular and compositional verification strategy, where functions can be replaced by their verified properties. We propose various effect logics as the temporal specifications, which are extended regular expressions (REs) and more flexible/expressive than the most deployed linear temporal logic (LTL). Furthermore, the proposed framework devises purely algebraic TRS to check the inclusions for the novel logic, avoiding the complex translation into automata.

This thesis demonstrates the applicability of the proposed framework and various REs-based temporal logics in different domains, such as synchronous programming, real-time systems, algebraic effects, etc. This thesis also presents the corresponding prototype systems, case studies, experimental results, and supporting proofs.