Embedding of systems of affine recurrence equations in Coq
In: TPHOLs 2003 : theorem proving in higher order logics (Rome, 8-12 September 2003)Lecture notes in computer science :155-170
Konferenz
- print, 17 ref
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.
Titel: |
Embedding of systems of affine recurrence equations in Coq
|
---|---|
Autor/in / Beteiligte Person: | CACHERA, David ; PICHARDIE, David |
Link: | |
Quelle: | TPHOLs 2003 : theorem proving in higher order logics (Rome, 8-12 September 2003)Lecture notes in computer science :155-170 |
Veröffentlichung: | Berlin: Springer, 2003 |
Medientyp: | Konferenz |
Umfang: | print, 17 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|