Cleanly combining specialised program analysers

Abstract

Automatically proving that (infinite-state) software programs satisfy a specification is an important task, but has proved very difficult. Thus, in order to obtain techniques that work with reasonable speed and without user guidance, researchers have typically targeted restricted classes of language features, programming idioms and properties. We have designed a system in which several of these specialised techniques can be used together in proving that a program is correct; this is done without breaking modularity by propagating information between the analyses, expressed as formulae of an expressive common logic. In this way, we can verify programs which, because they use diverse language features and idioms, are difficult or impossible to prove using any one individual technique. Our system is implemented in the experimental tool HECTOR.