Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
Línea 19: | Línea 19: | ||
|- | |- | ||
| '''Documentation:''' | | '''Documentation:''' | ||
− | | [http://www.cs.us.es/~mjoseh/pub/ | + | | Papers and documents related with this work: |
+ | *[http://www.cs.us.es/~mjoseh/pub/wProving_termination_with_multiset_orderings_in_PVS.pdf Proving termination with multiset orderings in PVS: theory, methodology and applications] | ||
+ | *[http://www.cs.us.es/~mjoseh/pub/Well_founded_multiset_order.pdf Formalización en PVS de la buena fundamentación del orden de multiconjuntos] | ||
|} | |} |
Revisión del 13:01 15 jun 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 theories here. |
Documentation: | Papers and documents related with this work: |