December 2004 - PPL-devel - BUGSENG Mailman

ppl/src LinExpression.cc LinExpression.defs.hh
by Roberto Bagnara 05 Dec '04

05 Dec '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-12-05 21:56:16 Modified files: src : LinExpression.cc LinExpression.defs.hh Log message: New method LinExpression::OK(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/LinExpression.cc.diff?cvs… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/LinExpression.defs.hh.dif…

1 0

ppl src/Generator.defs.hh src/Generator.inline ...
by Roberto Bagnara 05 Dec '04

05 Dec '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-12-05 21:48:47 Modified files: src : Generator.defs.hh Generator.inlines.hh LinExpression.defs.hh LinExpression.inlines.hh Variable.defs.hh Variable.inlines.hh tests : membytes1.cc Log message: Added Variable::total_memory_in_bytes() and Variable::external_memory_in_bytes(). Added Generator::total_memory_in_bytes() and Generator::external_memory_in_bytes(). Added LinExpression::total_memory_in_bytes() and LinExpression::external_memory_in_bytes(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Generator.defs.hh.diff?cv… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Generator.inlines.hh.diff… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/LinExpression.defs.hh.dif… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/LinExpression.inlines.hh.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Variable.defs.hh.diff?cvs… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Variable.inlines.hh.diff?… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/membytes1.cc.diff?cvsro…

1 0

ppl/tests membytes1.cc
by Roberto Bagnara 05 Dec '04

05 Dec '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-12-05 07:47:14 Modified files: tests : membytes1.cc Log message: Avoid compiler warnings. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/membytes1.cc.diff?cvsro…

1 0

ppl ./TODO interfaces/Prolog/Prolog_interface.dox
by Roberto Bagnara 05 Dec '04

05 Dec '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-12-05 07:31:45 Modified files: . : TODO interfaces/Prolog: Prolog_interface.dox Log message: We now explain to the GNU Prolog user that GNU Prolog must be configured using the `--disable-regs' option, if it has to work with _any_ foreign code (not just the PPL). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/TODO.diff?cvsroot=ppl&r1=1.11… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/interfaces/Prolog/Prolog_inte…

1 0

Due seminari sulla generazione e le applicazioni di invarianti polinomiali
by Roberto Bagnara 03 Dec '04

03 Dec '04

[Con preghiera di diffusione e scuse per l'eventuale ricezione di copie multiple. RB] ---------------------------------------------------------------------- Date: Martedi`, 11 gennaio 2005 Time: 14:30 Speaker: Enric Rodriguez Carbonell Technical University of Catalonia (UPC) Barcelona, Spain Title: Generation of Polynomial Equality Invariants by Abstract Interpretation Abstract: Program verification aims at proving that a program meets its specification, i.e. that the actual program behaviour coincides with the desired one. Invariants are properties that hold at any reachable state of the system, and are essential in order to prove safety requirements, when one must show that the system will never reach a bad state. Abstract interpretation is a framework for generating these invariants, which can be expressed in a variety of languages, e.g. intervals, linear inequalities and modular equalities. This seminar is focused on finding polynomial equality invariants by means of the abstract interpretation approach. The semantics of a simple imperative programming language is given in terms of ideals of polynomials, a basic concept in algebraic geometry. It is shown with some examples how polynomial invariants can be employed in order to verify properties of imperative programs. Place: Sala Riunioni Dipartimento di Matematica Universita` di Parma Via D'Azeglio, 85/A Parma ====================================================================== Date: Martedi`, 11 gennaio 2005 Time: 15:45 Speaker: Enric Rodriguez Carbonell Technical University of Catalonia (UPC) Barcelona, Spain Title: Applications of Polynomial Invariants Abstract: In a previous talk, the application of polynomial invariants to the verification of imperative programs has been discussed. In this seminar it is shown how polynomial invariants can also be employed in order to verify properties of other classes of systems: Petri nets and hybrid systems. Petri nets are a mathematical modelling tool for studying systems that are characterized as being concurrent, asynchronous, distributed, parallel, non-deterministic, and/or stochastic. On the other hand, hybrid systems are systems that have discrete event dynamics as well as continuous time dynamics. They are used in the analysis of, e.g, continuous systems with phased operations (walking robots, biological cell growth and division) and continuous systems controlled by discrete logic (aircraft autopilot modes, thermostats, chemical plants with valves and pumps, automobile automatic transmissions). Place: Sala Riunioni Dipartimento di Matematica Universita` di Parma Via D'Azeglio, 85/A Parma ---------------------------------------------------------------------- -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0