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 `on-line`, 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 `off-line`, once for all, interactively with a general purpose prover; the off-line proof shows that the verification conditions checked by the on-line prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the on-line prover. This approach is called mechanized result verification

Mechanized Result Verification: an Industrial Application

Traverso, Paolo;Bertoli, Piergiorgio
2000-01-01

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 `on-line`, 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 `off-line`, once for all, interactively with a general purpose prover; the off-line proof shows that the verification conditions checked by the on-line prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the on-line prover. This approach is called mechanized result verification
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1958
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact