Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.
Tue 22 SepDisplayed time zone: (UTC) Coordinated Universal Time change
16:00 - 17:00 | |||
16:00 20mTalk | Synthesis of Infinite-State Systems with Random Behavior Research Papers Andreas Katis University of Minnesota, Grigory Fedyukovich Florida State University, Jeffrey Chen University of Minnesota, David Greve Collins Aerospace, Sanjai Rayadurgam University of Minnesota, Michael Whalen University of Minnesota | ||
16:20 20mTalk | Demystifying Loops in Smart Contracts Research Papers Benjamin Mariano University of Texas at Austin, Yanju Chen University of California, Santa Barbara, Yu Feng University of California, Santa Barbara, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, USA | ||
16:40 20mTalk | Patching as Translation: The Data and the Metaphor Research Papers Yangruibo Ding Columbia University, Baishakhi Ray Columbia University, USA, Prem Devanbu University of California, Vincent J. Hellendoorn Carnegie Mellon University DOI Pre-print |