Workshop on "Program Correctness:
abstract interpretation vs. classical verification methods"

Venezia 10-12 June 1996
Auditorium Santa Margherita

Speakers:

Jean-Raymond Abrial, Paris
Frank de Boer, Utrecht
Livio Colussi, Padova
Patrick Cousot, LIENS - Paris
Yves Deville, U.C. Louvain
Gerard Ferrand, Orleans
Giorgio Levi, Pisa
Jan Maluszynski, Linkoping
Angelo Morzenti, Milano
Dino Pedreschi, Pisa

Monday, 10	h. 11.00 - 13.30 Patrick Cousot	h. 15.00 - 18.30 Giorgio Levi Gerard Ferrand
Tuesday, 11	h. 9.00 - 14.00 Jan Maluszynski Frank De Boer Livio Colussi	h. 15.30 - 18.30 Jean-Raymond Abrial Angelo Morzenti
Wednesday, 12	h. 10.00 - 13.30 Yves Deville Dino Pedreschi

Jean-Raymond Abrial: Formal Construction of Distributed Programs (with an example of protocol construction).

Livio Colussi Data Flow Semantics for (C)LP and Applications.

Patrick Cousot From Semantics to Classical Proof Methods by Abstract Interpretation.

Frank de Boer - Maurizio Gabbrielli : Proving Correctness of CCP and of CLP with dynamic scheduling.

Yves Deville: Correctness criteria in logic program synthesis .

Gerard Ferrand: Towards proof methods of partial correctness and declarative error diagnosis in (Constraint) Logic Programming .

Giorgio Levi: Proving properties of logic programs by abstract diagnosis.

Jan Maluszynski: Directional types and abstract interpretation

Angelo Morzenti: Specification, validation, and verification of industrially-sized time critical systems in TRIO .

Dino Pedreschi : The Declarative Side of Magic