January 2005 - PPL-devel - BUGSENG Mailman

ppl/src Checked_Number.defs.hh Checked_Number. ...
by Abramo Bagnara 07 Jan '05

07 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-07 23:39:59 Modified files: src : Checked_Number.defs.hh Checked_Number.inlines.hh Makefile.am Rounding.inlines.hh checked.defs.hh checked.inlines.hh checked_ext.inlines.hh Log message: Allows Checked_Number to handle extended values via appropriate policy. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Checked_Number.defs.hh.di… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Checked_Number.inlines.hh… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Makefile.am.diff?cvsroot=… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Rounding.inlines.hh.diff?… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked.defs.hh.diff?cvsr… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked.inlines.hh.diff?c… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_ext.inlines.hh.di…

1 0

Due seminari sulla generazione e le applicazioni di invarianti polinomiali
by Roberto Bagnara 07 Jan '05

07 Jan '05

[Con preghiera di diffusione e scuse per l'eventuale ricezione di copie multiple. Ulteriori dettagli alla pagina http://www.cs.unipr.it/Seminars/ 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

ppl/src checked_float.inlines.hh
by Abramo Bagnara 06 Jan '05

06 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-06 21:30:03 Modified files: src : checked_float.inlines.hh Log message: White spaces fix. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_float.inlines.hh.…

1 0

ppl/src checked_int.inlines.hh
by Abramo Bagnara 06 Jan '05

06 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-06 21:29:33 Modified files: src : checked_int.inlines.hh Log message: White spaces fix. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_int.inlines.hh.di…

1 0

ppl/src Float.defs.hh
by Abramo Bagnara 06 Jan '05

06 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-06 21:28:46 Modified files: src : Float.defs.hh Log message: White spaces fix. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Float.defs.hh.diff?cvsroo…

1 0

ppl/src Extended_Number.types.hh Extended_Numb ...
by Abramo Bagnara 06 Jan '05

06 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-06 21:27:38 Removed files: src : Extended_Number.types.hh Extended_Number.inlines.hh Log message: Removed files. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Extended_Number.types.hh.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Extended_Number.inlines.h…

1 0

ppl/src Extended_Number.defs.hh
by Abramo Bagnara 06 Jan '05

06 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-06 21:27:14 Removed files: src : Extended_Number.defs.hh Log message: Removed files. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Extended_Number.defs.hh.d…

1 0

w3ppl/htdocs/Documentation ppl.bib
by Patricia Hill 04 Jan '05

04 Jan '05

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: hill(a)cs.unipr.it 2005-01-04 13:41:59 Modified files: htdocs/Documentation: ppl.bib Log message: Removed erroneous line in Mine01a. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl.bi…

1 0

ppl/tests/Polyhedron memory2.cc
by Roberto Bagnara 02 Jan '05

02 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-02 08:09:31 Modified files: tests/Polyhedron: memory2.cc Log message: Force failure everywhere until the bug is fixed. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/memory2.cc.d…

1 0

ppl/tests/Polyhedron Makefile.am memory2.cc
by Roberto Bagnara 01 Jan '05

01 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-01 23:54:34 Modified files: tests/Polyhedron: Makefile.am Added files: tests/Polyhedron: memory2.cc Log message: Another program to test the allocation error recovery facility of the library. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/memory2.cc?c… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/Makefile.am.…

1 0