Abstracting an Operational Semantics to Finite Automata

Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 defined by an equivalence class construction.
Original languageEnglish
Title of host publicationInformation and Communication Technologies in Education, Research, and Industrial Applications
Subtitle of host publication11th International Conference, ICTERI 2015, Lviv, Ukraine, May 14-16, 2015, Revised Selected Papers
PublisherSpringer
Pages109-123
Number of pages16
ISBN (Electronic)978-3-319-30246-1
ISBN (Print)978-3-319-30245-4
DOIs
Publication statusPublished - 12 May 2015

Publication series

NameCommunications in Computer and Information Science
PublisherSpringer International Publishing
Volume594
ISSN (Print)1865-0929

Fingerprint

Dive into the research topics of 'Abstracting an Operational Semantics to Finite Automata'. Together they form a unique fingerprint.

Cite this