Embedding of Systems of Affine Recurrence Equations in Coq.
In: Theorem Proving in Higher Order Logics (9783540406648); 2003, p155-170, 16p
Buch
Zugriff:
Systems of affine recurrence equations (SAREs) over polyhedral domains are widely used to model computation-intensive algorithms and to derive parallel code or hardware implementations. The development of complex SAREs for real-sized applications calls for the elaboration of formal verification techniques. As the systems we consider are generic, i.e., depend on parameters whose value are not statically known, we considered using theorem provers, and have implemented a translation from SAREs into the Coq system. We take advantage of the regularity of our model to automatically generate an inductive type adapted to each particular system. This allows us to automatically prove that the functional translation of equations respects the wanted fixpoint properties, and to systematically derive mutual induction schemes. [ABSTRACT FROM AUTHOR]
Copyright of Theorem Proving in Higher Order Logics (9783540406648) is the property of Springer eBooks and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Titel: |
Embedding of Systems of Affine Recurrence Equations in Coq.
|
---|---|
Autor/in / Beteiligte Person: | Cachera, David ; Pichardie, David |
Quelle: | Theorem Proving in Higher Order Logics (9783540406648); 2003, p155-170, 16p |
Veröffentlichung: | 2003 |
Medientyp: | Buch |
ISBN: | 978-3-540-40664-8 (print) |
DOI: | 10.1007/10930755_10 |
Sonstiges: |
|