  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.
