Computing Publications

Publications Home » Cleanly combining specialised pro...

Cleanly combining specialised program analysers

Nathaniel Charlton, Michael Huth

Conference or Workshop Paper
Automated Reasoning Workshop 2007, 19th-20th April 2007, Department of Computing, Imperial College, London
April, 2007

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.


Extended abstract for Automated Reasoning Workshop 2007

PDF of full publication (102 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.