Reseña: Machine-checked proofs for realizability checking algorithms
Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Machine-checked proofs for realizability checking algorithms.
Sus autores son
- Andreas Katis (de la Universidad de Minesota),
- Andrew Gacek (del Rockwell Collins Advanced Technology Center) y
- Michael W. Whalen (del Critical Systems Group (CriSys) en la Universidad de Minesota).
Su resumen es
We have recently proposed a contract-based realizability checking algorithm involving the use of theories, to provide an auxiliary procedure to consistency checking of “leaf-level” components in complex embedded systems. To prove the soundness of our approach on realizability, we formalized the necessary definitions and theorems of Towards realizability checking of contracts using theories, in the Coq proof and specification language.
El código de las correspondientes teorías en Coq se encuentra [aquí](.https://github.com/andrewkatis/Coq/
blob/master/realizability/Realizability.v).