[PPL-devel] [GIT] ppl/ppl(master): Added an entry for the new functionality concerning the synthesis of linear (quasi-) ranking functions.
Roberto Bagnara
bagnara at cs.unipr.it
Sun Apr 11 09:37:04 CEST 2010
Module: ppl/ppl
Branch: master
Commit: f6bc3b69e7f30d3993b5292c14d3091891fc4f3a
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6bc3b69e7f30d3993b5292c14d3091891fc4f3a
Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date: Sun Apr 11 09:25:47 2010 +0200
Added an entry for the new functionality concerning the synthesis of linear (quasi-) ranking functions.
---
NEWS | 24 ++++++++++++++++--------
1 files changed, 16 insertions(+), 8 deletions(-)
diff --git a/NEWS b/NEWS
index 0ed5d9e..0dfcdf6 100644
--- a/NEWS
+++ b/NEWS
@@ -14,14 +14,22 @@ o New class PIP_Problem provides a Parametric Integer Programming
(PIP) problem solver (mainly based on P. Feautrier's
specification). The implementation combines a parametric dual
simplex algorithm using exact arithmetic with Gomory's cut
- generation.
- Still under beta testing.
-
-o New "deterministic" timeout computation facilities: it is now possible
- to set computational bounds (on the library calls taking exponential time)
- that do not depend on the actual elapsed time and hence are independent
- from the actual computation environment (CPU, operating system, etc.).
- Still under beta testing.
+ generation. Still under beta testing.
+
+o New "deterministic" timeout computation facilities: it is now
+ possible to set computational bounds (on the library calls taking
+ exponential time) that do not depend on the actual elapsed time and
+ hence are independent from the actual computation environment (CPU,
+ operating system, etc.). Still under beta testing.
+
+o New support for termination analysis via the automatic synthesis of
+ linear ranking functions. Given a sound approximation of a loop,
+ the PPL provides methods to decide whether that approximation
+ admits a linear ranking function (possibly obtaining one as a
+ witness for termination) and to compute the space of all such
+ functions. In addition, methods are provided to obtain the space
+ of all linear quasi-ranking functions, for use in conditional
+ termination analysis. Still under beta testing.
o All the PPL semantic objects provide new methods
More information about the PPL-devel
mailing list