Algorithmic games for full ground references

DOI10.1007/s10703-017-0292-9zbMath1392.68147OpenAlexW2743782362WikidataQ59613817 ScholiaQ59613817MaRDI QIDQ1650867

Nikos Tzevelekos, Andrzej S. Murawski

Publication date: 16 July 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0292-9

zbMATH Keywords

full abstractiongame semanticsprogram equivalenceautomata over infinite alphabets

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Operationally-based program equivalence proofs using LCTRSs ⋮ Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts ⋮ On-the-fly bisimilarity checking for fresh-register automata

Uses Software

• eVolCheck
• SymDiff
• coneqct

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functions with local state: regularity and undecidability
• A new approach to abstract syntax with variable binding
• Context-free languages over infinite alphabets
• Correctness of data representations involving heap data structures
• Game-theoretic analysis of call-by-value computation
• A game semantics of names and pointers
• Regression Verification for Multi-threaded Programs
• Fragments of ML Decidable by Nested Data Class Memory Automata
• Algorithmic Nominal Game Semantics
• A Fragment of ML Decidable by Visibly Pushdown Automata
• Algorithmic Games for Full Ground References
• Full abstraction for nominal general references
• A Contextual Equivalence Checker for IMJ*
• Game Semantic Analysis of Equivalence in IMJ
• Visibly pushdown languages
• Full Abstraction for Reduced ML
• Deconstructing General References via Game Semantics
• The impact of higher-order state and control effects on local relational reasoning
• State-dependent representation independence
• eVolCheck: Incremental Upgrade Checker for C
• Small bisimulations for reasoning about higher-order imperative programs
• Typed Lambda Calculi and Applications

This page was built for publication: Algorithmic games for full ground references