Name
Abstract | ||
|---|---|---|
. We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which
generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done “online”,
at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some
verification conditions; the other is done “offline”, once for all, interactively with a general purpose prover; the offline
proof shows that the verification conditions checked by the online prover are sufficient to guarantee the correctness of each
translation. The provably correct verification conditions can thus be seen as specifications for the online prover. This approach
is called mechanized result verification. This paper describes the project requirements and explains the motivations to formal validation by mechanized result verification,
provides an overview of the formalization of the specifications for the online prover and discusses in detail some issues
we have addressed in the mechanized offline proof. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/PL00010809 | STTT |
Keywords | Field | DocType |
valida- tion,safety critical software,decomposition,mechanized result verification,on- line/offline checking,theorem proving | Programming language,General purpose,Computer science,Automated theorem proving,Formal validation,Correctness,Theoretical computer science,Software,Gas meter prover,Software verification | Journal |
Volume | Issue | Citations |
3 | 1 | 3 |
PageRank | References | Authors |
0.45 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paolo Traverso | 1 | 3483 | 223.80 |
| Piergiorgio Bertoli | 2 | 775 | 46.89 |