From program verification to program synthesis

By S. Srivastava, Sumit Gulwani, Jeffrey S. Foster. ACM-SIGACT Symposium on Principles of Programming Languages, 2010

322 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/e5e079f02139c2baf5ca22466d82e58fc4e1c48f

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Code completion with statistical language models (2014, methodology): “Partial programs, or templates, have also been effectively used for synthesis of various problems including classic sequential algorithms [32], bit-ciphers [31], and concurrent algorithms [37].”
Program Synthesis Using Natural Language (2015, background): “Traditional program synthesis, synthesizing programs from complete specifications [18, 35, 51, 52], has not yet seen wide adoption due to the difficultly of writing such specifications and verifying the synthesized program satisfies this specification.”
Syntax-guided synthesis (2013, unknown): “Besides program sketching, a number of recent efforts such as synthesis of loop-free programs [5], synthesis of Excel macros from examples [6], program de-obfuscation [7], synthesis of protocols from the skeleton and example behaviors [8], synthesis of loop-bodies from pre/post conditions [9], integ”
The Sketching Approach to Program Synthesis (2009, methodology): “which aims to use techniques from program verification to synthesize complex algorithms from sketch-like skeletons [6].”
Synthesizing coupling proofs of differential privacy (2017, background): “[42] to find an inductive invariant and a coupling strategy.”
Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications (2018, methodology): “Nevertheless, there are a range of methods that rely on some form of SMT-based synthesis (Srivastava et al., 2010; Gulwani et al., 2010).”
Dimensions in program synthesis (2010, unknown): “We rather present a simplistic view; for more details, we refer the reader to work on template based program synthesis [69, 67, 71] and component based program synthesis [23, 33].”
Synthesis of loop-free programs (2011, unknown): “This theme of transforming a verifier into a synthesizer is also present in recent work [36, 34], where the focus is on synthesizing code fragements along with inductive invariants as first-order instantiations of user-provided templates.”
NLyze: interactive programming by natural language for spreadsheet data analysis and manipulation (2014, background): “The traditional view of program synthesis has been to synthesize programs from formal and complete specifications [27, 37].”
Automating string processing in spreadsheets using input-output examples (2011, unknown): “Logical reasoning techniques (such as those used in learning straight-line bit-vector programs from input-output examples [8], or loopy programs from logical specifications [19]) are not suited for various reasons: they are not as scalable (several minutes are acceptable for discovering a new bit-ve”
Automated feedback generation for introductory programming assignments (2012, methodology): “We use constraint-based synthesis technology [16, 37, 40] to efficiently search over this large space of programs.”
Genetic programming for Reverse Engineering (2013, unknown): “) [86] could be applied.”
Spreadsheet table transformations from examples (2011, background): “Program synthesis has traditionally been motivated by the need to synthesize non-trivial algorithms [11, 21, 22] or to discover tricky code-snippets [10, 23].”
Program sketching (2012, result): “[20], both of whom were influenced by our earlier work.”
Program Synthesis (2017, methodology): “On one extreme, we have invariant-based methods that generate constraints that faithfully assert that the program satisfies the given specification [133].”