Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
(No se muestran 16 ediciones intermedias de 2 usuarios) | |||
Línea 1: | Línea 1: | ||
{| border="1" | {| border="1" | ||
− | | '''Title:''' Proving termination with multiset orderings in PVS: theory, methodology and applications | + | | '''Title:''' |
+ | | Proving termination with multiset orderings in PVS: theory, methodology and applications | ||
|- | |- | ||
− | | ''' | + | | '''Authors:''' |
+ | | {{jalonso}}, {{mjoseh}} and {{fmartin}}. | ||
|- | |- | ||
− | | '''Date:''' November 2009. | + | | '''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: | |
− | + | # A formalization of the theorem of Dershowitz and Manna. | |
− | + | # A methodology for proving termination properties. | |
− | + | # Three case studies: a tail-recursive definition of Ackermann's function, an iterative definition of McCarthy's 91 function and an iterative function to compute a generic schema for double recursion | |
− | * '''Documentation:''' | + | |- |
+ | | '''Code:''' | ||
+ | | You can find the PVS theories: | ||
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/PROTEMO.tgz Version in PVS-3.2] | ||
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/PROTEMO.tgz Version in PVS-4.2]. | ||
+ | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/PROTEMO.tgz Version in PVS-5.0]. | ||
+ | |- | ||
+ | | '''Documentation:''' | ||
+ | | Papers and documents related with this work: | ||
+ | *[http://www.cs.us.es/~mjoseh/pub/Proving_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 actual del 14:19 8 feb 2012
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: |
Documentation: | Papers and documents related with this work: |