|Thesis abstract: |
An important phase of the software development cycle concerns the verification of the correct behaviours of software products.
Although most of software defects can be discovered through an accurate testing, formal methods, and in particular model checking,
can reasonably guarantee the absence of defects in software products according their specification.
However, such methods are generally computationally intensive and verification of complex software can be unfeasible.
Nevertheless software is continuously subjected to changes, which are particularly common in the new software development paradigms, like agile development.
We want to face this problem by developing techniques capable of incrementality, i.e., approaches which are able, when verifying a new version of an already verified program,
to reuse the intermediate results obtained during previous executions on older versions of the artifact to speed up the process.
Moreover, we want to develop techniques which can achieve incrementality by exploiting the syntactic structure of the program to be verified.
These techniques can exploit the structure of the artifact to be verified for limiting the portion of the new input that has to be re-analyzed.
This is performed at both syntactic and semantic level.
For the syntactic point of view, only a fraction of the new artifact is re-parsed.
Then, the results of the syntactic incrementality are used to obtain semantic incrementality by performing only the computations related to the changed part which thus need to be redone.