Abstracting an operational semantics to finite automata

There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction mapping from semantics to automata and proving a simulation property seems to be easy. This paper aims at identifying the reasons why simple proofs break, among them artifacts in the semantics that lead to stuttering steps in the simulation. We then present a semantics based on the zipper data structure, with a direct interpretation of evaluation as navigation in the syntax tree. The abstraction function is then trivial to define. The only difficulty resides in showing that the generated automaton is finite.
 

Online Copy

Online version on Arxiv

Conference version at ICTERI (2015)

Formal development on Bitbucket

BibTeX Entry

@inproceedings{baklanova15:_abstr_operat_seman_finit_autom,
  author    = {Nadezhda Baklanova and
               Wilmer Ricciotti and
               Jan{-}Georg Smaus and
               Martin Strecker},
  title     = {Abstracting an Operational Semantics to Finite Automata},
  booktitle = {Proceedings of the 11th International Conference on {ICT} in Education,
               Research and Industrial Applications: Integration, Harmonization and
               Knowledge Transfer, Lviv, Ukraine, May 14-16, 2015.},
  pages     = {354--365},
  year      = 2015,
  url       = {https://www.irit.fr/~Martin.Strecker/Publications/abstracting_op_sem_2014.html},
}