Name
Abstract | ||
|---|---|---|
Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, for example, safety- or security-critical applications. The context for our work is the SPARK Approach for the development of high integrity software. The SPARK Approach provides a significant degree of automation in proving exception freedom. Where this automation fails, however, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimize this burden by increasing the automation, through an integration of proof planning and a program analysis oracle. We advocate a `cooperative' integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/s10817-006-9034-1 | J. Autom. Reasoning |
Keywords | Field | DocType |
program proof,proof planning,static analysis,SPARK | Automated reasoning,Spark (mathematics),Programmer,Programming language,Computer science,Oracle,Automation,Software,Program analysis,Software verification | Journal |
Volume | Issue | ISSN |
36 | 4 | 0168-7433 |
Citations | PageRank | References |
6 | 0.43 | 31 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew Ireland | 1 | 122 | 15.39 |
| Bill J. Ellis | 2 | 16 | 1.30 |
| Andrew Cook | 3 | 6 | 0.43 |
| Roderick Chapman | 4 | 120 | 10.62 |
| Janet Barnes | 5 | 6 | 0.43 |