Back to homepage utwente.nl
Eduardo Zambon
Graphs for Abstract Interpretation of Languages
Description of research
As more and more systems in our everyday environment contain major software parts, and we are depending on such systems more and more (we are counting on them), the importance of the dependability of the software is increasing. Unfortunately, there are still very few generally applicable methods for software verification, i.e., the ensurance of its correct functioning under all circumstances. Reasons for this are, one the one hand, the degree of expertise necessary for existing verification methods, and on the other, their poor embedding in the average software development trajectory. An important practical objection is, moreover, that current verification methods typically assume the existence of a sufficiently detailed and precise model of system behaviour. In practice such models hardly ever exist, and the time and expertise to construct them are missing. Therefore, examples of methods that are being used widely in practice are typing and testing, neither of which necessarily depends on the existence of models.
In this project we investigate a new way of automatically verifying software on the basis of code, without assuming a predefined model. The technique used is static analysis, a general principle that encompasses typing; the new aspect is the use of graph transformations to capture the effect of the software. Graphs offer a natural model for the behaviour of dynamic software systems, and at the same time offer the basis for a generic form of static analysis, which can be driven by the properties to be verified.
Advisor(s)
dr.ir. Arend Rensink
Duration
2008 - 2012
Project
Sponsor
Strategic Research Orientation
DSN - Dependable Systems and Networks
Links to relevant web pages:
- |
- |
- |
- |
Pictures
