Using program synthesis for program analysis

DOI10.1007/978-3-662-48899-7_34MaRDI QIDQ3460078zbMATH OpenOpenAlexFDO

Authors

Publication date 12 January 2016

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Abstract: In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the {it synthesis fragment}. Satisfiability of a formula in the synthesis fragment is decidable over finite domains; specifically the decision problem is NEXPTIME-complete. If a formula in this fragment is satisfiable, a solution consists of a satisfying assignment from the second order variables to emph{functions over finite domains}. To concretely find these solutions, we synthesise emph{programs} that compute the functions. Our program synthesis algorithm is complete for finite state programs, i.e. every emph{function} over finite domains is computed by some emph{program} that we can synthesise. We can therefore use our synthesiser as a decision procedure for the synthesis fragment of second-order logic, which in turn allows us to use it as a powerful backend for many program analysis tasks. To show the tractability of our approach, we evaluate the program synthesiser on several static analysis problems.

Recommendations

• Programmable program synthesis
• From program verification to program synthesis
• Synthesizing imperative programs from examples guided by static analysis
• Decidable synthesis of programs with uninterpreted functions
• Program synthesis using dual interpretation

Cited in

(8)

• Synthesising programs with non-trivial constants
• scientific article; zbMATH DE number 1203405 (Why is no real title available?)
• Decidable synthesis of programs with uninterpreted functions
• Automatic synthesis of logical models for order-sorted first-order theories
• A framework for combining analysis and verification
• Type-based parametric analysis of program families
• Automatic synthesis of data-flow analyzers
• On collecting semantics for program analysis

This page was built for publication: Using program synthesis for program analysis

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