2014/09/17 by Cristina David, Daniel Kroening, David, Cristina +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques #cs.LO
paper · pdf · doi:10.48550/arxiv.1409.4925
19 pages
openalex publication_date 2014/09/17 · arxiv created 2015/01/17 · arxiv updated 2015/01/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentially, the heuristic reduces a second-order problem to a first-order/propositional one, while the validation is often just a call to a SAT/SMT solver. This results in a monolithic design of such analyses that conflates the formulation of the problem with the solving process. Consequently, any change to the latter causes changes to the whole analysis. This design is dictated by the state of the art in solver technology. While SAT/SMT solvers have experienced tremendous progress, there are barely any second-order solvers. This paper takes a step towards addressing this situation by proposing a decidable fragment of second-order logic that is still expressive enough to capture numerous program analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We refer to the satisfiability problem for this fragment as Second-Order SAT and show it is NEXPTIME-complete. Finally, we build a decision procedure for Second-Order SAT based on program synthesis and present experimental evidence that our approach is tractable for program analysis problems.