| Autor: |
Arusoaie, Andrei, Nowak, David, Rusu, Vlad, Lucanu, Dorel |
| Přispěvatelé: |
Dynamic Reconfigurable Massively Parallel Architectures and Languages (DREAMPAL), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Extra Small Extra Safe (2XS), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Department of Computer Science [Lasi], Universitatea Alexandru Ioan Cuza [Lasi], INRIA Lille - Nord Europe, Alexandru Ioan Cuza, University of Iasi, Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: |
angličtina |
| Rok vydání: |
2015 |
| Předmět: |
|
| Zdroj: |
[Technical Report] RR-0471, INRIA Lille-Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27 |
| Popis: |
Proving programs correct is one of the major challenges that computer scientists have been struggling with during the last decades.For this purpose, Reachability Logic (RL) was proposed as a language-parametric generalisation of Hoare Logic. Recently, based on RL, an automatic verification procedure was given and proved sound. In this paper we generalise this procedure and prove its soundness formally in the Coq proof assistant. For the formalisation we had to deal with all the minutiae that were neglected in the paper proof. The trickiest one was appropriate renaming of free variables which, we discovered, was handled in the paper proof using an insufficient assumption.We also discovered a missing case in the paper proof, and we clarified some implicit and hidden hypotheses.Last but not least, the Coq formalisation provides us with a certified program-verification procedure. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
