A constraint-based approach to solving games on infinite graphs

DOI10.1145/2535838.2535860MaRDI QIDQ5408418zbMATH OpenOpenAlexFDO

Authors T. Beyene, Swarat Chaudhuri, Andrey Rybalchenko, C. Popeea

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2535838.2535860

zbMATH Keywords

gamesHorn clausesprogram synthesisproof rulesreactive synthesisstatic analysis

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10) 2-person games (91A05) Games involving graphs (91A43)

Recommendations

• On the synthesis of strategies in infinite games
• scientific article; zbMATH DE number 2077117
• Computer Aided Verification
• scientific article; zbMATH DE number 1863183
• Infinite games played on finite graphs

Cited in

(22)

• Solving quantified linear arithmetic by counterexample-guided instantiation
• \textsc{LTL} falsification in infinite-state systems
• An automaton learning approach to solving safety games over infinite graphs
• A symbolic algorithm for lazy synthesis of eager strategies
• Horn clause solvers for program verification
• Reachability games on automatic graphs
• Predicate abstraction for program verification
• Admissible Strategies in Infinite Games over Graphs
• A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies
• scientific article; zbMATH DE number 3961298 (Why is no real title available?)
• scientific article; zbMATH DE number 1953100 (Why is no real title available?)
• scientific article; zbMATH DE number 2024632 (Why is no real title available?)
• scientific article; zbMATH DE number 1863183 (Why is no real title available?)
• Computer Aided Verification
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Software Verification of Hyperproperties Beyond k-Safety
• Reasoning About Data Trees Using CHCs
• Realizability modulo theories
• On the complexity of multi-pushdown games
• Predicate abstraction for hyperliveness verification
• Causality-based game solving
• Learning union of integer hypercubes with queries (with applications to monadic decomposition)

Describes a project that uses

Uses Software

• LTL2BA
• z3
• HSF

This page was built for publication: A constraint-based approach to solving games on infinite graphs

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