Bibliografia
[AC96] M. Abadi, L. Cardelli. A Theory of Objects. Springer, 1996.
[AH96] Alur, Henzinger. Reactive Modules, Proc. LICS 96.
[An95] Andersen. Partial Model Checking. LICS, 1995.
[AHM+98] Alur, Henzinger, Mang, Qadeer, Rajamani,Taisiran. MOCHA. In Proc CAV 98.
[AS03] G. Amato and F. Scozzari. A General Framework for Variable Aliasing: Towards Optimal Operators for Sharing Properties. In Proceedings of International Workshop on Logic Based Program Synthesis and Tranformation, volume 2664 of LNCS, pages 52--60. Springer-Verlag, 2003.
[ASW94] Andersen, Stirling, Winskel. A compositional proof system for the modal mu-calculus. LICS, 1994.
[BMS+98] Maria Garcia de La Banda, Kim Marriott, Peter Stuckey, Harald Sondergaard, Differential Methods in Logic Program Analysis Journal of Logic Programming, 37(1) pages. 1--37, 1998
[BBDT02] R. Barbuti, C. Bernardeschi, N. De Francesco, L. Tesei. Fixing the Java bytecode verifier by a suitable type domain. In Proceedings of the 14th International Conference on Software Engineering and Knowledge Engineering (SEKE'02), ACM Press, 377--382, 2002.
[BCT04] R. Barbuti, S. Cataudella, L. Tesei. Abstract interpretation against races. To appear on Fundamenta Informaticae, 2004.
[BGMP97] F.S. de Boer, M. Gabbrielli, E. Marchiori and C. Palamidessi. Proving Concurrent Constraint Programs Correct. Transactions on Programming Languages and Systems (TOPLAS), 19(5): 685-725. ACM Press, 1997.
[BGM01] F.S. de Boer, M. Gabbrielli and M.C. Meo. A Denotational Semantics for a Timed Linda Language. Proc. 3th Symposium PPDP . ACM Press, 2001.
[BGM01a] F.S. de Boer, M. Gabbrielli and M.C. Meo. A Temporal Logic for reasoning about Timed Concurrent Constraint Programs. In Proc. TIME 01. IEEE Press, 2001.
[Car97] LucaCardelli. Type systems. The Handbook of Computer Science and Engineering, Chapter 103, 2208-2236, CRC Press, 1997.
[Cou97] Patrick Cousot. Types as Abstract Interpretations. In Proceedings of the 24th Symposium on Principles of Programming Languages. Paris, France, 316-331, January 1997.
[CC77] P. Cousot, R. Cousot. Abstract Interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages (POPL'77). ACM Press, 238-258, 1977.
[CC92] P. Cousot, R. Cousot Abstract Interpreation Frameworks Journal of Logic and Computations, 2(4), pages 511-549, 1992
[CDH+00] James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng. Bandera: extracting finite-state models from Java source code. ICSE 2000: 439-448
[Del03] Giorgio Delzanno Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design 23(3): 257-301 (2003)
[DRV02] Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin Towards the Automated Verification of Multithreaded Java Programs. TACAS 2002: 173-187
[FA99] C. Flanagan, M. Abadi. Object Types against Races. In Proceedings of the10th International Conference on Concurrency Theory (CONCUR '99). Lecture Notes in Computer Science 1664. Springer, 288-303, 1999.
[FM99] S. N. Freund, J. C. Mitchell. A Formal Framework for the Java Bytecode Language and Verifier. In Proceedings of 15th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'99). ACM Press, 147-166, 1999.
[GH98] Andrew D. Gordon, Paul D. Hankin. A Concurrent Object Calculus: Reduction and Typing. Electronic Notes in Theoretical Computer Science (ENTCS), 16, 1998.
[HT98] M. Hagiya, A. Tozawa. On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines. In Proceedings of the 5th International Symposium on Static (SAS'98). Lecture Notes on Computer Science 1503. Springer, 17-32, 1998.
[HQR+98] Henzinger, Qadeer, Rajamani, You assme we gurantee: Mthodology and case studies, Proc CAV 98.
[MH92] K. Muthukumar, M. V. Hermenegildo Compile-Time Derivation of Variable Dependency Using Abstract Interpretation Journal of Logic Programming 13(2&3), pages. 315--347, 1992
[Nie88] Strictness analysis and denotational abstract interpretation, Information and Computation 76(1), pages 29--92, 1988.
[JTM98] Compositional verification of concurrent systems using Petri net based condensation rules. Juan, E.Y.T.; Tsai, J.J.P.; Murata, Tadao In: ACM Trans. on Programming Languages and Systems, Vol. 20, No. 5, pages 917-979. 1998.
[Lan03] Cosimo Laneve. A type system for JVM threads. Theoretical Computer Science, 290(1), 741-778, 2003. [LY99] T. Lindholm, F. Yellin. The Java Virtual Machine Specification. Second Edition. The Java Series. Addison-Wesley, 1999.
[OCa99] Robert O'Callahan. A Simple, Comprehensive Type System for Java Bytecode Subroutines. In Proceedings of the 26th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages (POPL'99). ACM Press, 70-78, 1999. [SA99] R. Stata, M. Abadi. A type system for Java bytecode subroutines. ACM Transactions on Programming Languages and Systems, 21(1), 90-137, 1999.
[RRS+00]. C.R. Ramakrishnan, I.V. Ramakrishnan, Scott A. Smolka et al. XMC: A logic programming-based verification toolkit. CAV 2000.
[Win83] Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983
Il focus principale dell'attivita' della nostra unita' e' sullo studio di tecniche di analisi e verifica per programmi orientati agli oggetti e multithreaded (ad esempio, programmi Java). Considereremo questo problema da vari punti di vista, principalmente usando tecniche basate su interpretazione astratta, vincoli e metodi composizionali. Intendiamo inoltre studiare l'analisi di linguaggi logici (anche con vincoli) e linguaggi dichiarativi in genere usando opportune semantiche ``collecting''. L'attivita' dell'unita' di Bologna quindi e' rilevante per i workpackages 1, 5 e 6 del progetto. Specificatamente, facendo riferimento alla struttura generale del progetto, si identificano le seguenti direzioni di ricerca per il lavoro dell'unita' di Bologna. Workpackage 1 "Analisi statica" Task Bo.1.1: "Interpretazione astratta per programmi orientati agli oggetti". I sistemi di tipi e gli algoritmi di inferenza di tipo sono i metodi classici che vengono usati per l' analisi statica di proprieta' dinamiche di programmi [Car97]. Comunque, in molti articoli che propongono l'uso di tecniche di interpretazione astratta per eseguire analisi statiche su linguaggi di programmazione, viene sottolineato il fatto che spesso le analisi basate su regole di tipaggio dei costrutti del linguaggio sono troppo rigide e impongono condizioni di correttezza che potrebbero essere meno restrittive. Questa affermazione e' confermata anche dal fatto che spesso e' possibile ridefinire i sistemi di tipi e/o gli algoritmi di inferenza di tipo come semantiche o interpreti astratti [Cou97]. Per implementare l'analisi statica di proprieta' dinamiche, un interprete astratto esegue un programma astraendo i valori reali delle variabili in certi elementi di un dominio astratto. La computazione astratta e terminante puo' essere allora vista come un'approssimazione dell'insieme di tutte le computazioni reali del programma. Per queste caratteristiche, in molti casi, l'interpretazione astratta riesce ad essere piu' precisa dell'analisi basata sui tipi certificando correttamente un piu' alto numero di programmi. Seguendo questa idea, il nostro obiettivo e' quello di definire dei framework di interpretazione astratta che migliorino le analisi statiche esistenti basate sui tipi oppure che ne introducano di nuove. Piu' precisamente consideriamo gli obiettivi specifici che seguono. Obiettivo 1.1.1 Vogliamo definire framework di interpretazione astratta che migliorino analisi statiche esistenti basate sui tipi o ne introducano di nuove. In particolare, vorremmo definire un framework per l'analisi statica di programmi in Java bytecode. Questo framework dovrebbe essere basato su una formalizzazione della semantica dei programmi bytecode e su una conseguente interpretazione astratta che usa i domini astratti appropriati. Un'applicazione interessante, per i suoi aspetti di sicurezza e mobilita', potrebbe essere la verifica di proprieta' di sicurezza di programmi bytecode provenienti da una fonte non affidabile. Questo in aggiunta all'analisi gia' svolta dal verificatore del bytecode. Obiettivo 1.1.2 Usando l'interpretazione astratta, abbiamo intenzione di introdurre nuove analisi statiche, o potenziarne di esistenti, che riguardano in maniera piu' focalizzata gli aspetti di concorrenza dei formalismi orientati agli oggetti. Useremo, come linguaggi di base, calcoli ad oggetti concorrenti. Un esempio di questo tipo di lavoro e' il miglioramento dell'analisi che controlla l'assenza di accessi concorrenti errati ad oggetti condivisi (race conditions). Obiettivo 1.1.3 Abbiamo introdotto una nozione di non interferenza temporizzata per sistemi a tempo reale modellati con automi temporizzati. Tale nozione e' utile per rilevare interferenza dovuta alla frequenza di certe azioni e puo' essere usata, ad esempio, per analizzare la resistenza di componenti di rete ad attacchi che sfruttano l'informazione sul tempo. Sfortunatamente, la nozione piu' naturale di non interferenza temporizzata e' indecidibile. Vogliamo usare l'interpretazione astratta per definire nozioni implementabili approssimate che permettano poi la realizzazione di strumenti di analisi. Task Bo.1.2: "Analisi di linguaggi dichiarativi sulla base della semantica collecting" Obiettivo 1.2.1. Vogliamo fornire una caratterizzazione algebrica del significato di semantica collecting. L'unico lavoro che conosciamo che affronta questo problema e' [Nie88]. Come esempio del tipo di risultati che vogliamo ottenere, supponiamo di fissare una semantica standard e alcune proprieta' degli osservabili a cui siamo interessati (ad esempio, la monotonia della funzione di astrazione rispetto all'ordinamento computazionale). Possiamo derivare la semantica collecting come la sematica iniziale tra tutte quelle in cui l'analisi puo' essere svolta all'interno del framework basato su connessioni di Galois. Obiettivo 1.2.2 Vogliamo sviluppare una nuova semantica che sia costruita dall'inizio per essere piu' precisa sia di quella goal-dependent che di quella goal-independent, per tutti i domini astratti. Il vantaggio di questo risultato sarebbe la disponibilita' di una semantica unica adatta a tutti i tipi di analisi di linguaggi lgici. Pensiamo inoltre che cio' porterebbe a una comprensione piu' profonda della maniera in cui i domini astratti sono costruiti, specialmente del modo in cui posso essere decomposti in due componenti, una chiusa per istanze e l'altra chiusa per anti-istanze. Obiettivo 1.2.3 Vogliamo studiare algoritmi ottimali per l'unificazione astratta e il matching astratto di sostituzioni e vincoli. Siamo particolarmente interessati ai domini astratti per proprieta' di aliasing e sharing, utili per la parallelizzazione automatica di programmi logici (con vincoli) [MH92]. Implementeremo inoltre alcuni nuovi domini introdotti in [AS03] e studieremo la maniera di applicare il matching astratto in altri campi, come nei sistemi di riscrittura di termini o nei linguaggi funzionali. Workpackage 5: "Vincoli" Task Bo.5.1: "Analisi composizionale basata su vincoli di programmi multithreaded" In questo sottotask ci proponiamo di studiare l'applicazione della combinazione di interpretazione astratta e programmazione con vincoli all'analisi e verifica di programmi multithreaded. Per poter gestire esempi reali, sara' indispensabile studiare le tecniche di estrazione di modelli astratti a partire da programmi concreti e le tecniche di analisi composizionali. I nostri obbiettivi sono quindi i seguenti: Obiettivo 5.1.1 A partire da modelli astratti di programmi multithreaded (specificati in formalismi stile algebra dei processi), studieremo i fondamenti teorici della verifica composizionale basata su vincoli. Il punto chiave e' sfruttare la composizionalita' delle operazioni su vincoli in modo da specificare modularmente diverse analisi di un sistema concorrente. Piu' in dettaglio, studieremo una semantica denotazione basata su vincoli per processi definiti in un'algebra adeguata; gli operatori sintattici del linguaggio (composizione parallela, restrizione ecc.) dovranno essere modellato attraverso operatori semantici definiti su vincoli (congiunzione, quantificazione esistenziale, ecc). Utilizzando tale semantica, definiremo un sistema di prova composizionale nel quale la fase di verifica potra' essere ridotta ad un problema di soddisfacibilita' di vincoli. Come detto in precedenza, oltre all'interesse teorico, un approccio di questo tipo sembra essere promettente anche da un punto di vista pratico, in quanto sono stati sviluppati risolutori di vincoli molto efficienti e provvisti di euristiche che permettono di risolvere anche problemi di grandi dimensioni. Obiettivo 5.1.2 Studieremo la possibile combinazione di interpretazione astratta e vincoli per l'estrazione di modelli astratti a partire da programmi concreti (ad es. in Java). In questo contesto i vincoli possono essere utilizzati per specificare condizioni sull'ambiente in programmi aperti (una caratteristica tipica dei programmi multithreaded). Obiettivo 5.1.3 Studieremo anche l'uso diretto di linguaggi basati su vincoli come CCP (Concurrent Constraint Programming) e CHR (Constraint Handling Rules) per la specifica e verifica di sistemi multithreaded. Siamo quindi interessanti a semantiche e metodologie di verifica composizionali per tali formalismi. Se alcuni risultati esistono per CCP, non siamo a conoscenza di risultati ottenuti nel caso di CHR dove la presenza di clausole con teste multiple genera complicazioni a livello semantico. Workpackage 6: "Tecniche di verifica" Task Bo.6.1: "Verifica simbolica di programmi multithreaded" Sulla base dei risultati del sottotask STBo2 ci proponiamo i seguenti obbiettivi Obiettivo 6.1.1 Studieremo metodi simbolici per la verifica dei modelli astratti di programmi multithreaded (ad es. utilizzando constraint-based model checkers) e astrazioni dinamiche (e.g. operatori di widening e accelerazione) da applicare durante la fase di analisi. Obiettivo 6.1.2 Studieremo quali tool esistenti di verifica ed analisi basati su risoluzione di vincoli (e.g. per vincoli lineari e formule proposizionali) possono essere utilizzati come supporto per la metodologia proposta nel progetto. Piu' in dettaglio ci proponiamo di identificare risolutori efficienti per la classe di vincoli utilizzata nelle nostra metodologia. Ad esempio, un punto chiave della nostra metodologia sembra essere la possibilita' di poter risolvere vincoli su domini finiti assegnando valori tutti distinti tra loro alle variabili. sarebbe quindi necessario utilizzare risolutori che gestiscono in maniera efficiente vincoli del tipo ``alldifferent''. Intendiamo infine dividere la nostra attivita' nelle seguenti fasi: Primo anno: Obiettivi 1.1.1, 1.1.2, 1.2.1, 5.1.1 e 5.1.3 Secondo anno: Obiettivi 1.1.3, 1.2.2, 1.2.3, 5.1.2, 6.1.1 e 6.1.2.
