Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
16 Apr 2019 Tuesday, 10:00 AM to 11:30 AM
COM2 Level 2
Asynchronous interactions are ubiquitous in computing systems and complicate design and programming. Automatic construction of asynchronous programs from specifications ("synthesis") could ease the difficulty, but known methods are complex, and intractable in practice. This work develops substantially simpler synthesis methods. A direct, exponentially more compact automaton construction is formulated for the reduction of asynchronous to synchronous synthesis. Experiments with a prototype implementation of the new method demonstrate practical feasibility.
Furthermore, it is shown that for several useful classes of temporal properties, automaton-based methods can be avoided altogether and replaced with simpler Boolean constraint solving.
Suguman is a PhD candidate working with Prof. Moshe Y. Vardi at Rice University. She is currently working in the areas of program verification and program synthesis. This talk was presented last year at CAV 2018.