# Beyond-Regular Typestate

## TL;DR

This paper introduces Beyond-Regular Typestate (BR-Typestate), an extension of regular typestates capable of modeling non-regular properties in programs and protocols, with a formal system and a prototype typechecker.

## Contribution

It presents a new expressive typestate system, BR-Typestate, along with formal proofs of soundness and a prototype implementation for verifying complex properties.

## Key findings

- BR-Typestate can model non-regular properties
- Prototype typechecker verifies real-world properties
- System is proven sound and tractable

## Abstract

We present an extension for regular typestates, called Beyond- Regular Typestate(BR-Typestate), which is expressive enough to model non-regular properties of programs and protocols over data. We model the BR-Typestate system over a dependently typed, state based, impera- tive core language, and we prove its soundness and tractability. We have implemented a prototype typechecker for the language, and we show how several important, real world non-regular properties of programs and protocols can be verified.