Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 16:00 - 16:20 at Kangaroo - Synthesis and Repair Chair(s): Shahar Maoz

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 Sep
Times are displayed in time zone: (UTC) Coordinated Universal Time

16:00 - 17:00: Synthesis and RepairResearch Papers at Kangaroo
Chair(s): Shahar MaozTel Aviv University, Israel
16:00 - 16:20
Synthesis of Infinite-State Systems with Random Behavior
Research Papers
Andreas KatisUniversity of Minnesota, Grigory FedyukovichFlorida State University, Jeffrey ChenUniversity of Minnesota, David GreveCollins Aerospace, Sanjai RayadurgamUniversity of Minnesota, Michael W. WhalenUniversity of Minnesota
16:20 - 16:40
Demystifying Loops in Smart Contracts
Research Papers
Benjamin MarianoUniversity of Texas at Austin, Yanju ChenUniversity of California, Santa Barbara, Yu FengUniversity of California, Santa Barbara, Shuvendu K. LahiriMicrosoft Research, Isil DilligUniversity of Texas at Austin, USA
16:40 - 17:00
Patching as Translation: The Data and the Metaphor
Research Papers
Yangruibo DingColumbia University, Baishakhi RayColumbia University, USA, Prem DevanbuUniversity of California, Vincent HellendoornCarnegie Mellon University
DOI Pre-print