Fri 12 Jan 2018 15:50 - 16:15 at Bunker Hill - Synthesis Chair(s): Nadia Polikarpova

Many problems in formal methods can be formalized as two-player games. For several applications, program synthesis for example, we are interested not just in the determining which player wins the game, but in computing a winning strategy for that player. This paper studies the strategy synthesis problem for games defined within the theory of linear rational arithmetic. Two types of games are considered. A satisfiability game is described by a quantified formula, and is played by two players that take turns instantiating quantifiers. The objective of each player is to prove (or disprove) satisfiability of the formula. A reachability game is described by a pair of formulas defining the legal moves of each player, and is played by two players that take turns choosing positions – rational vectors of some fixed dimension. The objective of each player is to reach a position where the opposing player has no legal moves (or to play the game forever). We give a complete algorithm for synthesizing winning strategies for satisfiability games and a sound (but necessarily incomplete) algorithm for synthesizing winning strategies for reachability games.

Fri 12 Jan

POPL-2018-papers
15:50 - 17:05: Research Papers - Synthesis at Bunker Hill
Chair(s): Nadia PolikarpovaUniversity of California, San Diego
POPL-2018-papers15:50 - 16:15
Talk
Azadeh FarzanUniversity of Toronto, Zachary KincaidPrinceton University
POPL-2018-papers16:15 - 16:40
Talk
Kartik ChandraStanford University, Rastislav BodikUniversity of Washington
POPL-2018-papers16:40 - 17:05
Talk
Xinyu WangUT Austin, Isil DilligUT Austin, Rishabh SinghMicrosoft Research