[Termtools] category for imperative programs

Claude Marche marche at lri.fr
Thu Mar 16 11:54:53 CET 2006


I've seen that AProve is able to deal with some kind of imperative
programs, written in the language IPAD.  I do not know this language,
but is their a fairly large common subset shared with C or Java ?
Are there other people working on that kind of termination problems ?

I know of the Terminator project at Microsoft
http://research.microsoft.com/terminator/ but I do not whether they
like to participate. They apparently consider true C programs. 

Anyway, it would be easy for me to include a category for IPAD, to
motivate more research on the case of imperative programs. I hope the
AProve team would agree to provide a suite of examples.

- Claude

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools



More information about the Termtools mailing list