Verifying annotated program families using symbolic game semantics

DOI10.1016/J.TCS.2017.09.029MaRDI QIDQ1680558zbMATH OpenOpenAlexFDO

Authors Aleksandar 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Program verification using symbolic game semantics
• Family-based SPL model checking using parity games with variability
• Tools and Algorithms for the Construction and Analysis of Systems
• Family-based model checking with mCRL2
• Software model checking based on game semantics and CSP

Cites work

• scientific article; zbMATH DE number 7445154 (Why is no real title available?)
• An error-tolerant type system for variational lambda calculus
• CONCUR 2005 – Concurrency Theory
• Compositional Predicate Abstraction from Game Semantics
• Finding suitable variability abstractions for family-based analysis
• Foundations of Software Science and Computational Structures
• From transition systems to variability models and from lifted model checking back to \textsf{UPPAAL}
• Full abstraction for PCF
• Game semantic analysis of equivalence in IMJ
• On full abstraction for PCF: I, II and III
• Program verification using symbolic game semantics
• Static Analysis
• The regular-language semantics of second-order idealized ALGOL
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Variability encoding: from compile-time to load-time variability
• Variability-specific abstraction refinement for family-based model checking

Cited in

(3)

• Program verification using symbolic game semantics
• Finding suitable variability abstractions for lifted analysis
• Gamifying program analysis

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Verifying annotated program families using symbolic game semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1680558)