2015/08/31 by Cristina David, Daniel Kroening, David, Cristina +3
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #Software Engineering Research #Software Reliability and Analysis Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1508.07829
openalex publication_date 2015/08/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 functions over finite domains. To concretely find these solutions, we synthesise programs that compute the functions. Our program synthesis algorithm is complete for finite state programs, i.e. every function over finite domains is computed by some 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.