Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
Línea 16: | Línea 16: | ||
|- | |- | ||
| '''Code:''' | | '''Code:''' | ||
− | | You can find the PVS theories [http://www.cs.us.es/~mjoseh/pub/PROTEMO.tgz here]. | + | | You can find the PVS (version 3.2) theories [http://www.cs.us.es/~mjoseh/pub/PROTEMO.tgz here]. |
+ | | You can find the PVS (version 4.2) theories [http://www.cs.us.es/~mjoseh/pub/PROTEMO_4.2 here]. | ||
|- | |- | ||
| '''Documentation:''' | | '''Documentation:''' |
Revisión del 11:09 7 oct 2010
Title: | Proving termination with multiset orderings in PVS: theory, methodology and applications | |
Authors: | José A. Alonso, María J. Hidalgo and Francisco J. Martín. | |
Date: | November 2009. | |
Description: | This theory presents a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of:
| |
Code: | You can find the PVS (version 3.2) theories here. | You can find the PVS (version 4.2) theories here. |
Documentation: | Papers and documents related with this work: |