From program verification to program synthesis

DOI10.1145/1706299.1706337zbMath1312.68068OpenAlexW2101432564MaRDI QIDQ5255085

Jeffrey S. Foster, Saurabh Srivastava, Sumit Gulwani

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706337

zbMATH Keywords

verificationproof-theoretic program synthesis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (23)

\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Synthesis of positive logic programs for checking a class of definitions with infinite quantification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ A theory of formal synthesis via inductive learning ⋮ Synthesizing Imperative Code from Answer Set Programming Specifications ⋮ Iterative genetic improvement: scaling stochastic program synthesis ⋮ The matrix reproved (verification pearl) ⋮ On the complexity of the quantified bit-vector arithmetic with binary encoding ⋮ Efficiently solving quantified bit-vector formulas ⋮ Unnamed Item ⋮ Algebra-based synthesis of loops and their invariants (invited paper) ⋮ Counterexample-Guided Model Synthesis ⋮ Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation ⋮ Defining behaviorizeable relations to enable inference in semi-automatic program synthesis ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Synthesis of sorting algorithms using multisets in \textit{Theorema} ⋮ Combining model finder and genetic programming into a general purpose automatic program synthesizer ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ ARMed SPHINCS ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers

This page was built for publication: From program verification to program synthesis