Beyond-Regular Typestate
Programming Languages
2017-02-28 v1
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.
Keywords
Cite
@article{arxiv.1702.08154,
title = {Beyond-Regular Typestate},
author = {Ashish Mishra and Y. N. Srikant},
journal= {arXiv preprint arXiv:1702.08154},
year = {2017}
}
Comments
submitted to CAV'17