Program verification using symbolic game semantics

DOI10.1016/J.TCS.2014.01.016MaRDI QIDQ477213zbMATH OpenOpenAlexFDO

Authors Aleksandar Dimovski

Publication date 2 December 2014

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

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

zbMATH Keywords

program verificationpredicate abstractionalgorithmic game semanticssymbolic automata

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

• scientific article; zbMATH DE number 7340142
• Verifying annotated program families using symbolic game semantics
• Tools and Algorithms for the Construction and Analysis of Systems
• Algorithmic nominal game semantics
• scientific article; zbMATH DE number 2110612

Cites work

• scientific article; zbMATH DE number 3735091 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 1759637 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• scientific article; zbMATH DE number 7340142 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• CONCUR 2005 – Concurrency Theory
• Compositional Predicate Abstraction from Game Semantics
• Formal Program Verification Using Symbolic Execution
• Foundations of Software Science and Computation Structures
• On full abstraction for PCF: I, II and III
• Static Analysis
• Symbolic bisimulations
• The regular-language semantics of second-order idealized ALGOL
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

• Finding suitable variability abstractions for lifted analysis
• Verifying annotated program families using symbolic game semantics
• From bounded checking to verification of equivalence via symbolic up-to techniques
• State separation for code-based game-playing proofs
• scientific article; zbMATH DE number 7445154 (Why is no real title available?)
• Static Analysis
• scientific article; zbMATH DE number 7340142 (Why is no real title available?)
• Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting

This page was built for publication: Program verification using symbolic game semantics

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