Curriculum Vitae et Studiorum di Roberto Bagnara

Table of Contents

• 1  Scheda anagrafica
  • 1.1  Recapiti
  • 1.2  Attuale posizione professionale
  • 1.3  Titoli di studio
  • 1.4  Lingue straniere conosciute
• 2  Curriculum vitae et studiorum
• 3  Descrizione dell'attività didattica
  • 3.1  Titolarità di insegnamenti ufficiali
  • 3.2  Affidamento di insegnamenti ufficiali
  • 3.3  Collaborazioni didattiche
  • 3.4  Attività di relatore e correlatore per tesi di laurea
  • 3.5  Dottorati di ricerca
  • 3.6  Altre attività didattiche
• 4  Descrizione dell'attività di ricerca
  • 4.1  Interessi di ricerca
  • 4.2  Descrizione dei lavori pubblicati
  • 4.3  Software recente
    • 4.3.1  CHINA
    • 4.3.2  OCRA
    • 4.3.3  PPL
    • 4.3.4  PURRS
    • 4.3.5  CLAIR
  • 4.4  Periodi di ricerca congiunta all'estero
  • 4.5  Seminari
  • 4.6  Comitati di programma
  • 4.7  Organizzazione di scuole, conferenze, workshop e seminari
  • 4.8  Attività editoriali
  • 4.9  Attività di referee per riviste internazionali
  • 4.10  Attività di referee per conferenze internazionali
  • 4.11  Partecipazione a progetti di ricerca
    • 4.11.1  Progetti Terminati o in Corso
    • 4.11.2  Progetti Presentati
  • 4.12  Partecipazione a scuole
  • 4.13  Partecipazione a conferenze e workshop nazionali
  • 4.14  Partecipazione a conferenze e workshop internazionali
• 5  Elenco delle pubblicazioni
  • 5.1  Riviste internazionali
  • 5.2  Atti di conferenze internazionali
  • 5.3  Atti di workshop internazionali
  • 5.4  Tesi di dottorato
  • 5.5  Rapporti tecnici
  • 5.6  Altri scritti

1  Scheda anagrafica

1.1  Recapiti

1.2  Attuale posizione professionale

1.3  Titoli di studio

• Diploma di Perito Industriale per le Telecomunicazioni, Istituto Tecnico Industriale di Cesena (FO), anno scolastico 1981--82.
• Laurea con lode in ``Scienze dell'Informazione'', Università degli Studi di Pisa, 17 luglio 1992.
• Dottorato di ricerca in ``Informatica'' (VIII ciclo), Università degli Studi di Pisa, 8 settembre 1997.

1.4  Lingue straniere conosciute

2  Curriculum vitae et studiorum

1982

Consegue il diploma di Perito Industriale per le Telecomunicazioni con la votazione di 52/60.

1983--84

Assolve agli obblighi di leva prestando servizio militare dal 18 maggio 1983 al 7 maggio 1984 presso il II Battaglione Granatieri ``Cengio'', Roma.

1984--87

Prende parte ad un concorso per un posto di Assistente Tecnico presso l'Università di Bologna, vincendolo. Assume servizio il 9 maggio 1984 presso il Dipartimento di Fisica di detta università. Lavora nel gruppo di Fisica Biomedica, divenendo responsabile dello studio e sviluppo dei sistemi di acquisizione dati in tempo reale per gli esperimenti effettuati dal suddetto gruppo. Si occupa inoltre di analisi dei segnali e delle immagini partecipando, in qualità di esperto software, a ricerche riguardanti:

• acquisizione dati ed analisi in tempo reale di segnali cardiaci (in collaborazione con l'ospedale S. Orsola di Bologna);
• acquisizione dati ed analisi in tempo reale di segnali sismici (in collaborazione con il Dipartimento di Geofisica dell'Università di Bologna);
• riconoscimento automatizzato (mediante analisi delle immagini) di cellule cancerose;
• classificazione automatizzata (mediante analisi delle immagini) di particelle, per lo studio della deposizione negli aerosol.

Come parte integrante delle sue mansioni sviluppa un interprete ed un compilatore FORTH usati (sia in ambiente uniprocessor che in ambiente multi-processor con memoria condivisa) per l'acquisizione dati e l'analisi in tempo reale. Partecipa alla costruzione di una rete per la trasmissione di dati tra le apparecchiature di laboratorio e il centro di calcolo del Dipartimento di Fisica. Nell'ambito di questo lavoro sviluppa un programma Kermit per macchine basate sulla famiglia di processori MC680x0. Tale programma è stato usato su processori embedded nei sistemi di acquisizione dati, in sistemi CP/M68K, OS9, VERSADOS e altri [64]. L'implementazione, chiamata ``Kermit68K'', è stata distribuita dal ``Columbia University Center for Computing Activities''. Collabora all'esperimento ``DELPHI'' del CERN (il Laboratorio Europeo per la Fisica delle Particelle), prendendo parte alle attività del gruppo ``DAS'' (Data Acquisition Systems) e occupandosi dello sviluppo di software per la diagnostica automatica dei malfunzionamenti hardware dei sistemi di acquisizione dati. Rassegna le proprie dimissioni volontarie il 31 dicembre 1987.

1988

Viene scelto dal CERN come Technical Student Fellow. L'1 gennaio 1988 inizia il lavoro al CERN (Data Handling Division, Online Computing Group, Readout Architecture Section), prendendo parte allo sviluppo di sistemi real-time, in particolar modo per ciò che concerne il software di base per microprocessori (sistemi di Event Handling e di Asynchronous Service Trap [13, 65]) e il software di supporto per microprocessori (cross-assemblatori, cross-compilatori e pre-processori). Lavora inoltre, insieme a Tim Berners-Lee (il padre del World-Wide Web) ed altri, allo sviluppo di sistemi RPC (Remote Procedure Call) [14, 66] per l'implementazione di sistemi distribuiti. Conclude il suo periodo al CERN il 30 settembre 1988. Continua però il rapporto di collaborazione come consulente esterno ed è di nuovo al CERN dall'1 luglio al 31 agosto 1989.

1988--1992

Frequenta il corso di laurea in Scienze dell'Informazione presso l'Università degli Studi di Pisa, seguendo un piano di studi (indirizzo generale) orientato all'approfondimento delle basi logico-matematiche dell'informatica e dei linguaggi di programmazione.

1992

Il 17 luglio 1992 consegue il diploma di Laurea in Scienze dell'Informazione con la votazione di 110/110 e lode, discutendo la dissertazione dal titolo ``Interpretazione Astratta di Linguaggi Logici con Vincoli su Domini Finiti'' [67]. Relatore: Prof. Giorgio Levi, controrelatore: Prof. Ugo Montanari.

1992

Partecipa come collaboratore a contratto ad attività di ricerca coordinate dal Prof. Giorgio Levi presso il Dipartimento di Informatica dell'Università degli Studi di Pisa nell'ambito di progetti ESPRIT.

1992-1997

Alla fine del 1992 risulta vincitore di due posti dell'ottavo ciclo del Dottorato di Ricerca, rispettivamente in Informatica presso il Dipartimento di Informatica di Pisa e in Matematica Computazionale e Informatica Matematica presso il Dipartimento di Matematica dell'Università di Padova. Esercita opzione per il Dottorato di Ricerca in Informatica. Discute la tesi [44] dinnanzi alla commissione nazionale l'8 settembre 1997 con esito positivo.

1997

Dall'1 gennaio al 31 ottobre svolge l'attività di research fellow presso la School of Computer Studies della University of Leeds (Inghilterra).

1997-2001

Dall'1 novembre 1997 al 15 dicembre 2001 è ricercatore presso il Dipartimento di Matematica dell'Università degli Studi di Parma. In questo periodo inizia a stabilire i contatti che porteranno alla creazione di un piccolo gruppo di ricerca sul tema dell'analisi dei programmi.

2001-presente

Dal 16 dicembre 2001 è professore associato presso il Dipartimento di Matematica dell'Università degli Studi di Parma. Contribuisce, tra l'altro, all'istituzione ed organizzazione del corso di laurea in ``Informatica'' (nuovo ordinamento).

3  Descrizione dell'attività didattica

3.1  Titolarità di insegnamenti ufficiali

1. Programmazione I (1 modulo), corsi di laurea in ``Matematica'', ``Matematica e Informatica'' e ``Matematica per la tecnologia e la finanza'', a.a. 2001--2002.
2. Fondamenti dell'Informatica, corso di laurea in ``Informatica'', a.a. 2002--2003 e 2004--2005.
3. Fondamenti dell'Informatica, corsi di laurea in ``Matematica'' e ``Matematica e Informatica'', a.a. 2003--2004.

3.2  Affidamento di insegnamenti ufficiali

1. Informatica (80 ore), corso di laurea in ``Biotecnologie'' (v.o.), aa.aa. 1999--2000 e 2000--2001.
2. Laboratorio di informatica (1 modulo semestrale), corso di laurea in ``Matematica'' (v.o.), a.a. 2000--2001.
3. Programmazione (metodi avanzati) (2 moduli semestrali), corso di laurea in ``Matematica'' (v.o.), aa.aa. 2000--2001 e 2002--2003.
4. Programmazione 3 corsi di laurea in ``Matematica'' e ``Matematica e Informatica'', a.a. 2002--2003.
5. Scrittura matematica e informatica, corsi di laurea in ``Matematica'' e ``Matematica e Informatica'', a.a. 2002--2003.
6. Scrittura matematica e informatica, corso di laurea in ``Informatica'', aa.aa. 2003--2004 e 2004--2005.
7. Analisi e verifica del software, corso di laurea in ``Informatica'', a.a. 2003--2004 e 2004--2005.

3.3  Collaborazioni didattiche

1. Gruppo di lezioni (8 ore) su ``La compilazione di Prolog e la Warren Abstract Machine'', nell'ambito del corso di Linguaggi Speciali di Programmazione del corso di laurea in ``Scienze dell'Informazione'' dell'Università di Pisa, aa.aa. 1990--1991, 1991--1992, 1992--1993 e 1993--1994, docente: Prof. Giorgio Levi.
   
   
2. Esercitazioni per il corso di ``Linguaggi Formali e Compilatori'' del corso di laurea in ``Scienze dell'Informazione'' dell'Università di Pisa, a.a. 1995--1996, docente: Prof. Pierpaolo Degano.
   
   
3. Lezioni ed esercitazioni teoriche e pratiche per il corso di Teoria ed applicazioni delle macchine calcolatrici (TAMC) del corso di laurea in ``Scienze Ambientali'' dell'Università di Parma, aa.aa. 1997--1998, 1998--1999, 1999--2000 e 2000--2001, docente: Prof. Gianfranco Rossi.
   
   
4. Esercitazioni teoriche e pratiche per il corso di Fondamenti dell'informatica del corso di laurea in ``Matematica'' dell'Università di Parma, aa.aa. 1998--1999 e 1999--2000, docente: Prof. Grazia Lotti.
   
   
5. Lezioni e supporto ai progetti per il corso di Metodologie di Programmazione, del corso di laurea in ``Informatica'' dell'Università di Parma, aa.aa. 2003--2004 e 2004--2005, docente: Dott. Enea Zaffanella.

3.4  Attività di relatore e correlatore per tesi di laurea

1. Motta, M. Un'implementazione efficiente ed innovativa del dominio Pos per l'analisi statica di programmi logici. Tesi di laurea in ``Scienze dell'Informazione''. Relatore: G. Levi; correlatore: R. Bagnara. Università degli Studi di Pisa. a.a. 1994--1995.
2. Scudellari, M. C. Analisi bottom-up di programmi logici con vincoli basata su trasformazioni Magic-Set. Tesi di laurea in ``Scienze dell'Informazione''. Relatore: G. Levi; correlatore: R. Bagnara. Università degli Studi di Pisa. a.a. 1994--1995.
3. Castellacci, B. Implementazione di un'analisi di tipi per programmi logici basata su grammatiche regolari. Tesi di laurea in ``Scienze dell'Informazione''. Relatore: G. Levi; correlatore R. Bagnara. Università degli Studi di Pisa. a.a. 1995--1996.
4. Stazzone, A. Annotazione e trasformazione di programmi logici con vincoli. Tesi di laurea in ``Matematica''. Università degli Studi di Parma, Relatore: R. Bagnara; correlatore: E. Zaffanella. a.a. 1999--2000.
5. Ricci, E. Rappresentazione e manipolazione di poliedri convessi per l'analisi e la verifica di programmi. Tesi di laurea in ``Matematica''. Università degli Studi di Parma. Relatore: R. Bagnara; correlatori: C. Medori ed E. Zaffanella. a.a. 2001--2002.
6. Zolo, T. Risoluzione automatica di relazioni di ricorrenza. Tesi di laurea in ``Matematica''. Università degli Studi di Parma. Relatore: R. Bagnara; correlatori: A. Zaccagnini ed E. Zaffanella. a.a. 2001--2002.
7. Pescetti, A. L'algoritmo di Zeilberger per la risoluzione automatica di ricorrenze. Tesi di laurea in ``Matematica''. Università degli Studi di Parma. Relatore: R. Bagnara; correlatore: A. Zaccagnini. a.a. 2004--2005.

3.5  Dottorati di ricerca

1. Membro del collegio dei docenti del dottorato in ``Matematica, Statistica, Scienze Computazionali e Informatica'', XVI, XVII, XVIII, XIX e XX ciclo, Dipartimento di Matematica dell'Università degli Studi di Milano.

3.6  Altre attività didattiche

1. Lezioni seminariali per il ``Corso di perfezionamento per la formazione degli insegnanti di matematica'' organizzato dalla Facoltà di Scienze MM. FF. NN. dell'Università degli Studi di Parma, aa.aa. 1997--1998 e 1998--1999.
   
   
2. Corso di alfabetizzazione informatica per gli insegnanti delle scuole materne ed elementari di Suvereto (LI), 1999.

4  Descrizione dell'attività di ricerca

4.1  Interessi di ricerca

• Semantica dei linguaggi di programmazione
• Tecniche formali per l'analisi e la verifica dei programmi
• Interpretazione astratta
• Techniche avanzate di compilazione;
• Programmazione logica e con vincoli
• Computer algebra

4.2  Descrizione dei lavori pubblicati

• Nella tesi di Laurea [67] (i cui risultati sono stati in seguito estesi e pubblicati in [15, 31, 32]) è stata studiata l'applicabilità di tecniche per la soluzione approssimata di vincoli, note nel campo dell'Intelligenza Artificiale, all'analisi a tempo di compilazione dei programmi logici con vincoli (CLP). L'idea trae origine dalla necessità di studiare il comportamento di un programma logico con vincoli numerici mediante la sua valutazione su un dominio approssimato di vincoli. Le tecniche di inferenza su grafo e di propagazione di vincoli su reti di vincoli trovano quindi una naturale applicazione nel campo dell'analisi statica di programmi mediante interpretazione astratta.
  
  
• In [15, 31, 32] sono state studiate le applicazioni di queste tecniche all'analisi statica di linguaggi logici con vincoli su domini finiti e sul dominio dei numeri reali, con particolare riferimento alla determinazione di vincoli impliciti e ridondanti. Questo tipo di analisi ha molteplici applicazioni nell'ottimizzazione del procedimento di compilazione di detti linguaggi.
  
  
• In [2, 33] sono state introdotte alcune costruzioni su domini di vincoli. Tali costruzioni consentono, in modo automatico, di ``migliorare'' un dominio dato incorporando informazioni di tipo implicativo e disgiuntivo. Diversi domini interessanti per l'analisi di programmi logici con vincoli posso essere costruiti e giustificati in modo molto semplice facendo ricorso a dette costruzioni. È stato poi mostrato che tali costruzioni danno luogo ad un'algebra di domini di vincoli con proprietà molto interessanti. Questa metodologia per la definizione di nuovi domini di vincoli è utilizzata nella Parma Polyhedra Library [26, 54, 72] ed è stata estesa con operatori di widening generici in [28, 60].
  
  
• Per la parte sperimentale del lavoro di ricerca, hanno giocato un ruolo importante il progetto e la realizzazione dell'analizzatore China [44, 71]. China è un analizzatore data-flow/control-flow per programmi logici con vincoli su domini simbolici (alberi finiti o alberi razionali) e numerici. Il prototipo corrente (circa 40.000 righe di codice C++) ha funzionalità molto estese rispetto agli analizzatori attualmente disponibili. In particolare incorpora combinazioni di domini piuttosto sofisticate (vedi sopra), ottimizzazioni della procedura di calcolo dei punti fissi, informazioni su pattern di chiamata e di successo per mezzo di trasformazione del programma eccetera.
  
  
• In [16, 34] viene affrontato il problema della determinazione incrementale delle variabili ground in analisi basate su alberi binari di decisione (BDD). Tale problema è di estrema rilevanza per molte applicazioni pratiche. Infatti, l'analisi di groundness è di cruciale importanza per l'ottimizzazione di programmi logici e CLP. Inoltre l'incrementalità è necessaria per poter disporre efficientemente di informazioni sulla groundness delle variabili durante l'analisi (e non solo al termine dell'analisi stessa). Tale necessità emerge nell'analisi di linguaggi che impiegano meccanismi di delay (che sono solitamente basati su condizioni di groundness). Un esempio è CLP(R), dove i vincoli non lineari sono sospesi fino al momento in cui diventano lineari. La disponibilità delle informazioni di groundness durante l'analisi permette anche di impiegare, nell'analisi di aliasing, domini computazionalmente meno complessi di Sharing, a parità di precisione (anzi con l'incremento di precisione dovuto al passaggio da Def a Pos) e con significativi vantaggi sull'efficienza complessiva dell'analisi. In [16, 34] vengono esplorate alcune possibili soluzioni, a partire da quelle più semplici, fino ad arrivare ad una rappresentazione ibrida che distingue le variabili ground dalle dipendenze ground. Il risultato è sorprendente: la rappresentazione ibrida è sensibilmente più efficiente delle rappresentazioni usuali ``pure'' (ovvero basate solo su BDD). E questo a prescindere dal fatto che si sia interessati o meno alle informazioni di groundness nel corso dell'analisi. Ad essere migliorata è l'efficienza dell'analisi di groundness in sé stessa, sia in termini di velocità di esecuzione che (ed ancor più) in termini di memoria utilizzata. Il fatto che la rappresentazione ibrida consenta l'accesso in tempo costante (e molto efficiente) alle variabili ground dà poi luogo ad ovvi ed ulteriori vantaggi.
  
  In [19, 38] quest'idea viene spinta oltre, separando le informazioni sull'equivalenza di coppie di variabili. Due variabili sono equivalenti se sono entrambe ground o entrambe non ground. La nuova rappresentatione ibrida che deriva da questa ulteriore fattorizzazione, grazie ad uno sforzo implementativo molto accurato ed attento, è nettamente più efficiente di ogni altro approccio. L'analisi di programmi sul dominio Pos è stata resa più veloce, su programmi di media grandezza, di un ordine di grandezza e più. Non solo: programmi di grandi dimensioni che prima non erano assolutamente trattabili con Pos ora sono analizzabili in tempi del tutto ragionevoli.
  
  
• In [35] viene presentata una caratterizzazione semantica adatta a catturare non solo i linguaggi CLP ``ideali'', ma anche i linguaggi realmente implementati e, in particolare quei sistemi che, per ragioni di efficienza, impiegano un risolutore di vincoli incompleto (CLP(R) e clp(fd), ad esempio). La semantica presentata in [35] è una versione, riveduta e corretta in alcuni punti cruciali, di quella introdotta da Jaffar e Maher. In [35] vengono messe in luce l'importanza e la ragionevolezza di un'ipotesi di incrementalità del risolutore di vincoli (il risultato del risolutore non dipende dal fatto che un certo numero di vincoli gli sia presentato in blocco o uno alla volta). Sotto questa condizione la semantica definita in [35], con caratterizzazioni sia top-down che bottom-up: è AND-composizionale (i vincoli di risposta a goal qualsiasi possono essere ricostruiti a partire dai vincoli di risposta a goal atomici più generali); non perde la distinzione tra vincoli attivi (inviati al risolutore di vincoli) e passivi (ovvero sospesi). Viene inoltre mostrato che l'ipotesi di incrementalità è cosí ragionevole che, senza di essa, è impossibile definire una semantica basata su atomi che sia, al tempo stesso, AND-composizionale e indipendente dalla regola di calcolo.
  
  
• L'obiettivo dell'analisi di sharing per i programmi logici è quello di determinare, per ogni punto del programma, quali coppie di variabili logiche possono essere legate a termini che condividono una terza variabile logica. Il dominio normalmente utilizzato per detta analisi (Sharing, Jacobs e Langen, 1989) caratterizza invece gli insiemi di variabili che possono condividere una variabile. In [3, 17] ci si chiede, per la prima volta, se questo dominio (oramai standard) non sia forse inutilmente complesso per l'analisi di sharing. La risposta è positiva: definendo una relazione di equivalenza su Sharing siamo in grado di ottenere un dominio più semplice, riducendo la complessità (nel caso peggiore) della procedura di unificazione da esponenziale a polinomiale. Si dimostra inoltre che il nuovo dominio (in seguito denominato PSD, per Pair-Sharing Dependencies) non può essere ulteriormente astratto senza incorrere in perdite di precisione dell'analisi corrispondente.
  
  
• Naturalmente, è importante che gli analizzatori statici siano basati su risultati teorici dimostrati in modo convincente. In programmazione logica, il dominio Sharing, come si è detto, è una scelta pressoché standard per l'analisi di sharing e per ulteriori studi teorici. A dispetto di ciò si è riscontrato che non esistevano, prima della pubblicazione dei lavori [4, 18, 39], dimostrazioni soddisfacenti delle proprietà chiave, commutatività ed idempotenza, che rendono Sharing ben definito. Inoltre, le prove o congetture pubblicate circa la correttezza di Sharing presumono che il linguaggio analizzato implementi l'unificazione con l'occur-check, il ché è falso nella quasi totalità dei casi. I lavori [4, 18, 39] chiudono queste falle, rimaste aperte per quasi un decennio. In particolare, viene data una generalizzazione della funzione di astrazione di Sharing che può essere applicata ad ogni linguaggio, con o senza l'occur-check. Oltre a questo, vengono dimostrati i risultati di correttezza, idempotenza e commutatività per l'operazione di unificazione astratta.
  
  
• Avendo constatato che né il dominio Sharing di Jacobs e Langen, né la sua astrazione PSD descritta in [3, 17, 37] consentono di analizzare programmi di grandi dimensioni, in [20, 41, 47] è stato studiato il dominio proposto da C. Fecht, formato dalla combinazione del dominio Pos con un'astrazione molto debole di Sharing. Sebbene questa combinazione rappresenti un buon compromesso tra precisione ed efficienza, si sono riscontrate perdite di precisione significative nell'analisi di parecchi programmi ``reali''. Questa perdita di precisione concerne la groundness, il pair-sharing, la linearità, ma non la freeness: prendendo spunto da questa osservazione empirica, si è dimostrato formalmente che una famiglia piuttosto ampia di astrazioni di Sharing non comporta perdite di precisione sulla freeness. In [20, 41, 47] si definisce un nuovo dominio per l'analisi di sharing che supporta l'implementazione di svariate tecniche di widening. In particolare, con questo dominio risulta semplice utilizzare l'idea di Fecht per realizzare un widening vero e proprio. Sono stati considerati anche widening più precisi, ma la sperimentazione estensiva che condotta suggerisce come sia difficile migliorare il primo widening proposto, a patto che il dominio Pos sia incluso nel dominio complessivo. Quando questo non è il caso, widening più precisi basati su clique nei grafi di pair-sharing consentono di ottenere una migliore precisione a costi assolutamente accettabili.
  
  
• La complementazione, e cioè l'operazione inversa del prodotto ridotto, rappresenta una tecnica relativamente nuova per la determinazione di decomposizioni minimali dei domini astratti. Filé e Ranzato hanno introdotto un metodo particolarmente semplice per il calcolo del complemento. Tra le applicazioni del loro metodo, essi hanno considerato la rimozione per complementazione del dominio di pair-sharing (PS) dal dominio di set-sharing di Jacobs e Langen's (Sharing). Dal momento che il risultato di questa operazione è lo stesso Sharing, Filé e Ranzato ne hanno concluso che il dominio PS è ``troppo astratto'' per lo scopo che si erano prefissi.
  
  In [5, 21, 48] si mostra come la radice di queste difficoltà non stia in PS, ma in Sharing e, più precisamente, nell'informazione ridondante che Sharing contiene rispetto alle dipendenze ground e al pair-sharing. Infatti, le difficoltà svaniscono se la nostra versione non ridondante di Sharing, PSD [3, 5, 17, 37], viene utilizzata in luogo di Sharing. Per stabilire questo risultato su PSD, abbiamo definito uno schema generale per sottodomini di Sharing che include Def (un dominio per l'analisi di groundness) e PSD come casi particolari. Questo getta nuova luce sulla struttura di Sharing e svela una connessione naturale, sebbene inattesa, tra Def e PSD.
  
  In [5, 21, 48], inoltre, viene data sostanza all'affermazione del fatto che la complementazione, da sola, non è sufficiente per ottenere decomposizioni veramente minimali. La soluzione giusta a questo problema consiste prima nella rimozione delle ridondanze attraverso il calcolo del quoziente del dominio rispetto al comportamento osservabile, e poi nella decomposizione per complementazione.
  
  
• In [23, 36, 49] è presentata la costruzione razionale di un dominio generico con informazione strutturale per l'analisi di programmi CLP. Il dominio proposto, Pattern(D), ha come parametro un qualsiasi dominio astratto, D, che soddisfi alcuni requisiti assolutamente ragionevoli. Il dominio discende dal dominio parametrico per l'analisi di programmi logici Pat(Â) introdotto da A. Cortesi e colleghi. D'altra parte, la formalizzazione del nostro dominio astratto per l'analisi di programmi CLP è indipendente dalla tecnica di implementazione: Pat(Â) (opportunamente esteso per trattare correttamente i linguaggi CLP che omettono l'occurs-check nella procedura di unificazione) è una delle possibili implementazioni. Ragionando ad un più alto livello di astrazione siamo in grado di riferirci a nozioni classiche della teoria dell'unificazione e di consentire all'implementatore una notevole libertà d'azione. Infatti, come dimostriamo in [36, 23, 49], un analizzatore che incorpori informazione strutturale basandosi sul nostro approccio può essere estremamento competitivo, non solo dal punto di vista della precisione, ma anche dal punto di vista dell'efficienza.
  
  
• Riguardo la precisione delle combinazioni di domini che includono il dominio Sharing di Jacobs e Langen, esiste un piccolo nucleo di tecniche, quali la combinazione standard con informazioni di linearità e di freeness, solitamente denotata con SFL, che sono oramai ampiamente accettate ed utilizzate. Esistono diverse altre proposte per il raffinamento di Sharing. Queste proposte, che sono circolate nella comunità scientifica più o meno inosservate per anni, sono accomunate dal fatto che nessuna di esse sembra essere stata convalidata sperimentalmente dai rispettivi autori. Per questa ragione, come parte del nostro sforzo di spingere la precisione dell'analisi oltre i limiti attuali, in [8, 22, 40] ci si è posti il problema di verificare se e quanto dette proposte possono contribuire ad un effettivo miglioramento della precisione. In particolare, in [8, 22, 40] sono state discusse e/o valutate sperimentalmente le seguenti possibilità:
  1. l'effetto della propagazione su SFL delle variabili ground identificate da Pos;
  2. l'incorporazione di informazione strutturale esplicita nel dominio di analisi;
  3. tecniche più sofisticate per integrare SFL e Pos;
  4. la questione del riordinamento dei binding nel calcolo dell'operatore mgu astratto;
  5. una proposta originale concernente l'aggiunta di un dominio che mantenga informazioni sull'insieme di variabili che sono ground o free;
  6. una tecnica raffinata per utilizzare le informazioni di linearità;
  7. la possibilità di migliorare la precisione dell'analisi mantenendo informazioni sulla compoundness delle variabili (in questo contesto, una variabile è detta compound se è certamente legata ad un termine che non è una variabile);
  8. il recupero di ``informazione nascosta'' nella combinazione di Sharing con l'usuale dominio per la freeness.
  
  
  
• Le attrattive dei linguaggi logici basati sulla teoria degli alberi razionali (come Prolog II ed i suoi successori, SICStus Prolog e Oz) sono:
  1. l'espressività con cui consentono la codifica di grammatiche ed altri oggetti autoreferenziali;
  2. l'efficienza della procedure di unificazione, che non richiede l'occurs-check senza per questo rinunciare alla correttezza.
  Sfortunatamente, l'uso degli alberi razionali infiniti è causa di problemi seri. Ad esempio, molti predicati built-in e di libreria sono indefiniti per tali alberi e la loro applicazione deve quindi essere soggetta a controlli che, se svolti a tempo di esecuzione, comportano costi computazionali significativi. Inoltre, diverse tecniche di analisi e manipolazione dei programmi sono corrette limitatamente a quelle parti di programma o a quelle esecuzioni che, dimostrabilmente, sono interessate solo da alberi finiti. È perció importante conoscere almeno in parte, automaticamente e staticamente, quelle variabili (le variabili finite) che, nei punti del programma di interesse, saranno sempre legate a termini finiti.
  
  In [24, 50] viene proposta una nuova analisi data-flow che, formalizzata in termini di interpretazione astratta, cattura questa informazione. Il dominio è parametrico: una semplice componente per registrare l'insieme delle variabili finite viene accoppiato ad un dominio generico (il parametro della costruzione) che fornisce informazioni di sharing. Quest'ultimo dominio è specificato in modo astratto cosí da garantire la correttezza del dominio composito e, al tempo stesso, la generalità dell'approccio.
  
  In [25, 51] viene introdotto un dominio di funzioni Booleane che esprime, in modo piuttosto preciso, come la finitezza di una variabile influenzi la finitezza di altre variabili. La verifica sperimentale che abbiamo condotto mostra come la combinazione dei domini descritti in [24, 50] e in [25, 51] fornisca un metodo valido (ovvero applicabile a programmi reali) per ottenere precise informazioni sulla finitezza dei termini coninvolti nelle computazioni di programmi logici con vincoli.
  
  Un lavoro che combina ed estende le idee di [24, 25, 50, 51] è in corso di pubblicazione su rivista [7, 61].
  
  
• Il dominio dei poliedri convessi riveste un ruolo fondamentale in molte applicazioni per l'analisi statica e la verifica (semi-) automatica di sistemi hardware e software. In [26, 54] vengono evidenziate alcune problematiche relative alla rappresentazione e manipolazione dei poliedri convessi non necessariamente chiusi, per i quali le librerie software esistenti offrono un supporto inadeguato. Viene affrontato e risolto il problema della rappresentazione ad alto livello di tali poliedri per mezzo del metodo della Doppia Descrizione (introdotto da Motzkin e colleghi), rendendola indipendente dalla particolare tecnica di implementazione utilizzata. Inoltre, per l'implementazione basata su e-rappresentazioni introdotta da Halbwachs e colleghi, viene mostrato come l'algoritmo standard di minimizzazione della rappresentazione fornisca risultati insoddisfacenti, aprendo la strada ad inefficienze evitabili e possibili errori di programmazione. Per risolvere il problema evidenziato, viene definito un concetto più forte di minimizzazione, specificando e dimostrando corretto l'algoritmo corrispondente.
  
  In [42, 43] viene proposta una generalizzazione dell'implementazione dei poliedri NNC basata sulla e-rappresentazione, consentendo di apprezzarne meglio le potenzialità ed i limiti. In particolare, si mostra l'esistenza di una rappresentazione alternativa, che risulta avere caratteristiche computazionali duali rispetto a quella originale. I risultati presentati in [26, 42, 43], completi delle dimostrazioni formali ed esposti in un contesto omogeneo, sono raccolti in [11], attualmente in corso di stampa su rivista.
  
  
• Gli operatori di widening, la cui formalizzazione si deve a Patrick e Radhia Cousot, consentono di forzare e/o accellerare la convergenza del calcolo dell'analisi statica nel caso in cui siano impiegati domini astratti infiniti o computazionalmente troppo costosi. Nel caso del dominio dei poliedri, l'unico operatore di widening formalizzato ed utilizzato nella pratica è quello proposto da Cousot ed Halbwachs nel 1978, che giustamente prende il nome di widening standard. Tale operatore, però, risulta essere troppo impreciso per gli scopi di alcune applicazioni dell'analisi statica. Sebbene alcuni operatori più precisi siano stati proposti in letteratura, questi non sono veri e propri widening, in quanto non garantiscono la convergenza della computazione in un tempo finito. Per ovviare a questo problema, in [27, 57] si definisce uno schema generale per la definizione di nuovi widening sul dominio dei poliedri. Usando tale schema, una o più euristiche di approssimazione possono essere sistematicamente trasformate in operatori di widening più precisi del widening standard. Lo schema è stato istanziato considerando sia operatori già proposti in letteratura, sia operatori inediti: il widening ottenuto, all'atto pratico, è stato verificato essere più preciso del widening standard per una percentuale significativa dei benchmarks considerati. La versione estesa del lavoro presentato in [27, 57] è stata recentemente accettata per la pubblicazione su rivista [10].
  
  
• Uno dei successi finora ottenuti con la Parma Polyhedra Library è costituito dalla suo utilizzo in cTI, il primo sistema per l'inferenza di terminazione universale left per programmi logici. L'inferenza di terminazione generalizza sia l'analisi che il controllo di terminazione. Tradizionalmente, un analizzatore di terminazione tenta di dimostrare che una data classe di interrogazioni di un programma logico termina. Questa classe deve essere fornita all'analizzatore, generalmente per mezzo di annotazioni che l'utente deve inserire. Naturalmente, l'analisi deve essere rieseguita ogni volta che la classe di interrogazioni viene modificata. L'inferenza di terminazione, al contrario, non richiede né le annotazioni dell'utente, né il ricalcolo. Infatti, con questo approccio, la classe di interrogazioni che l'analisi riuscirebbe a dimostrare essere terminanti viene inferita in un colpo solo. In [9] viene descritta l'architettura della nuova versione di cTI e vengono riportati i risultati di un'estensiva valutazione sperimentale del sistema che raccoglie molti esempi classici della letteratura sulla terminazione in programmazione logica e diversi programmi Prolog di dimensione e complessità assolutamente rispettabili. Grazie alla Parma Polyhedra Library la nuova versione di cTI è fino a due ordini di grandezza più efficiente della precedente implementazione.
  
  
• La progettazione ed implementazione di domini astratti espressivi ed efficienti per l'analisi data-flow e la verifica dei sistemi informatici sono compiti ardui. Per questo motivo, continua ad esservi un grande interesse nei confronti di quelle metodologie che consentono di derivare un dominio astratto complesso applicando costruzioni sistematiche a domini astratti più semplici già esistenti. Di importanza chiave sono quelle tecniche che consentono di derivare, in modo automatico o quasi, degli operatori semantici corretti (anche se potenzialmente non ottimali) per i nuovi domini astratti. In questo contesto, la derivazione automatica degli operatori di widening merita una attenzione particolare, in quanto detti operatori devono anche garantire la convergenza dell'analisi, oltre alla sua correttezza. In [28, 60] vengono proposte due tecniche alternative per specificare operatori di widening generici per un dominio astratto ottenuto per mezzo della costruzione finite powerset (la quale consente di rappresentare tutte le disgiunzioni finite di elementi del dominio astratto di partenza). Entrambi gli operatori sono ottenuti a partire da un qualunque operatore di widening definito sul domino sottostante e sono parametrici rispetto alla specifica di alcune operazioni supplementari. Al fine di meglio esemplificare l'uso delle tecniche proposte, ne viene illustrata la loro istanziazione sul dominio finite powerset dei poliedri convessi, per il quale nessun operatore di widening (non banale) è stato proposto precedentemente. La versione estesa del lavoro [60], attualmente sottomessa per la pubblicazione su rivista, oltre alla dimostrazione dei risultati formali enunciati in [28], contiene anche la specifica di una terza tecnica per la derivazione automatica di un operatore di widening.
  
  
• L'obiettivo dell'analisi di complessità dei programmi è la determinazione di approssimazioni inferiori e superiori di misure di complessità di algoritmi, processi e strutture dati. Quando queste analisi sono parzialmente o completamente automatizzate, esse possono essere di supporto al programmatore nella comprensione dei programmi, guidare l'applicazione di trasformazioni per l'ottimizzazione di programmi e condurre alla scoperta di problemi di efficienza dovuti ad errori di programmazione molto difficilmente individuabili in altro modo. Le relazioni di ricorrenza giocano un ruolo molto importante nell'analisi di complessità dei programmi, dal momento che le misure di complessità si possono spesso e convenientemente esprimere per mezzo di sistemi di relazioni di ricorrenza. Il progetto Purrs (Parma University's Recurrence Relation Solver) ha per obiettivo la creazione di una libreria software in grado di risolvere od approssimare le relazioni di ricorrenza, con particolare riferimento all'analisi di complessità dei programmi. Il lavoro di ricerca finora svolto ha portato alla definizione di alcuni algoritmi che, in modo completamente automatico e sostanzialmente efficiente, consentono la soluzione o l'approssimazione (sia dall'alto che dal basso) di un'ampia classe di relazioni di ricorrenza. In particolare, sono state considerate le seguenti classi di relazion idi ricorrenza:
  • ricorrenze lineari di ordine finito a coefficienti costanti [58];
  • ricorrenze lineari di ordine 1 a coefficienti variabili;
  • una sottoclasse delle ricorrenze lineari di ordine infinito;
  • forme speciali di ricorrenze non lineari;
  • le cosiddette equazioni funzionali di rango 1, che scaturiscono dall'analisi di complessità degli algoritmi divide-et-impera.
  Per fare un esempio, consideriamo la ricorrenza lineare di ordine k data da
    x(n) = a₁ x(n-1) + ··· + a_k x(n-k) + p(n).     (1)
  Al momento attuale, Purrs è in grado di risolvere esattamente relazioni di ricorrenza lineari a coefficienti costanti di ordine fino a 4 (oltre a quelle di ordine più grande per cui sia possibile determinare le radici del polinomio caratteristico l^k - (a₁ l^k-1 + ··· + a_k)), se la parte non omogenea p è una combinazione lineare di prodotti di polinomi ed esponenziali. In realtà, è già possibile determinare la soluzione di alcune speciali ricorrenze del tipo (1) anche quando l'ordine è 1 e p è una funzione razionale (ad esempio, Purrs è in grado di trovare la formula chiusa per la somma parziale n-esima della serie di Mengoli), ed anche risolvere una classe di relazioni di ricorrenza lineari di ordine 1 a coefficienti variabili, oppure dimostrare automaticamente che non esiste una formula chiusa per la soluzione.
  
  Inoltre, Purrs riesce a determinare l'ordine di grandezza corretto della soluzione di una classe di ricorrenze generalizzate del tipo
    x(n) = a x(n / b) + g(n),     (2)
  dove a > 0, b > 1 è intero, e g è una combinazione lineare di prodotti di polinomi ed esponenziali e di prodotti di polinomi e funzioni logaritmiche. (Qui x(n/b) deve essere inteso come x(ë n/b û)). Queste ultime ricorrenze scaturiscono naturalmente nell'analisi di complessità di algoritmi divite et impera. Si noti che per le ricorrenze del tipo (2) può accadere un fenomeno che non capita alle soluzioni delle ricorrenze del tipo (1): per esempio, se a = b = 2, g(n) = 0 ed x(1) = 1, allora

  liminf n ® ¥

  x(n) 2n

  =

  1 2

  ,

  limsup n ® ¥

  x(n) 2n

  = 1,

  dato che x( 2^m + a ) = 2^m, se 0 £ a < 2^m. In altre parole, il rapporto fra la soluzione di questa ricorrenza generalizzata ed il suo termine dominante non ha limite, ma oscilla fra due quantità positive e finite. Per questo tipo di ricorrenze ed una vasta classe di funzioni g sono state ottenute approssimazioni della soluzione dell'ordine di grandezza corretto, cioè due funzioni ``semplici'' x₁(n) ed x₂(n) tali che x₁(n) £ x(n) £ x₂(n) per ogni n ³ 1, e che

  L1 =

  liminf n ® ¥

  x(n) x1(n)

  > 0,      L2 =

  limsup n ® ¥

  x(n) x2(n)

  < + ¥.

  Quando g(n) = n^k aⁿ, il sistema Purrs determina le funzioni x₁ ed x₂ in modo che il rapporto L₂ / L₁ sia il più piccolo possibile, ferma restando la condizione x₁(n) £ x(n) £ x₂(n) per ogni n ³ 1. Per fare questo si sono dovuti estendere in varie direzioni i risultati già noti, che riguardavano quasi esclusivamente la determinazione di maggiorazioni per la soluzione di ricorrenze di tipo (7) della forma x(n) = O(x₂(n)) , senza preoccuparsi né del valore della costante implicita nella notazione di Landau, né di dare le corrispondenti minorazioni. È in preparazione una serie di articoli che conterranno una descrizione completa della parte matematica del progetto, sia nelle sue parti originali che in quelle già note. La prima parte è ultimata e già pubblicata [58].
  
  Uno dei problemi che sono sorti durante lo sviluppo di Purrs è il seguente: dal momento che le soluzioni in forma chiusa di ricorrenze anche modeste possono essere molto complesse, come possiamo acquistare confidenza nel nostro risolutore? Come possiamo validare o forse confutare i risultati che questo fornisce? Inoltre, in quei casi in cui le soluzioni esatte sono cosí complesse da essere inutilizzabili, come possiamo cedere precisione in cambio di semplicità approssimandole dall'alto e dal basso? E infine, riguardo al problema di gestire insiemi di soluzioni di relazioni di ricorrenza: come possiamo confinare tali insiemi per mezzo di limitazioni inferiori e superiori? In [59] vengono date alcune soluzioni a questi problemi, facendo attenzione, ove possibile, ad utilizzare solo aritmetica intera e/o condizioni che possono essere controllate molto efficientemente e in modo completamente automatico. La valutazione sperimentale di queste idee sta dando risultati molto promettenti, con speedup di un ordine di grandezza e più rispetto ai metodi tradizionali. Grazie a questo lavoro, Purrs è in grado, in un gran numero di casi, di certificare rapidamente la correttezza della soluzione determinata, verificando che soddisfa le condizioni iniziali e la relazione di ricorrenza.

4.3  Software recente

4.3.1  CHINA

4.3.2  OCRA

4.3.3  PPL

4.3.4  PURRS

4.3.5  CLAIR

• analisi lessicale;
• analisi sintattica e generazione dell'albero di sintassi astratta (parsing);
• controllo statico della correttezza rispetto ai tipi;
• semantica operazionale mediante sistema di transizioni;
• interpretazione (concreta);
• interpretazione astratta ed analisi statica;
• compilazione.

4.4  Periodi di ricerca congiunta all'estero

1. Technical Student Fellow presso il CERN (European Organization for Nuclear Research) di Ginevra (Svizzera), dall'1 gennaio al 30 settembre 1988.
   
   
2. Visiting researcher presso il Department of Computer Science della Monash University di Melbourne (Australia), dal 14 gennaio al 16 febbrario 1995.
   
   
3. Research fellow presso la School of Computer Studies della University of Leeds (Inghilterra), dall'1 gennaio al 31 ottobre 1997.
   
   
4. A partire dal 1998, ha visitato numerose volte (almeno una settimana ogni anno) la School of Computing della University of Leeds, dove collabora ad attività di ricerca con Patricia Hill.
   
   
5. Nell'ambito del programma di scambio docenti previsto dal protocollo culturale tra Italia e Spagna, ha effettuato una visita di studio, finanziata dal MURST, presso la Facultad de Informática, Universidad Politécnica de Madrid, collaborando con il gruppo del Prof. Manuel Hermenegildo, dal 27 gennaio al 2 febbraio 2001.
   
   
6. Nell'ambito del progetto ``Ambienti Avanzati per lo Sviluppo di Programmi Logici'' (Azioni Integrate Italia-Spagna 2001, codice IT229), ha effettuato visite di studio di una settimana l'una presso la Facultad de Informática, Universidad Politécnica de Madrid, nel novembre 2001, settembre 2002 e maggio 2003.
   
   
7. Professeur invité presso il Département de Mathématiques et Informatique della Université de La Réunion, S^t Denis (Oceano Indiano, Francia), per i mesi di maggio 2002 e giugno 2005.

4.5  Seminari

1. ``Introduzione alla Warren Abstract Machine'', Dipartimento di Informatica, Università di Pisa, marzo 1991.
   
   
2. english``Data-Flow Analysis for Constraint Logic-Based Languages'', School of Computer Studies, University of Leeds, marzo 1997.
   
   
3. ``Analisis eficiente de informacion estructural para lenguajes de programacion logica y de restricciones'', Departamento de Inteligencia Artificial, Universidad Politécnica de Madrid, gennaio 2001.
   
   
4. ``Widening Sharing'', Departamento de Inteligencia Artificial, Universidad Politécnica de Madrid, gennaio 2001.
   
   
5. english``The Parma Polyhedra Library'', Institut de Recherche en Mathématiques et Informatique Appliquées, Université de La Réunion, maggio 2002.
   
   
6. english``Symbolic Computation Support for Complexity Analysis and the PURRS Project'', Facultad de Informática, Universidad Politécnica de Madrid, maggio 2003.
   
   
7. english``Convex Polyhedra for the Analysis and Verification of Hardware and Software Systems: the `Parma Polyhedra Library'', Dipartimento di Matematica, Università di Parma, dicembre 2003.
   
   
8. english``Representation and Manipulation of Not Necessarily Closed Convex Polyhedra'', Dipartimento di Matematica, Università di Parma, febbraio 2004.
   
   
9. ``Abstract Interpretation and the Parma Polyhedra Library: from Theory to Practice and Vice Versa'', Dipartimento di Informatica, Sistemi e Produzione, Università degli Studi di Roma ``Tor Vergata'', novembre 2004.

4.6  Comitati di programma

1. Membro del comitato di programma della ``2000 Joint Conference on Declarative Programming'', La Habana, Cuba, 4--7 dicembre, 2000.
   
   
2. Membro del comitato di programma del tredicesimo ``Workshop on Logic Programming Environments'', Mumbai, India, 8 dicembre 2003.
   
   
3. Membro del comité de lecture della tredicesima edizione delle ``Journées Francophones de Programmation en Logique et de programmation par Contraintes'' (JFPLC 2004), Angers, Francia, 21--23 giugno 2004,
   
   
4. Membro del comitato di programma del quattordicesimo ``International Symposium on Logic-based Program Synthesis and Transformation'' (LOPSTR'05), Londra, Regno Unito, 7--9 settembre 2005.
   
   
5. Membro del comitato di programma della ventunesima ``International Conference on Logic Programming'' (ICLP'05), Barcellona, Spagna, 2--5 ottobre 2005.

4.7  Organizzazione di scuole, conferenze, workshop e seminari

1. Workshop Chair per i ``Joint International Symposia SAS'98 and PLILP-ALP'98'', Pisa, Italia, 14--18 settembre 1998.
   
   
2. Organizzatore, insieme a Patricia Hill della University of Leeds della ``Second International Summer School on Computational Logic'', Maratea, Italia, 25--30 agosto 2002 (http://www.cs.unipr.it/ISCL02).
   
   
3. Organizzatore del ciclo di seminari su ``Convex Polyhedra for the Analysis and Verification of Hardware and Software Systems'', Dipartimento di Matematica, Università di Parma, novembre 2003 --- febbraio 2004 (http://www.cs.unipr.it/ppl/seminars_2003_2004).
   
   
4. Membro del comitato organizzatore del CILC'04 -- Convegno Italiano di Logica Computazionale, diciannovesimo incontro annuale della ``Associazione Italiana Gruppo Ricercatori e Utenti di Logic Programming'' (GULP), Dipartimento di Matematica, Università di Parma, 16--17 giugno 2004 (http://www.cs.unipr.it/CILC04).

4.8  Attività editoriali

1. Implementation Area Editor e curatore della sezione Net Talk per 'ALP newsletter, il bollettino della Association for Logic Programming.

4.9  Attività di referee per riviste internazionali

1. Journal of Logic Programming;
   
   
2. Journal of Functional and Logic Programming;
   
   
3. Information Processing Letters.

4.10  Attività di referee per conferenze internazionali

1. GULP'93, ``Ottavo Convegno sulla Programmazione Logica'', Gizzeria Lido (CZ), giugno 1993.
   
   
2. AMAST'93, ``Algebraic Methodology and Software Technology'', Enschede, Olanda, giugno 1993.
   
   
3. WSA'93, ``3rd International Workshop on Static Analysis'', Padova, settembre 1993.
   
   
4. ILPS'93, english``International Logic Programming Symposium'', Vancouver, British Columbia, Canada, ottobre 1993.
   
   
5. AI*IA'93, ``Terzo Congresso dell'Associazione Italiana per l'Intelligenza Artificiale'', Torino, ottobre 1993.
   
   
6. SAC'94, ``ACM Symposium on Applied Computing'', Phoenix, Arizona, USA, marzo 1994.
   
   
7. ICLP'94, ``International Conference on Logic Programming'', S. Margherita Ligure, giugno 1994.
   
   
8. PLILP'94, ``Programming Languages Implementation and Logic Programming'', Madrid, Spagna, settembre 1994.
   
   
9. ALP'94, ``Third International Conference on Algebraic and Logic Programming'', Madrid, Spagna, settembre 1994.
   
   
10. GULP-PRODE'94, ``Joint Conference on Declarative Programming'', Peñíscola, Spagna, settembre 1994.
    
    
11. SAS'94, ``International Static Analysis Symposium'', Namur, Belgio, settembre 1994.
    
    
12. PLILP'95, ``International Symposium on Programming Languages, Implementations, Logics and Programs'', Utrecht, Paesi Bassi, settembre 1995.
    
    
13. ILPS'95, ``International Logic Programming Symposium'', Portland, Oregon, USA, dicembre 1995.
    
    
14. ESOP'96, ``European Symposium on Programming'', Linköping, Svezia, aprile 1996.
    
    
15. ECAI'96, ``European Conference on Artificial Intelligence'' Budapest, Ungheria, agosto 1996.
    
    
16. PLILP'96, ``Eighth International Symposium on Programming Languages, Implementations, Logics, and Programs'', Aachen, Germania, settembre 1996.
    
    
17. SAS'96, ``Third International Static Analysis Symposium'', Aachen, Germania, settembre 1996.
    
    
18. LOPSTR'97, ``Seventh International Workshop on Logic Program Synthesis and Transformation'', Leuven, Belgio, luglio 1997.
    
    
19. JICSLP'98, ``Joint International Conference and Symposium on Logic Programming'' Manchester, Regno Unito, giugno 1998.
    
    
20. SAS'98, ``Fifth International Static Analysis Symposium'', Pisa, Italia, settembre 1998.
    
    
21. PLILP/ALP'98, ``Tenth International Symposium on Programming Languages, Implementations, Logics and Programs'' and ``Seventh International Conference on Algebraic and Logic Programming'', Pisa, Italia, settembre 1998.
    
    
22. SAS'99, ``International Static Analysis Symposium'', Venezia, Italia, settembre 1999.
    
    
23. PPDP'99, ``International Conference on Principles and Practice of Declarative Programming'', Parigi, Francia, settembre/ottobre 1999.
    
    
24. SAS 2000, ``Seventh International Static Analysis Symposium'', Santa Barbara, USA, giugno/luglio 2000.
    
    
25. ESSLLI-2000, ``Twelfth European Summer School in Logic, Language and Information'', student session, Birmingham, Regno Unito, agosto 2000.
    
    
26. APPIA-GULP-PRODE'00, ``2000 Joint Conference on Declarative Programming'', La Havana, Cuba, dicembre 2000.
    
    
27. LPAR 2000, ``Seventh International Conference on Logic for Programming and Automated Reasoning'', Isola della Réunion, Oceano Indiano, novembre 2000.
    
    
28. LPAR 2001, ``Eighth International Conference on Logic for Programming, Artificial Intelligence and Reasoning'', La Havana, Cuba, dicembre 2001.
    
    
29. SAS'02, ``Ninth International Static Analysis Symposium'', Madrid, Spagna, settembre 2002.
    
    
30. ESOP'03, ``European Symposium on Programming'', Varsavia, Polonia, aprile 2003.
    
    
31. SAS'03, ``Tenth International Static Analysis Symposium'', San Diego, California, USA, giugno 2003.
    
    
32. PSI'03, ``Perspectives of System Informatics'', Novosibirsk, Akademgorodok, Russia, luglio 2003.
    
    
33. APPIA-GULP-PRODE'03, ``2003 Joint Conference on Declarative Programming'', Reggio Calabria, Italia, settembre 2003.
    
    
34. WLPE'03, ``13th Workshop on Logic Programming Environments'', Mumbai, India, dicembre 2003.
    
    
35. VMCAI'04, ``Fifth International Conference on Verification, Model Checking and Abstract Interpretation'', Venezia, Italia, gennaio 2004.
    
    
36. ESOP'04, ``European Symposium on Programming'', Barcellona, Spagna, marzo--aprile 2004.
    
    
37. SAS'04, ``Eleventh International Static Analysis Symposium'', Verona, Italia, agosto 2004.
    
    
38. CAV'05, ``Seventeenth International Conference on Computer Aided Verification'', The University of Edinburgh, Scozia, UK, luglio 2005.

4.11  Partecipazione a progetti di ricerca

4.11.1  Progetti Terminati o in Corso

1. Partecipa al progetto ESPRIT Basic Research Action Project n. 6707, ``ParForce''.
   
   
2. Partecipa al programma di ricerca cofinanziato dal MURST intitolato ``Certificazione automatica di programmi mediante interpretazione astratta'' (1999--2001, coordinatore nazionale: Prof. Roberto Giacobazzi, Università di Verona).
   
   
3. Partecipa al programma di ricerca cofinanziato dal MURST intitolato ``Interpretazione astratta, sistemi di tipo e analisi control-flow'' (2000--2002, coordinatore nazionale: Prof. Giorgio Levi, Università di Pisa).
   
   
4. Nell'ambito delle Azioni Integrate Italia-Spagna 2001 coordina, per la parte italiana, il progetto biennale dal titolo ``Ambienti avanzati per lo sviluppo di programmi logici'' (IT229). Coordinatore per la parte spagnola: Prof. Germán Puebla Sánchez, Facultad de Informática, Universidad Politécnica de Madrid.
   
   
5. Partecipa al programma di ricerca cofinanziato dal MURST intitolato ``Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche'' (2001--2003, coordinatore nazionale: Prof. Domenico Cantone, Università di Catania).
   
   
6. Partecipa, come responsabile dell'unità di Parma al programma di ricerca cofinanziato dal MURST intitolato ``Verifica di sistemi reattivi basata su vincoli'' (2002--2004, coordinatore nazionale: Prof. Maurizio Gabbrielli, Università di Bologna).
   
   
7. Partecipa, come responsabile dell'unità di Parma al programma di ricerca cofinanziato dal MIUR intitolato ``AIDA --- Interpretazione Astratta: Progettazione e Applicazioni'' (2004--2006, coordinatore nazionale: Prof. Roberto Giacobazzi, Università di Verona).

4.11.2  Progetti Presentati

1. Ha partecipato, come rappresentante nazionale per l'Italia e come coordinatore (insieme a François Irigoin, École des Mines de Paris) del workpackage su Numerical Abstract Domains, alla proposta IST (VI programma quadro) intitolata ``AINoE: Network of Excellence on Abstract Interpretation'' (004456).

4.12  Partecipazione a scuole

1. ``Fifth International School for Computer Science Researchers'', Lipari, Italia, 21 giugno -- 3 luglio 1993.
   
   
2. NATO Advanced Study Institute ``CONSTRAINT PROGRAMMING'', Pärnu, Estonia, 13--24 agosto 1993.
   
   
3. ``2000 International Summer School in Computational Logic'', Acquafredda di Maratea, Basilicata, Italia, 3--8 settembre 2000.

4.13  Partecipazione a conferenze e workshop nazionali

• GULP'91, ``Sesto Congresso sulla Programmazione Logica'', Pisa, giugno 1991.
  
  
• Compulog 2 meeting, Roma, dicembre 1992. Presentazione del lavoro:

  Bagnara, R., Giacobazzi, R., and Levi, G. Applications of Constraint Propagation to Data-Flow Analysis.

  
  
  
• GULP'93, ``Ottavo Convegno sulla Programmazione Logica'', Gizzeria Lido (CZ), giugno 1993.
  
  
• Workshop progetto nazionale ``Modelli della Computazione e dei Linguaggi di Programmazione'', Volterra (PI), settembre 1993. Presentazione del lavoro:

  Bagnara, R. englishDetection of Future Redundant Constraints in CLP( R).

4.14  Partecipazione a conferenze e workshop internazionali

• ``Third International Workshop on Exstensions of Logic Programming'', Bologna, Italia, febbraio 1992.
  
  
• WSA'92, ``Second International Workshop on Static Analysis'', Bordeaux, Francia, settembre 1992.
  
  
• ALP'92, ``Third International Conference on Algebraic and Logic Programming'', Volterra, Italia, settembre 1992.
  
  
• CAIA'93, ``Ninth IEEE Conference on Artificial Intelligence for Applications'', Orlando (Florida), Stati Uniti, marzo 1993.
  
  
• WSA'93, ``Third International Workshop on Static Analysis'', Padova, Italia, settembre 1993.
  
  
• Workshop su ``Constraints for Program Analysis'', Århus, Danimarca, febbraio 1994. Presentazione del lavoro:

  Bagnara, R. Detection of Redundant Numeric Constraints in CLP Languages.

  
  
  
• ICLP'94, ``International Conference on Logic Programming'', S. Margherita Ligure, giugno 1994.
  
  
• GULP-PRODE'94, ``Joint Conference on Declarative Programming'', Peñíscola, Spagna, settembre 1994.
  
  
• CCP'95, ``First International Workshop on Concurrent Constraint Programming'', Cà Dolfin, Venezia, maggio 1995.
  
  
• GULP-PRODE'95, ``Joint Conference on Declarative Programming '', Marina di Vietri, settembre 1995.
  
  
• ``Special Workshop on Abstract Interpretation of Logic Languages'', Eilat, Israele, giugno 1995.
  
  
• APPIA-GULP-PRODE'96, ``1996 Joint Conference on Declarative Programming'', Donostia-San Sebastián, Spagna, luglio 1996.
  
  
• PLILP'96, ``Eighth International Symposium on Programming Languages, Implementations, Logics, and Programs'', Aachen, Germania, settembre 1996.
  
  
• SAS'96, ``Third International Static Analysis Symposium'', Aachen, Germania, settembre 1996.
  
  
• SAS'97, ``Third International Static Analysis Symposium'', Parigi, Francia, settembre 1997.
  
  
• APPIA-GULP-PRODE'98, ``1998 Joint Conference on Declarative Programming'', A Coruña, Spagna, luglio 1998.
  
  
• SAS'98, ``Fifth International Static Analysis Symposium'', Pisa, Italia, settembre 1998.
  
  
• PLILP/ALP'98, ``Tenth International Symposium on Programming Languages, Implementations, Logics and Programs'' and ``Seventh International Conference on Algebraic and Logic Programming'', Pisa, Italia, settembre 1998.
  
  
• AMAST'98, ``Seventh International Conference on Algebraic Methodology and Software Technology'' Amazzonia, Brasile, gennaio 1999.
  
  
• APPIA-GULP-PRODE'99, ``1999 Joint Conference on Declarative Programming'', L'Aquila, Italia, settembre 1999.
  
  
• SAS'99, ``International Static Analysis Symposium'', Venezia, Italia, settembre 1999.
  
  
• PPDP'99, ``International Conference on Principles and Practice of Declarative Programming'', Parigi, Francia, settembre/ottobre 1999.
  
  
• PPDP'00, ``Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming'', Montreal, Canada, settembre 2000.
  
  
• LPAR 2000, ``Seventh International Conference on Logic for Programming and Automated Reasoning'', Réunion, Oceano Indiano, novembre 2000.
  
  
• SAS 2001, ``Eighth International Symposium on Static Analysis'', Parigi, Francia, luglio 2001.
  
  
• APPIA-GULP-PRODE 2001, ``2001 Joint Conference on Declarative Programming'', Évora, Portogallo, settembre 2001.
  
  
• SAS'02, ``Ninth International Static Analysis Symposium'', Madrid, Spagna, settembre 2002.
  
  
• ITCLS'02, ``Implementation Technology for Computational Logic Systems'', Madrid, Spagna, settembre 2002.
  
  
• AVoCS 2003, ``Third Workshop on Automated Verification of Critical Systems'', Southampton, Regno Unito, aprile 2003.
  
  
• SAS'03, ``Tenth International Static Analysis Symposium'', San Diego, California, USA, giugno 2003.
  
  
• ITCLS'03, ``Implementation Technology for Computational Logic Systems'', Pisa, Italia, settembre, 2003.
  
  
• VMCAI'04, ``Fifth International Conference on Verification, Model Checking and Abstract Interpretation'', Venezia, Italia, gennaio 2004.
  
  
• ETAPS'04, ``European Joint Conferences on Theory and Practice of Software'', Barcellona, Spagna, marzo--aprile 2004.
  
  
• ICLP'04, ``Twentieth International Conference on Logic Programming'', Saint-Malo, Francia, settembre 2004.

5  Elenco delle pubblicazioni

[]

Le pubblicazioni elencate, tranne alcuni rapporti tecnici, sono disponibili all'URI http://www.cs.unipr.it/ bagnara. I rapporti tecnici sono disponibili all'URI http://www.cs.unipr.it.

5.1  Riviste internazionali

[1]

Bagnara, R. A unified proof for the convergence of Jacobi and Gauss-Seidel methods. SIAM Review 37, 1 (1995), 93--97.

[2]

Bagnara, R. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming 30, 1--2 (1998), 119--155.

[3]

Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. Theoretical Computer Science 277, 1-2 (2002), 3--46.

[4]

Hill, P. M., Bagnara, R., and Zaffanella, E. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming 2, 2 (2002), 155--201.

[5]

Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. Theory and Practice of Logic Programming 2, 2 (2002), 233--261.

[6]

Hill, P. M., Zaffanella, E., and Bagnara, R. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Theory and Practice of Logic Programming 4, 3 (2004), 289--323.

[7]

Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. Finite-tree analysis for constraint logic-based languages. Information and Computation 193, 2 (2004), 84--116.

[8]

Bagnara, R., Zaffanella, E., and Hill, P. M. Enhanced sharing analysis techniques: A comprehensive evaluation. Theory and Practice of Logic Programming 5, 1&2 (2005), 1--43.

[9]

Mesnard, F., and Bagnara, R. cTI: A constraint-based termination inference tool for ISO-Prolog. Theory and Practice of Logic Programming 5, 1&2 (2005), 243--257.

[10]

Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. Science of Computer Programming (2005). To appear.

[11]

Bagnara, R., Hill, P. M., and Zaffanella, E. Not necessarily closed convex polyhedra and the double description method. Formal Aspects of Computing (2005). To appear.

[12]

Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. Software Tools for Technology Transfer (2005). To appear.

5.2  Atti di conferenze internazionali

[13]

Perrin, Y., Bagnara, R., Berners-Lee, T. J., Carena, W., Divia, R., Parkman, C., Petersen, J., Tremblet, L., and Wessels, B. The valet-plus embedded into large physics experiments. In Proceedings of the ``VMEbus in Research International Conference'' (Zürich, Oct. 1988), C. Eck and C. Parkman, Eds., Elsevier Science Publishers B.V. (North-Holland), Amsterdam, pp. 59--68.

[14]

Heyes, G., Wessels, B., Perrin, Y., Bagnara, R., Berners-Lee, T. J., Carena, W., Divia, R., Parkman, C., Petersen, J., and Tremblet, L. The integration of vax and valet-plus data acquisition software. Contribution to the ``Sixth Conference on Real-Time Computer Applications in Nuclear, Particle, and Plasma Physics'' (Williamsburg, VA, May 1989). IEEE Transactions on Nuclear Science 36, 5 (1989), 1572--1576.

[15]

Bagnara, R., Giacobazzi, R., and Levi, G. An application of constraint propagation to data-flow analysis. In Proceedings of ``The Ninth Conference on Artificial Intelligence for Applications'' (Orlando, Florida, March 1993), IEEE Computer Society Press, Los Alamitos, CA, pp. 270--276.

[16]

Bagnara, R. A reactive implementation of Pos using ROBDDs. In Programming Languages: Implementations, Logics and Programs, Proceedings of the Eighth International Symposium (Aachen, Germany, 1996), H. Kuchen and S. D. Swierstra, Eds., vol. 1140 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 107--121.

[17]

Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. In Static Analysis: Proceedings of the 4th International Symposium (École Normale Supérieure, Paris, France, 1997), P. Van Hentenryck, Ed., vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 53--67.

[18]

Hill, P. M., Bagnara, R., and Zaffanella, E. The correctness of set-sharing. In Static Analysis: Proceedings of the 5th International Symposium (Pisa, Italy, 1998), G. Levi, Ed., vol. 1503 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 99--114.

[19]

Bagnara, R., and Schachte, P. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In Proceedings of the ``Seventh International Conference on Algebraic Methodology and Software Technology (AMAST'98)'' (Amazonia, Brazil, 1999), A. M. Haeberer, Ed., vol. 1548 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 471--485.

[20]

Zaffanella, E., Bagnara, R., and Hill, P. M. Widening Sharing. In Principles and Practice of Declarative Programming (Paris, France, 1999), G. Nadathur, Ed., vol. 1702 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 414--431.

[21]

Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. In Static Analysis: Proceedings of the 6th International Symposium (Venice, Italy, 1999), A. Cortesi and G. Filé, Eds., vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 69--84.

[22]

Bagnara, R., Zaffanella, E., and Hill, P. M. Enhanced sharing analysis techniques: A comprehensive evaluation. In Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (Montreal, Canada, 2000), M. Gabbrielli and F. Pfenning, Eds., Association for Computing Machinery, pp. 103--114.

[23]

Bagnara, R., Hill, P. M., and Zaffanella, E. Efficient structural information analysis for real CLP languages. In Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000) (Reunion Island, France, 2000), M. Parigot and A. Voronkov, Eds., vol. 1955 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 189--206.

[24]

Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E., Finite-tree analysis for constraint logic-based languages, In Static Analysis: Proceedings of the 8th International Symposium (SAS 2001), (Paris, France, 2001), P. Cousot, Ed., vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 165--184.

[25]

Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M. Boolean functions for finite-tree dependencies. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001) (Havana, Cuba, 2001), R. Nieuwenhuis and A. Voronkov, Eds., vol. 2250 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, pp. 575--589.

[26]

Bagnara, R., Ricci, E., Zaffanella, E., and Hill, P. M. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In Static Analysis: Proceedings of the 9th International Symposium (Madrid, Spain, 2002), M. V. Hermenegildo and G. Puebla, Eds., vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 213--229.

[27]

Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis: Proceedings of the 10th International Symposium (San Diego, California, USA, 2003), R. Cousot, Ed., vol. 2694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 337--354.

[28]

Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) (Venice, Italy, 2003), B. Steffen and G. Levi, Eds., vol. 2937 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 135--148.

[29]

Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Widening operators for weakly-relational numeric abstractions. In Static Analysis: Proceedings of the 12th International Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer Science, Springer-Verlag, Berlin.

[30]

Bagnara, R., Rodríguez-Carbonell, E., and Zaffanella, E. Generation of basic semi-algebraic invariants using convex polyhedra. In Static Analysis: Proceedings of the 12th International Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer Science, Springer-Verlag, Berlin.

5.3  Atti di workshop internazionali

[31]

Bagnara, R., Giacobazzi, R., and Levi, G. Static analysis of CLP programs over numeric domains. In Actes ``Workshop on Static Analysis '92'' (Bordeaux, September 1992), M. Billaud, P. Castéran, M. Corsini, K. Musumbu, and A. Rauzy, Eds., vol. 81--82 of Bigre, Atelier Irisa, IRISA Campus de Beaulieu, pp. 43--50.

[32]

Bagnara, R. On the detection of implicit and redundant numeric constraints in CLP programs. In Proceedings of the ``1994 Joint Conference on Declarative Programming (GULP-PRODE'94)'' (Peñíscola, Spain, September 1994), M. Alpuente, R. Barbuti, and I. Ramos, Eds., pp. 312--326.

[33]

Bagnara, R. Constraint systems for pattern analysis of constraint logic-based languages. In Proceedings of the ``1995 Joint Conference on Declarative Programming (GULP-PRODE'95)'' (Marina di Vietri, Italy, September 1995), M. Alpuente and M. I. Sessa, Eds., pp. 581--592.

[34]

Bagnara, R. Straight ROBDDs are not the best for Pos. In Proceedings of the ``1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'96)'' (Donostia-San Sebastián, Spain, 1996), Lucio, P., Martelli, M., and Navarro, M., Eds., pp. 493--496.

[35]

Bagnara, R., Comini, M., Scozzari, F., and Zaffanella, E. The AND-compositionality of CLP computed answer constraints. In Proceedings of the ``1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'96)'' (Donostia-San Sebastián, Spain, 1996), Lucio, P., Martelli, M., and Navarro, M., Eds., pp. 355--366.

[36]

Bagnara, R. Structural information analysis for CLP languages. In Proceedings of the ``1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'97)'' (Grado, Italy, 1997), Falaschi, M., Navarro, M., and Policriti, A., Eds., pp. 81--92.

[37]

Bagnara, R., Hill, P. M., and Zaffanella, E. Sharing revisited. In Proceedings of the ``1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'97)'' (Grado, Italy, 1997), Falaschi, M., Navarro, M., and Policriti, A., Eds., pp. 69--80.

[38]

Bagnara, R., and Schachte, P. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In Proceedings of the ``1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'98)'' (A Coruña, Spain, 1998), Freire-Nistal, J. L., Falaschi, M., and Vilares-Ferro, M., Eds., pp. 227--239.

[39]

Hill, P. M., Bagnara, R., and Zaffanella, E. The correctness of set-sharing. In Proceedings of the ``1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'98)'' (A Coruña, Spain, 1998), Freire-Nistal, J. L., Falaschi, M., and Vilares-Ferro, M., Eds., pp. 255--267.

[40]

Bagnara, R., Zaffanella, E., and Hill, P. M. Enhancing Sharing for precision. In Proceedings of the ``APPIA-GULP-PRODE'99 Joint Conference on Declarative Programming'' (L'Aquila, Italy, 1999), Meo, M. C., and Ferro, M. V., Eds., pp. 213--227.

[41]

Zaffanella, E., Bagnara, R., and Hill, P. M. Widening Sharing. In Proceedings of the ``APPIA-GULP-PRODE'99 Joint Conference on Declarative Programming'' (L'Aquila, Italy, 1999), Meo, M. C., and Ferro, M. V., Eds., pp. 559--573.

[42]

Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding of not necessarily closed convex polyhedra. In Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems (Madrid, Spain, 2002), M. Carro, C. Vacheret, and K.-K. Lau, Eds., pp. 147--153. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática.

[43]

Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding and implementation of not necessarily closed convex polyhedra. In Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (Southampton, UK, 2003), M. Leuschel, S. Gruner, and S. Lo Presti, Eds., pp. 161--176. Published as TR Number DSSE-TR-2003-2, University of Southampton.

5.4  Tesi di dottorato

[44]

Bagnara, R. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy, Mar. 1997. Printed as Report TD-1/97.

5.5  Rapporti tecnici

[45]

Bagnara, R., Hill, P. M., and Zaffanella, E. Sharing revisited. Tech. Rep. 97.19, School of Computer Studies, University of Leeds, U.K., 1997.

[46]

Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. Quaderno 172, Dipartimento di Matematica, Università di Parma, Italy, 1998. Available at http://www.cs.unipr.it/Publications/.

[47]

Zaffanella, E., Bagnara, R., and Hill, P. M. Widening set-sharing. Quaderno 188, Dipartimento di Matematica, Università di Parma, 1999.

[48]

Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. Tech. Rep. 99.07, School of Computer Studies, University of Leeds, U.K., 1999.

[49]

Bagnara, R., Hill, P. M., and Zaffanella, E. Efficient structural information analysis for real CLP languages. Quaderno 229, Dipartimento di Matematica, Università di Parma, 2000. Available at http://www.cs.unipr.it/ bagnara/.

[50]

Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E., Finite-tree analysis for constraint logic-based languages, Quaderno 251, Dipartimento di Matematica, Università di Parma, 2001. Available at http://www.cs.unipr.it/ bagnara/.

[51]

Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M., Boolean functions for finite-tree dependencies, Quaderno 252, Dipartimento di Matematica, Università di Parma, 2001. Available at http://www.cs.unipr.it/ bagnara/.

[52]

Hill, P. M., Zaffanella, E., and Bagnara, R. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Quaderno 273, Dipartimento di Matematica, Università di Parma, Italy, 2001. Available at http://www.cs.unipr.it/Publications/. Also published as technical report No. 2001.22, School of Computing, University of Leeds, U.K.

[53]

Bagnara, R., and Carro, M. Foreign language interfaces for Prolog: A terse survey. Quaderno 283, Dipartimento di Matematica, Università di Parma, Italy, 2002. Version 1. Available at http://www.cs.unipr.it/Publications/.

[54]

Bagnara, R., Ricci, E., Zaffanella, E., and Hill, P. M. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. Available at http://www.cs.unipr.it/Publications/.

[55]

Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding and implementation of not necessarily closed convex polyhedra. Quaderno 305, Dipartimento di Matematica, Università di Parma, Italy, 2002. Available at http://www.cs.unipr.it/Publications/.

[56]

Hill, P. M., Zaffanella, E., and Bagnara, R. On the analysis of set-sharing, freeness and linearity for finite and rational tree languages. Tech. Rep. 2003.08, School of Computing, University of Leeds, U.K., 2003. Available at http://www.comp.leeds.ac.uk/research/pubs/reports.shtml.

[57]

Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. Quaderno 312, Dipartimento di Matematica, Università di Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.

[58]

Bagnara, R., Zaccagnini, A., and Zolo, T. The automatic solution of recurrence relations. I. Linear recurrences of finite order with constant coefficients. Quaderno 334, Dipartimento di Matematica, Università di Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.

[59]

Bagnara, R., and Zaccagnini, A. Checking and bounding the solutions of some recurrence relations. Quaderno 344, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.

[60]

Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. Quaderno 349, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.

[61]

Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. Finite-tree analysis for constraint logic-based languages: the complete unabridged version. Quaderno 363, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.

[62]

Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Università di Parma, Italy, 2005. Available at http://www.cs.unipr.it/Publications/.

[63]

Bagnara, R., Rodríguez-Carbonell, E., and Zaffanella, E. Generation of basic semi-algebraic invariants using convex polyhedra. Report de recerca LSI-05-14-R, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, Barcelona, Spain, 2005. Available at http://www.lsi.upc.es/dept/techreps/techreps.html.

5.6  Altri scritti

[64]

Bagnara, R. Announcing Kermit68K, a Portable 68000 Kermit Program. Info-Kermit Digest 6, 15 (July 1987).

[65]

Bagnara, R. A General Event Handling System for the Valet-Plus. CERN Data Handling Division, Online Computing Group, September 1988.

[66]

Bagnara, R. Remote Procedure Call. CERN Mini & Micro Computer Newsletter 20 (October 1988).

[67]

Bagnara, R. Interpretazione astratta di linguaggi logici con vincoli su domini finiti. M.Sc. dissertation, University of Pisa, July 1992. In Italian.

[68]

Bagnara, R. Analysing with China. The Association for Logic Programming Newsletter 12, 1 (1999), 9.

[69]

Bagnara, R. Is the ISO Prolog standard taken seriously? The Association for Logic Programming Newsletter 12, 1 (1999), 10--12.

[70]

Bagnara, R. On the quality of available Prolog implementations. The Association for Logic Programming Newsletter 12, 2 (1999), 12--14.

[71]

Bagnara, R. Precise and Practical Mode Analysis with the China Analyzer. Computational Logic 7, November 1999.

[72]

Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. The Parma Polyhedra Library User's Manual, release 0.5 ed. Department of Mathematics, University of Parma, Parma, Italy, Dec. 2004. Available at http://www.cs.unipr.it/ppl/.

[73]

Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Widening operators for weakly-relational numeric abstractions. Report arXiv:cs.PL/0412043, 2004. Extended abstract. Contribution to the International workshop on ``Numerical & Symbolic Abstract Domains'' (NSAD'05, Paris, January 21, 2005). Available at http://arxiv.org/ and http://www.cs.unipr.it/ppl/.

[Page last updated on August 17, 2005, 15:38:46.]