Verifying annotated program families using symbolic game semantics

DOI10.1016/j.tcs.2017.09.029zbMath1380.68121OpenAlexW2762612122MaRDI QIDQ1680558

Aleksandar S. Dimovski

Publication date: 16 November 2017

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2017.09.029

zbMATH Keywords

algorithmic game semanticssymbolic automatamodel checking algorithmsprogram families

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Finding suitable variability abstractions for lifted analysis

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Program verification using symbolic game semantics
• Variability encoding: from compile-time to load-time variability
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• The regular-language semantics of second-order idealized ALGOL
• Finding suitable variability abstractions for family-based analysis
• Game Semantic Analysis of Equivalence in IMJ
• Compositional Predicate Abstraction from Game Semantics
• An error-tolerant type system for variational lambda calculus
• Variability-Specific Abstraction Refinement for Family-Based Model Checking
• From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL
• Tools and Algorithms for the Construction and Analysis of Systems
• Foundations of Software Science and Computational Structures
• Static Analysis
• CONCUR 2005 – Concurrency Theory
• Tools and Algorithms for the Construction and Analysis of Systems