Abstracting an operational semantics to finite automata

Autor: Nadezhda Baklanova, Martin Strecker, Wilmer Ricciotti, Jan-Georg Smaus
Přispěvatelé: Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Centre National de la Recherche Scientifique - CNRS (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Institut National Polytechnique de Toulouse - INPT (FRANCE)
Jazyk: angličtina
Rok vydání: 2014
Předmět:
FOS: Computer and information sciences
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR]
Theoretical computer science
Computer science
Formal semantics (linguistics)
02 engineering and technology
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
computer.software_genre
Interface homme-machine
Operational semantics
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Denotational semantics
Architectures Matérielles
Computer Science::Logic in Computer Science
0202 electrical engineering
electronic engineering
information engineering
Génie logiciel
Programming language semantics
[INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC]
Failure semantics
Computer Science - Programming Languages
Programming language
Formal methods
Verification
020207 software engineering
16. Peace & justice
Type erasure
Modélisation et simulation
Systèmes embarqués
[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation
Action semantics
Well-founded semantics
Computational semantics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Cryptographie et sécurité
Computer Science::Programming Languages
020201 artificial intelligence & image processing
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems
Abstraction
computer
Finite automata
Programming Languages (cs.PL)
Zdroj: Information and Communication Technologies in Education, Research, and Industrial Applications-11th International Conference, ICTERI 2015, Lviv, Ukraine, May 14-16, 2015, Revised Selected Papers
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015)
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), May 2015, Lviv, Ukraine. pp.109-123, ⟨10.1007/978-3-319-30246-1_7⟩
Information and Communication Technologies in Education, Research, and Industrial Applications ISBN: 9783319302454
ICTERI
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: