Novel Automatic Solver for Program Analysis – SOPRANO

Modern societies crucially rely on digital infrastructures, and it
is becoming clear that high-quality software can be obtained only
with the help of proper software verification tools. Today most
major verification approaches rely on automatic external solvers.
These solvers, however, do not fill the current and future needs for
verification: lack of satisfying model generation, lack of
reasoning on difficult theories (e.g. floating-point arithmetic),
lack of extensibility for specific or new needs. The SOPRANO project
aims at solving these problems and preparing the next
generation of verification-oriented solvers by gathering experts
from academia and industry.

We will design a new framework for the
cooperation of solvers, focused on model generation and borrowing
principles from SMT (current standard) and CP (well-known in
optimization). Our main scientific and technical objectives are the following.
The first objective is to design a new collaboration framework for
solvers, centered around synthesis rather than satisfiability and
allowing cooperation beyond that of Nelson-Oppen while still
providing minimal interfaces with theoretical guarantees. The
second objective is to design new decision procedures for
industry-relevant and hard-to-solve theories. The third objective
is to implement these results in a new open-source platform. The
fourth objective is to ensure industrial-adequacy of the techniques
and tools developed through periodical evaluations
from the industrial partners.

Our main approach is to combine principles coming from both SMT
and CP. Roughly speaking, we seek to add to SMT the extensibility
of CP and its native handling of domains, and to CP the elegant
communication interfaces of SMT and its ability to reason over
formulas with complex boolean structures (conflict analysis) and
quantifiers. In a canonical SMT solver, the Boolean Theory enjoys
a privileged status. We want to explore how to break this
privileged status, in order to allow theory
solvers to contribute more directly to each part of the solving
process. For that, we will develop a notion of first-class domain
and first-class conflict analysis.
The major results of the project includes scientific,
technological, and industrial benefits.
The project has the potential to deliver significant breakthroughs
in automated solving and program analysis. The major
outcome will be a paradigm shift in the combination of automated
solvers, going beyond current standard cooperation frameworks in
terms of extensibility, model-synthesis abilities, and richness of
communication between theories.

The resulting solvers will be more widely applicable, easier to tune
for specific applications, and potentially more efficient, by
encompassing the best trade-offs from SMT and CP.

The major technological output will be the open-source platform
implementing the results, including the cooperation mechanism.

OCamlPro and AdaCore, the industrial partners, will take full
advantage of the project to improve their lines of products and
services. Finally, traditional industrial partners of CEA and
UPSud will directly benefit from improvements of the verification
tools of the project members.

The Consortium is composed of CEA (software verification tools and
CP solving), University of Paris-Sud (SMT solving and
floating-point theory), Inria Rennes (CP solving, floating-point theory),
OcamlPro (software editor and SMT solver developer),
Adacore (software solution for Ada programming language).