Testo italiano

Certificazione automatica di programmi mediante interpretazione astratta

Testo inglese

Automatic program certification by abstract interpretation

GIACOBAZZI	ROBERTO
(cognome)	(nome)
Università degli Studi di VERONA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di SCIENTIFICO E TECNOLOGICO
(settore scient.discipl.)	(Dipartimento/Istituto)

giaco@sci.univr.it
(E-mail)

ROSSI	GIANFRANCO
(cognome)	(nome)

Professore associato	30/08/1956	RSSGFR56M30H223G
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi di PARMA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di MATEMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

0521/902309	0521/902350	gianfr@prmat.math.unipr.it
(prefisso e telefono)	(numero fax)	(E-mail)

K05B

Testo italiano
ANALISI DI PROGRAMMI ; PROGRAMMAZIONE LOGICA CON VINCOLI ; INTERPRETAZIONE ASTRATTA ; VERIFICA DI PROGRAMMI ; VINCOLI INSIEMISTICI

Testo inglese
PROGRAM ANALYSIS ; CONSTRAINT LOGIC PROGRAMMING ; ABSTRACT INTERPRETATION ; PROGRAM VERIFICATION ; SET CONSTRAINTS

Testo italiano

Gianfranco Rossi ha ricevuto la laurea in Scienze dell'Informazione
dall'Universita' di Pisa nel 1979. Dal 1981 al 1983 ha lavorato presso
la societa` Intecs Co. System House a Pisa. Da Novembre 1983 a
Febbraio 1989 e` stato ricercatore presso il Dipartimento di
Informatica dell'Universita` di Torino. Da Marzo 1989 e' Professore
Associato di Fondamenti dell'Informatica, attualmente in servizio
presso l'Universita' di Parma. E` autore di numerosi articoli
riguardanti principalmente i linguaggi di programmazione, con
particolare riferimento ai linguaggi di programmazione logica e al
Prolog, e gli algoritmi di unificazione estesi. I suoi attuali
interessi di ricerca sono nel campo dei linguaggi (logici) con insiemi
e degli algoritmi di unificazione insiemistica.

Testo inglese

Gianfranco Rossi received his degree in Computer Science from the
University of Pisa in 1979. From 1981 to 1983 he was employed at
Intecs Co. System House in Pisa. From November 1983 to February 1989
he was a researcher at the Dipartimento di Informatica of the
University of Turin. Since March 1989 he is an Associate Professor of
Computer Science, currently with the University of Parma. He is the
author of several papers dealing mainly with programming languages, in
particular logic programming languages and Prolog, and extended
unification algorithms. His current research interests are (logic)
programming languages with sets and set unification algorithms.

1. DOVIER A., POLICRITI A., ROSSI G., , "Uniform Axiomatic View of Lists, Multisets, and Sets, and the Relevant Unification Algorithms" , Rivista: Fundamenta Informaticae , Volume: 36(2/3) , pp.: 201-234 , (1998) .
2. DOVIER A., PONTELLI E., ROSSI G., OMODEO E., "{log}: A Language for Programming in Logic with Finite Sets" , Rivista: Journal of Logic Programming , Volume: 28(1) , pp.: 1-55 , (1996) .
3. GIORDANO L., MARTELLI A., ROSSI G., , "Structured Prolog: A Language for Structured Logic Programming" , Rivista: Software: Concepts and Tools , Volume: 15 , pp.: 125-145 , (1994) .
4. LAMMA E., MELLO P., ROSSI G., , "Parametric Composable Modules in a Logic Programming Language" , Rivista: Computer Languages , Volume: 18 , pp.: 105-123 , (1993) .
5. GIORDANO L., MARTELLI A., ROSSI G., , "Extending Horn Clause Logic with Implication Goals" , Rivista: Theoretical Computer Science , Volume: 95(1) , pp.: 43-74 , (1992) .

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						1999	2000
1	ROSSI	GIANFRANCO	MATEMATICA	Prof. associato	K05B	11	8
2	BAGNARA	ROBERTO	MATEMATICA	Ricercatore	K05B	11	8

1.10.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							1999	2000

1.10.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.10.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.10.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	Dottore di ricerca	25	11

1.10.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Mesi uomo
1.	ZAFFANELLA	ENEA	Universita` degli Studi di Modena e Reggio Emilia	Coll. di Elab. Dati, VII liv.	12

Testo italiano

Tecniche e strumenti per l'analisi efficiente di programmi

Testo inglese

Tools and techniques for efficient program analysis

Testo italiano

Varie proposte sono state avanzate di recente nel campo dei metodi formali ed informali per la specifica e la verifica di sistemi software sicuri. Tra queste, gli approcci basati sull'interpretazione astratta [CC77,CC79,CC92a,CC92b] sembrano particolarmente promettenti. L'interpretazione astratta e' un metodo generale che permette di fornire un modello approssimato dell'esecuzione di un programma e puo' percio' essere di grande utilita' nella specifica di strumenti "semantics-based" per l'analisi di programmi, inclusa la sicurezza ed altre forme di certificazione dei programmi. Il punto chiave nella definizione di un interprete astratto e' la definizione di un dominio astratto, e cioe' di un oggetto matematico che permetta di approssimare proprieta' concrete di un programma in termini delle corrispondenti proprieta' astratte. Scegliere un dominio astratto appropriato corrisponde di fatto ad aumentare o diminuire la precisione dell'analisi.
Vari domini astratti sono stati stati sviluppati allo scopo di permettere l'analisi di programmi basata su interpretazione astratta.
Il dominio "Sharing" [JL92] e` il dominio di analisi piu` usato per la determinazione del possibile aliasing tra le variabili di un programma logico. Dopo la sua introduzione, la ricerca si e` soprattutto concentrata sul come migliorare ulteriormente la sua precisione combinandolo con altri domini: linearita`, "freeness", sostituzioni astratte "depth-k", e cosi` via [BC93, KS94, MH92]. In un recente lavoro e` stato dimostrato che Sharing, quando considerato in isolamento, e` ottimo [CF99].
Un'altra scelta che sembra offrire risultati interessanti nell'analisi di programmi e' quella che prevede l'utilizzo di domini astratti di tipo insiemistico ("set-based analysis") [HJ94, CC95, CL96, CLB97]. L'utilizzo di tali domini comporta la necessita' di dover descrivere e trattare operazioni anche complesse su insiemi tramite opportune formule insiemistiche del prim'ordine (vincoli insiemistici). Una classe di vincoli insiemistici ampiamente studiata e' quella dei set-constraint, che sono essenzialmente congiunzioni di relazioni di inclusione tra insiemi di termini su una data segnatura S (si veda ad esempio [AW92, Aik94, HJ94, Koz98]). Per questo tipo di vincoli insiemistici (e per loro sotto-classi) sono stati proposti vari algoritmi per la verifica della loro soddisfacibilita' rispetto ad una data interpretazione privilegiata (ad esempio, [AKVW93, GTT93, GTT93a, CP94, Ste94]).
Altre interessanti classi di vincoli insiemistici sono quelle fornite dai linguaggi logici con vincoli insiemistici, come CLPS [LL91], Conjunto [Ger97], e CLP(SET) [DR93, DPPR98]. Sebbene sviluppate come parte di linguaggi di tipo general-purpose questo tipo di vincoli insiemistici potrebbe risultare adeguato anche ad un impiego nella analisi di programmi set-based come una valida alternativa all'uso dei set-constraint.
Il gruppo di Parma (Dipartimento di Matematica) ha maturato significative esperienze sia sull'analisi di aliasing per programmi logici, che sulla definizione e gestione di linguaggi di vincoli insiemistici.
Per quanto riguarda l'aliasing, in [BHZ97] e` stato mostrato come il dominio Sharing sia inutilmente complesso per l'analisi di aliasing tra coppie di variabili. Nello stesso lavoro e` stata identificata la piu` semplice astrazione di Sharing che mantiene la stessa precisione di Sharing. Questo ha portato ad una significativa riduzione della complessita` della procedura di unificazione astratta. La correttezza di Sharing (e del piu` semplice dominio definito in [BHZ97]) e` stata completamente dimostrata (per la prima volta) in [HBZ98]. Si osservi che in [HBZ98] la correttezza di Sharing viene dimostrata indipendentemente dal fatto che il linguaggio analizzato preveda l'unificazione con o senza l'"occur-check". Tutti i lavori precedenti sull'argomento assumono che l'occur-check sia eseguito, il che non e` vero per quasi tutti i linguaggi effettivamente implementati.
Un lavoro in corso di svolgimento [ZBH99] mostra che opportuni operatori di widening [CC92] applicati alla nostra versione non ridondante di Sharing, accoppiati con un'implementazione particolarmente efficiente del dominio Pos [BS99] e con un dominio per il rilevamento di informazioni strutturali [Bag97], danno luogo ad un'analisi molto accurata. Inoltre, la risultante tecnica di analisi si dimostra attuabile: l'analisi puo` essere applicata a qualsiasi programma logico (con o senza vincoli) e termina in ogni caso in tempi ragionevoli.
Per quanto riguarda i vincoli insiemistici, in [DR93] e' stato definito un linguaggio logico con vincoli insiemistici, denominato CLP(SET), successivamente ampliato in [DPPR98]. CLP(SET) offre la possibilita' di definire insiemi ereditariamente finiti di termini e di manipolarli tramite le usuali operazioni insiemistiche, quali quelle di uguaglianza, appartenenza, unione, ecc., opportunamente trattate come vincoli. Un'implementazione funzionante del linguaggio CLP(SET) e' attualmente disponibile nella forma di un interprete scritto in SICStus Prolog. Lavoro preliminare e' stato svolto in [DPR98] per mostrare che i set-constraint possono essere tradotti in CLP(SET)-constraint, e che il risolutore di vincoli fornito da CLP(SET) puo' essere utilizzato per stabilire la soddisfacibilita' di alcune sotto-classi di set-constraint non banali, anche nel caso in cui la loro soluzione coinvolga insiemi infiniti.

Testo inglese

A number of proposals have been recently put forward in formal and informal methods for specification and verification of secure systems. Among them, the approaches based on the abstract interpretation technique [CC77,CC79,CC92a,CC92b] seem particularly promising. Abstract interpretation is a general method that can be used to provide a formal semantic-based approximated model of program execution, which can be central in the specification of semantic-based tools for program analysis, including security and other forms of program certification.
The key point in the definition of an abstract interpreter is the definition of an abstract domain, that is a mathematical object which allows concrete properties of a program to be approximated in terms of corresponding abstract ones. Selecting appropriate abstract domains corresponds in fact to increase or decrease precision of the analysis.
A number of domains have been developed for program analysis based on abstract interpretation.
The domain Sharing [JL92] is the most widely used analysis domain for tracking aliasing information of logic programs. Variable aliasing is a phenomenon which may occur in general in presence of procedure calls and it refers to the fact that different variables may share a common region in memory. This fact induces an implicit flow of information which may strongly influence program certification and which is not detected by traditional analysis methods. After the introduction of Sharing, research has mostly concentrated on how to improve its precision further by combining it with other domains: linearity, freeness, depth-k abstract substitutions and so on [BC93, KS94, MH92]. Sharing, when considered in isolation, has been proved to be optimal in [CF99].
A different class of abstract domains which seems offering quite interesting results for program analysis is the class of set-based domains [HJ94, CC95, CL96, CLB97]. The ability to compute over such domains requires to be able to
define and manipulate (possibly complex) first-order formulae built-out of classical set-theoretical symbols (set-based constraints). A class of set-based constraints which has been widely studied in the past is the class of so called set-constraints (SC). Basically, SCs are conjunctions of inclusions between sets of terms over a given signature S (see, e.g., [AW92, Aik94, HJ94, Koz98]). For this kind of set-based constraints, a number of algorithms have been proposed to test satisfability w.r.t. a given privileged interpretation (see, e.g., [AKVW93, GTT93, GTT93a, CP94, Ste94]). Other interesting classes of set-based constraints are those provided by constraint logic programming (CLP) languages with sets, such as CLPS [LL91], Conjunto [Ger97], and CLP(SET) [DR93,DPPR98]. Though developed as part of general-purpose languages this kind of set-based constraints could be used as well as an alternative to SCs in set-based program analysis.
The group of Parma (Dipartimento di Matematica) has matured significant experiences on both aliasing (sharing) analysis of logic programs and the definition and management of set-based constraints.
In [BHZ97] the domain Sharing was proved to be unnecessarily complex for tracking aliasing between pairs of variables, and the simplest abstraction of Sharing, with the same precision as Sharing itself, was identified. This lead to a significant reduction in the complexity of the abstract unification procedure. The correctness of Sharing and of the simpler domain defined in [BHZ97] have been fully proved (for the first time) in [HBZ98]. It is worth noticing that in [HBZ98] the correctness of Sharing is proved independently from the fact that the analyzed language performs unification with or without the occur-check. All the previous works on the subject assumed the occur-check was performed, which is not true for almost all implemented languages. Ongoing work [ZBH99] shows that appropriate widening operators [CC92] applied to our non-redundant version of Sharing, together with a particularly efficient implementation of Pos [BS99] and with structural information [Bag97], gives rise to a very accurate analysis. Moreover, this technique is also practical: the analysis can be applied to just any (C)LP program and terminates in reasonable time.
As regards set-based constraints, a general-purpose CLP language with sets, called CLP(SET), has been defined in [DR93] and subsequently extended in [DPPR98]. CLP(SET) offers the possibility of defining heriditarily finite sets of terms and manipulating them through the usual basic set-theoretic operations, such as equality, membership, union, suitably dealt with as constraints. A working implementation of CLP(SET) is currently available in the form of an interpreter running on the top of SICStus Prolog. Preliminary work has been done [DPR98] to show that, set constraints can be translated to CLP(SET) constraints and that the CLP(SET) constraint solver can be used to decide satisfiability of non-trivial sub-classes of set constraints, even if their solutions possibly involve infinite sets.

[Aik94] A. Aiken. Set constraints: Results, Applications, and Future Directions. In A. Borning editor, Principles and Practice of Constraint Programming, Second Int'l Workshop, PPCP'94, LNCS Vol. 874, pp. 326-335, Springer-Verlag, 1994.
[AKVW93] A.Aiken, D.Kozen, M.Vardi, and E.Wimmers. The complexity of set constraints. In E.Borger, Y.Gurevich, and K.Meinke, editors, Proc. 1993 Conference on CSL, volume 832 of LNCS, pages 1--17. Springer-Verlag, Berlin, 1993.
[AW92] A.Aiken and E.Wimmers. Solving systems of set constraints. In Proc. 7th Symp. Logic in Computer Science, pages 329--340. IEEE, 1992.
[ADR98] D.Aliffi, A.Dovier, and G.Rossi. From Set to Hyperset Unification. Journal of Functional and Logic Programming (MIT Press), to appear.
[Bag97] R. Bagnara. Structural information analysis for CLP languages. In M. Falaschi, M. Navarro, and A. Policriti, editors, Proceedings of the "1997 Joint Conference on Declarative Programming (APPIA-GULPPRODE'97)", pages 81-92, Grado, Italy, 1997.
[BC93] M. Bruynooghe and M. Codish. Freeness, sharing, linearity and correctness -- All at once. In P. Cousot, M. Falaschi, G. File', and A. Rauzy, editors, Static Analysis, Proceedings of the Third International Workshop, volume 724 of Lecture Notes in Computer Science, pages 153-164, Padova, Italy, 1993. Springer-Verlag, Berlin.
[BHZ97] R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 53-67, Paris, France, 1997. Springer-Verlag, Berlin. Extended version to appear on Theoretical Computer Science.
[BS99] R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, Proceedings of the "Seventh International Conference on Algebraic Methodology and Software Technology (AMAST'98)", volume 1548 of Lecture Notes in Computer Science, pages 471-485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.
[CC77] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238-252, 1977.
[CC79] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269-282, 1979.
[CC92a] P. Cousot and R. Cousot. Abstract interpretation and applications to logic programs. Journal of Logic Programming, 13(2&3):103-179, 1992.
[CC92b] P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269-295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.
[CC95] P.Cousot and R.Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Record of FPCA'95 - Conference on Functional Programming and Computer Architecture, pages 170-181. SIGPLAN/ SIGARCH/WG2.8, ACM Press, New York, USA.
[CF99] A. Cortesi and G. File'. Sharing is optimal. Journal of Logic Programming, 1999. To appear.
[CL96] M.Codish and V.Lagoon. Type Dependencies for Logic Programs Using ACI-Unification. Technical report, Department of Mathematics and Computer Science, Ben-Gurion University of the Negev, Beer-Sheva, Israel, 1996.
[CLB97] F.Bueno, M.Codish, and V.Lagoon. Sharing Analysis Using Set Logic Programs. In Lee Naish ed., Proc. of the Fourteenth International Conference on Logic Programming MIT Press, 1997, pag. 417.
[CP94] W.Charatonik and L.Pacholski. Set constraints with projections are in NEXPTIME. In 35th Annual Symposium on Foundations of Computer Science, pages 642-653, IEEE, 1994.
[DOPR96] A.Dovier, E.Omodeo, E.Pontelli, G.Rossi. {log}: A Language for Programming in Logic with Finite Sets. Journal of Logic Programming, Vol.28(1), North Holland, 1996, 1--55.
[DPPR98] A.Dovier, C.Piazza, E.Pontelli, and G.Rossi. On the Representation and Management of Finite Sets in CLP-languages. In J.Jaffar, editor, Proceedings of 1998 Joint International Conference and Symposium on Logic Programming (J.Jaffar ed.), pp. 40-54, The MIT Press, 1998.
[DPR98] A.Dovier, C.Piazza, G.Rossi. Narrowing the gap between Set-Constraints and CLP(SET)-Constraints. In AGP'98. Joint Conference on Declarative Programming (J. L. Freire and M. Falaschi, eds.), pp. 43--55, La Coruna (ES), July 1998.
[DPR98b] A. Dovier, A. Policriti, and G. Rossi. A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundamenta Informaticae, 36(2/3):201-234, 1998.
[DR93] A.Dovier and G.Rossi. Embedding Extensional Finite Sets in CLP. In D.Miller, ed., Proc. of Int'l Logic Programming Symposium, ILPS'93, p. 540--556, The MIT Press, 1993.
[Ger97] C.Gervet. Interval Propagation to Reason about Sets: Definition and Implementation of a Practical Language. Constraints 1(3):191--244, 1997.
[GTT93] R.Gilleron, S.Tison, and M.Tommasi. Solving system of set constraints with negated subset relationships. In Proc. 34th Symp. Foundations of Computer Science, pages 372--380. IEEE, 1993.
[GTT93a] R.Gilleron, S.Tison, and M.Tommasi. Solving systems of set constraints using tree automata. In Proc. Symp. Theoretical Aspects of Computer Science, volume 665 of LNCS, pages 505--514. Springer-Verlag, Berlin, 1993.
[HJ94] N.Heintze and J.Jaffar. Set Constraints and Set-Based Analysis. In A. Borning editor, Principles and Practice of Constraint Programming, Second Int'l Workshop, PPCP'94, LNCS Vol. 874, pp.281-298, Springer-Verlag, 1994.
[HBZ98] P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proceedings of the 5th International Symposium, volume 1503 of Lecture Notes in Computer Science, pages 99-114, Pisa, Italy, 1998. Springer-Verlag, Berlin.
[JL92] D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291-314, 1992.
[Koz98] D.Kozen. Set Constraints and Logic Programming. Information and Computation 142(1):2--25, 1998.
[KS94] A. King and P. Soper. Depth-k sharing and freeness. In P. Van Hentenryck, editor, Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 553-568, Santa Margherita Ligure, Italy, 1994. The MIT Press.
[LL91b] B.Legeard and E.Legros. Short overview of the CLPS system. In J.Maluszynsky and M.Wirsing, eds., Proc. of PLILP'91, vol.528 of LNCS, 431-433. Springer-Verlag, 1991.
[MH92] K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(2&3):315-347, 1992.
[Ste94] K.Stefansson.Systems of set constraints with negative constraints are NEXPTIME-complete. In Proc. 9th Symp. LICS. IEEE, 1994.
[Tar98] P. Tarau. Jinni: a lightweight java-based logic engine for internet programming. In K. Sagonas, editor, Proceedings of the JICSLP'98 Implementation of LP languages Workshop, Manchester, U.K., 1998. Invited talk.
[ZBH99] E. Zaffanella, R. Bagnara, and P. M. Hill. Widening set-sharing. Quaderno 188, Dipartimento di Matematica, Universita` di Parma, 1999.

Testo italiano

L'Unita' di Parma si propone di continuare ed approfondire le ricerche inerenti l'analisi di aliasing e la definizione di linguaggi di vincoli insiemistici ed il loro utilizzo nell'analisi di programmi basata su insiemi.
Per quanto riguarda l'analisi di aliasing ci si propone di portarla a livelli di precisione ed efficienza superiori a quelli odierni. E` chiaro che l'aspetto della precisione e` molto importante nel campo della certificazione di programmi. Piu` importante di quanto non lo sia, ad esempio, nel campo della compilazione ottimizzata: un fatto e` un'opportunita` di ottimizzazione mancata; altra cosa e` il non riuscire (magari spesso) a produrre certificati per i programmi analizzati, richiedendo cosi` l'intervento diretto dell'utente.
In questo progetto studieremo l'applicazione dell'analisi di aliasing, mirata alla certificazione di programmi, per "agenti mobili" scritti in linguaggi logici (con vincoli), Sebbene la base di conoscenze che il gruppo puo` mettere a disposizione sia significativa, questa nuova applicazione pone una quantita` di problemi che non sono mai stati affrontati prima d'ora. Il lavoro previsto include anche l'ulteriore miglioramento della precisione dell'analisi attraverso una combinazione piu` accurata con informazioni di linearita` e di "compoundness". Va osservato che l'uso della programmazione logica per lo sviluppo di agenti mobili non e` affatto un'idea stravagante, come potrebbe sembrare a prima vista. Cio` e` testimoniato da sistemi emergenti come Jinni [Tar98], che sono si` molto interessanti dal punto di vista teorico, ma sono anche completamente implementati e gia` in uso in applicazioni reali. Jinni costituira` un primo banco di prova per la nostra ricerca. Questo richiedera` l'estensione delle tecniche di analisi note in modo da consentire, tra l'altro, l'analisi di programmi incompleti o solo parzialmente specificati, e l'analisi di programmi concorrenti, comunicanti per mezzo di una "blackboard" condivisa.
Per quanto riguarda i vincoli insiemistici ci si pone come primo obiettivo lo studio e la definizione di domini astratti di tipo insiemistico e lo sviluppo di techniche di analisi di programmi basate sull'utilizzo di tali domini che permettano di ottenere forme di "set-based analysis" piu' generali e flessibili di quelle attualmente descritte in letteratura. Un ulteriore obiettivo che ci si pone in questo contesto e' lo sviluppo di un linguaggio logico con insiemi che permetta la definizione e manipolazione delle astrazioni insiemistiche previste dalle tecniche di analisi sviluppate al punto precedente, con particolare riferimento alle possibilita' di analisi di soddisfacibilita' dei vincoli insiemistici derivanti dall'applicazione delle tecniche stesse. Infine, utilizzando il linguaggio logico sviluppato, si intende realizzare semplici strumenti di analisi di programmi basati sulle tecniche di "set-based analysis" definite.
Il lavoro necessario a raggiungere gli obiettivi sopra esposti verra' svolto in piu' fasi in accordo con la suddivisione in fasi previste dal progetto (descritte nel Mod.A).
In una prima fase, studieremo la composizione di domini astratti per l'analisi di "aliasing" con informazioni di sicurezza. Tenteremo quindi di potenziare le tecniche di analisi ad oggi note in modo da poterle applicare all'analisi di agenti mobili, e in modo da raggiungere gli elevati livelli di precisione richiesti dall'obiettivo della certificazione automatica di programmi. In questa fase, si iniziera' anche lo studio delle tecniche di "set-based analysis" e dei linguaggi con vincoli insiemistici in esse impiegati.
Nella seconda fase studieremo e svilupperemo tecniche per l'analisi efficiente ed incrementale di programmi incompleti. Cio` e` necessario al fine di applicare la certificazione automatica di programmi alle nuove tecniche di compilazione come la compilazione "just-in-time" e quella cosiddetta "continua". Ci si propone inoltre di sviluppare nuove tecniche di analisi basate su insiemi mediante l'utilizzo di uno specifico linguaggio con insiemi, il linguaggio CLP(SET). Per questo si cerchera', da una parte, di estendere opportunamente il linguaggio CLP(SET) (in particolare, con l'allargamento al dominio degli alberi razionali e degli iper-insiemi [ADR98], e con l'introduzione di nuove forme di aggregati, quali i multi-insiemi, le liste e le liste-compatte, continuando ed ampliando il lavoro gia' iniziato in [DPR98b]), dall'altra, di analizzare come le possibilita' specifiche presenti in CLP(SET) (e non presenti, viceversa, ad esempio nel linguaggio dei set-constraint) permettano di individuare nuove classi di vincoli insiemistici decidibili che possono essere sfuttati per ottenere forme di analisi di programmi piu' ampie e precise.
Nell'ultima fase l'obiettivo e` quello di concretizzare tutto il lavoro svolto con la realizzazione di strumenti software effettivamente utilizzabili. Ci proponiamo quindi di completare un analizzatore statico di programmi da utilizzarsi in compilatori "Proof-Carrying-Code" e verificatori. Questo lavoro si basera` sull'analizzatore per programmi CLP China, che abbiamo sviluppato negli ultimi anni. China, che e` scritto in C++, e` probabilmente il piu` preciso ed efficiente analizzatore statico descritto oggi in letteratura (almeno per quanto riguarda le analisi di aliasing e groundness di variabili). Inoltre ci proponiamo di inserire all'interno dell'interprete CLP(SET) gia' esistente le estensioni del linguaggio previste e di implementare, tramite il linguaggio CLP(SET) stesso, alcuni semplici strumenti di analisi di programmi che sfruttino le tecniche di "set-based analysis" sviluppate nelle fasi precedenti.

Testo inglese

We plan to continue and deepen researches concerned with the aliasing analysis and the definition and application of set-based constraint languages in set-based program analysis.
As concerns aliasing analysis we plan to bring it to unprecedented levels of precision and efficiency. It is clear that, for program certification, precision is more an issue than on, say, optimized compilation: a missed optimization is one thing; failing to produce a certificate too often, thus calling for user intervention, is another. In this project, we will study the application of aliasing analysis to mobile (constraint) logic programming code for the purpose of program certification. While the knowledge base we can contribute in this field is significant, this novel application poses a number of questions that were never faced before. Planned work includes also improving precision further by performing a more precise combination of sharing with linearity and compoundness information.
It must be noted that the use of logic programming for mobile agents programming is not as exotic as it might seem at a first glance. This is testified by newly emerging systems such as Jinni [Tar98] that are, theoretically speaking, very interesting, fully implemented, and already used in real applications. Jinni constitutes an obvious first testbed for our research. This requires, among other things, extending the known analysis techniques with the ability to cope with incomplete, partially specified programs, multiple asynchronous inference engines running on separate threads, communication (between the engines) via a shared blackboard.
As concerns set-based constraints, our first goal will be the study and definition of set-based abstract domains and the development of program analysis techniques which, by suitably exploiting such domains, allow us to devise new forms of set-based analysis which are more general and flexible than those described in the literature. A further goal in this context is the development of a logic language with sets which allows us to define and manipulate the set data abstractions required by the analysis techniques just developed, with particular reference to the ability to check satisfiability of the set-based constraints generated by the application of the techniques themselves. Finally, we plan to use this logic language to develop simple program analysis tools which can exploit the new set-based analysis techniques we have developed.
The work we plan to do in order to fullfil the above mentioned goals will be organized in subsequent phases, according to the overall organization of the project (see Mod.A).
In a first phase we will study the combination of abstract domains for aliasing analysis with security information. We will also extend the analysis techniques known to date so as to apply to the analysis of concurrent mobile agents and so as to meet the precision criteria required by the application to program certification. In this phase we plan also to start the study of set-based program analysis techniques and of the relevant (logic) languages with sets used to support them.
In the second phase we will study and develop techniques for the efficient and incremental analysis of incomplete programs. This is required in order to apply automatic program certification to the new compilation techniques known as "just-in-time" and "continuous" compilation. Furthermore, we plan to develop new set-based analysis techniques by using a specific logic language with sets, namely CLP(SET). For this purpose, we will try, on the one hand, to extend CLP(SET) (in particular, by moving to the domain of rational trees and hypersets [ADR98], and by introducing new aggregate data abstractions, namely, multi-sets, lists and compact-list, continuing the work in [DPR98b]) and, on the other hand, to analyze how the distinguishing features of CLP(SET) (not available, in contrast, in current set-constraint languages) allow us to single out new classes of decidable set-based formulae, which could be exploited to obtain wider and more precise forms of program analysis.
In the last phase, we plan to concretize all the work done into usable software tools. We aim at providing a data-flow analyzer that can be used in Proof-Carrying-Code compilers and program verifiers. This work will be based on the China analyzer, a data-flow analyzer for CLP programs we have developed during the last years. China, which is written in standard C++, is probably the most precise and efficient data-flow analyzer (at least for variable aliasing and groundness) described today in the literature. Furthermore, we plan to add to the CLP(SET) interpreter all the extensions previously defined and to implement, by using the CLP(SET) language itself, new simple program analysis tools using the set-based analysis techniques developed in the previous phases.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese
1.	1998	1 personal computer "PC compatible": processore PentiumII a 233MHz, 64MB RAM, 4.2GB HD, sistema operativo Linux 2.2.2	1 PC compatible personal computer: PentiumII processor at 233MHz, 64MB RAM, 4.2GB HD, running Linux 2.2.2
2.	1993	1 workstation Sun SparcStation10: 32MB RAM, 3GB HD, sistema operativo Linux 2.2.2	1 workstation Sun SparcStation10: 32MB RAM, 3GB HD, running Linux 2.2.2
3.	1993	1 stampante laser Apple "LaserWriter"	1 laser printer Apple "LaserWriter"
4.
5.

Attrezzatura I
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")

Firma ____________________________________________	31/03/1999 13:14:40