A constraint-based approach to solving games on infinite graphs

DOI10.1145/2535838.2535860zbMath1284.91009OpenAlexW2140673956MaRDI QIDQ5408418

Andrey Rybalchenko, Swarat Chaudhuri, Tewodros A. Beyene, Corneliu 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

Horn clausesstatic analysisgamesprogram synthesisreactive synthesisproof rules

Mathematics Subject Classification ID

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

Related Items

Causality-based game solving, Learning union of integer hypercubes with queries (with applications to monadic decomposition), Predicate Abstraction for Program Verification, Horn Clause Solvers for Program Verification, Solving quantified linear arithmetic by counterexample-guided instantiation, Local Search For Satisfiability Modulo Integer Arithmetic Theories, A symbolic algorithm for lazy synthesis of eager strategies, \textsc{LTL} falsification in infinite-state systems

Uses Software

• z3
• HSF
• LTL2BA