A Hoare Logic with Regular Behavioral Specifications

TL;DR

This paper introduces a Hoare logic that incorporates regular expressions to specify and verify complex sequential behaviors in programs, enhancing expressiveness while maintaining proof automation.

Contribution

It extends Hoare logic with regular expressions for behavioral specifications, balancing expressiveness and automation, and demonstrates practical implementation with case studies.

Findings

Successfully verified email matcher and casino game steps

Balances expressiveness with proof automation

Prototype implementation integrated with verification tools

Abstract

We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences of events that arise during the execution. The idea is similar to session types or process-like behavioral contracts, two currently popular research directions. The approach presented here strikes a particular balance between expressiveness and proof automation, notably, it can capture interesting sequential behavior across multiple iterations of loops. The approach is modular and integrates well with autoactive deductive verification tools. We describe and demonstrate our prototype implementation in SecC using two case studies: A matcher for E-Mail addresses and a specification of the game steps in the VerifyThis Casino challenge.