Fri 17 Jun 2022 16:30 - 16:50 at Macaw - Refinement Types Chair(s): Sorav Bansal

In recent years, researchers have explored component-based synthesis, which aims to automatically construct programs that operate by composing calls to existing APIs. However, prior work has not considered efficient synthesis of methods with side effects, e.g., web app methods that update a database. In this paper, we introduce RbSyn, a novel type- and effect-guided synthesis tool for Ruby. An RbSyn synthesis goal is specified as the type for the target method and a series of test cases it must pass. RbSyn works by recursively generating well-typed candidate method bodies whose write effects match the read effects of the test case assertions. After finding a set of candidates that separately satisfy each test, RbSyn synthesizes a solution that branches to execute the correct candidate code under the appropriate conditions. We formalize RbSyn on a core, object-oriented language λsyn and describe how the key ideas of the model are scaled-up in our implementation for Ruby. We evaluated RbSyn on 19 benchmarks, 12 of which come from popular, open-source Ruby apps. We found that RbSyn synthesizes correct solutions for all benchmarks, with 15 benchmarks synthesizing in under 9 seconds, while the slowest benchmark takes 83 seconds. Using observed reads to guide synthesize is effective: using type-guidance alone times out on 10 of 12 app benchmarks. We also found that using less precise effect annotations leads to worse synthesis performance. In summary, we believe type- and effect-guided synthesis is an important step forward in synthesis of effectful methods from test cases.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

15:30 - 16:50
Refinement TypesSIGPLAN Track at Macaw
Chair(s): Sorav Bansal IIT Delhi and CompilerAI Labs
15:30
20m
Talk
(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
SIGPLAN Track
Yiyun Liu University of Maryland at College Park, James Parker Galois, Inc., Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software Institute
15:50
20m
Talk
(PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
SIGPLAN Track
Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
Link to publication DOI Authorizer link Pre-print
16:10
20m
Talk
(POPL 2021) Data Flow Refinement Type Inference
SIGPLAN Track
Zvonimir Pavlinovic Google, USA, Yusen Su University of Waterloo, Thomas Wies New York University
16:30
20m
Talk
(PLDI 2021) RbSyn: type- and effect-guided program synthesis
SIGPLAN Track
Sankha Narayan Guria University of Maryland, College Park, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland
Link to publication DOI Authorizer link Pre-print