CloSE - Cloud Solving Engine

The goal of this project is to explore the feasibility of a paradigm shift in the practice of program verification and analysis for industrially relevant programs, by reducing the impact of constraint solving techniques that currently represent a main bottleneck for verification approaches. Program verification and analysis techniques play an important role in software engineering, and have been extensively studied from the early seventies, mostly for proving program properties. They rely on constraint solving to prove the validity of formulas and conjectures generated during the verification. For example, symbolic techniques that are widely used in software engineering require simplifying and proving the validity of path conditions that are constraints on symbolic values, and indicate the conditions on the input values for executing a given set of paths. Both the recent improvements in processing resources and the wider set of applications of these techniques have raised new interests and expectations in program verification and analysis. Despite the spectacular advances in constraint solving techniques and the availability of mature solvers, constraint solving still represents a major bottleneck for program verification. The size of constraints grows quickly with the complexity of the program under analysis and may include hundreds of terms, thus impacting on the performance of the solvers. Many constraints may include terms of different nature, that may require different theories that work selectively on some terms and not others. As a consequence, many promising verification techniques, like many symbolic evaluation approaches, do not scale easily with the program size and the complexity of the terms that can occur in the conditions. This project proposes a new approach to constraint solving that can highly increase the scalability of program verification techniques. Our approach is based on the observation that the same or similar constraints may occur several times when dealing with many programs over time, and the constraints that must be evaluated in a given proof may have been already solved in previous proofs, and thus we can reuse previously saved proofs with a potentially big saving in time and effort. The success of the approach depends on the frequency of occurrence of the same or similar constraints and on the efficiency of the search of previous proofs.