Mechanized result verification: an industrial application
| Autor: | Piergiorgio Bertoli, Paolo Traverso |
|---|---|
| Rok vydání: | 2000 |
| Předmět: |
Correctness
Programming language business.industry Computer science Gas meter prover computer.software_genre Translation (geometry) Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Software General purpose TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Theory of computation business computer Software verification Information Systems |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 3:78-92 |
| ISSN: | 1433-2779 |
| DOI: | 10.1007/pl00010809 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink