Synthesizing imperative programs from examples guided by static analysis

DOI10.1007/978-3-319-66706-5_18MaRDI QIDQ5233251zbMATH OpenOpenAlexFDO

Authors Sunbeom So, Hakjoo Oh

Publication date 16 September 2019

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.06334

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We present a novel algorithm that synthesizes imperative programs for introductory programming courses. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our key idea is to combine enumerative program synthesis and static analysis, which aggressively prunes out a large search space while guaranteeing to find, if any, a correct solution. We have implemented our algorithm in a tool, called SIMPL, and evaluated it on 30 problems used in introductory programming courses. The results show that SIMPL is able to solve the benchmark problems in 6.6 seconds on average.

Recommendations

• From program verification to program synthesis
• Counterexample guided inductive synthesis modulo theories
• scientific article; zbMATH DE number 3960972
• Synthesis with abstract examples
• Example-directed synthesis: a type-theoretic interpretation

Cited in

(8)

• Automatic synthesis of data-flow analyzers
• Program synthesis using deduction-guided reinforcement learning
• Program boosting: program synthesis via crowd-sourcing
• Using program synthesis for program analysis
• scientific article; zbMATH DE number 4020482 (Why is no real title available?)
• Synthesizing Imperative Code from Answer Set Programming Specifications
• Component-based synthesis for complex APIs
• Counterexample guided inductive synthesis modulo theories

This page was built for publication: Synthesizing imperative programs from examples guided by static analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5233251)