Sistemi Formali per la Specifica, l'Analisi, la Verifica, la Sintesi e la Trasformazione di Sistemi Software - Unita' di Genova

• PAGINA PRINCIPALE: Notizie, Tematiche, Unita', Finanziamenti.
• Giorgio Levi (Coordinatore Nazionale). modello A (copia locale);
• Eugenio Moggi (Coordinatore Unita' di Genova), modello B Unita' di Genova; modello C CHIUSO;
• mailing-list locale: p40@disi.unige.it; mailing-list nazionale: semantica@di.unipi.it.

Composizione (qualifica e mesi uomo)

• Staff permanente:
  1. Ancona Massimo (PA) 10
  2. Astesiano Egidio (PO) 8
  3. Cerioli Maura (RC) 10
  4. Costa Gerardo (PO) 8
  5. Martelli Maurizio (PO) 8
  6. Moggi Eugenio (PO) 8
  7. Zucca Elena (RC) 10
• Dottorandi e borsisti:
  1. Ancona Davide (PostDoc) 10
  2. Belle' Gianna (Dott) 10
  3. Calcagno Cristiano (Dott) 10
  4. Coscia Eva (Dott) 10
  5. Zini Floriano (Dott) 10
  6. Cazzola Walter (Dott. Milano) 5
• Personale aggiunto in seguito:
  1. Bozzano Marco (Dott)
  2. Cuppari Alessio (Coll. esterno)
  3. Mascardi Viviana (Dott)
  4. Reggio Gianna (PA)

Tematiche, Compiti ed Obbiettivi

• Linguaggi funzionali: 1.1
• Linguaggi logici: 2.1
• Linguaggi modulari e ad oggetti: 4.2, 4.3
• Modelli, linguaggi e tecniche di specifica algebrica: 5.1
• Relazione sulla attivita' del primo anno

Linguaggi funzionali

• (1.1 persone): Moggi, Belle', Calcagno
• (1.1 compito) Si studieranno semantiche intensionali per modellare una varieta' di aspetti (p.e. distinzione di fase, struttura dei tipi di dato), che saranno poi utilizzate per lo sviluppo di linguaggi intermedi a due livelli (adottati nell'ambito della ottimizzazione basata sulla tecnica della "partial evaluation") e come fondamento per tecniche di analisi statica di programmi ad alto livello per architetture paralleli.
• (1.1 obbiettivi primo anno) Semantica dei linguaggi a due livelli per "partial evalutation", ed applicazioni alla verifica di correttezza della fase di specializzazione.
• (1.1 obbiettivi secondo anno) Tecniche di analisi statica degli errori di shape e tecniche di ottimizzazione di programmi che sfruttano l'informazione statica sulle shape.

Linguaggi logici

• (2.1 persone): Martelli, Bozzano, Mascardi, Zini
• (2.1 compito) La logica lineare offre una maggior espressivita' per la modellazione di aspetti operazionali rispetto alle logiche standard. Si studiera' l'applicazione dei linguaggi di programmazione logica lineare di ordine superiore per la prototipazione rapida (programmi come specifiche eseguibili) di sistemi concorrenti ad oggetti e di sistemi multi-agente.
• (2.1 obbiettivi primo anno) Sviluppo di un ambiente di programmazione logico e object-oriented, e sua applicazione ai database attivi object-oriented e deduttivi.
• (2.1 obbiettivi secondo anno) Ambienti di sviluppo per applicazioni orientate agli agenti.

Linguaggi modulari e ad oggetti

• (4.2 persone): Zucca, AnconaD;
• (4.3 persone): AnconaM, Cazzola
• (4.2 compito) Si proporra' un nucleo linguistico di moduli "mixin" (moduli con componenti deferred) ed un modello per tali moduli, entrambi il piu' possibile indipendenti dal linguaggio base sottostante. Si studieranno poi traduzioni di costrutti linguistici esistenti in tale nucleo e regole di riduzione che permettano di ridurre espressioni di modulo complesse in forma normale.
• (4.2 obbiettivi primo anno) Definizione di un linguaggio kernel per moduli mixin.
• (4.2 obbiettivi secondo anno) Definizione di leggi algebriche per il linguaggio dei moduli mixin e di un relativo calcolo.
• (4.3 compito) Si considereranno problemi di implementazione di linguaggi modulari ed object-oriented, con particolare riferimento ad aspetti riflessivi, alla gestione dinamica del comportamento degli oggetti e allo sviluppo di algoritmi di generazione di codice che incrementino il parallelismo a livello di codice macchina. Si studieranno anche le relazione tra modularita` e ottimizzazione di codice; tra modularita`, compilazioni separate ed ereditarieta`.
• (4.3 obbiettivi primo anno) Studio di meccanismi riflessivi in ambiente distribuito, realizzazione di un'estensione di Oberon che supporti il cambiamento dinamico del comportamento degli oggetti.
• (4.3 obbiettivi secondo anno) Sviluppo di algoritmi per la schedulazione delle istruzioni e l'allocazione dei registri su architetture RISC. Relazione tra compilazioni separate, ottimizzazione del codice, ereditarieta` di implementazione e caricamento dinamico dei moduli.

Modelli, linguaggi e tecniche di specifica algebrica

• (5.1 persone): Astesiano, Cerioli, Costa, Coscia, Reggio
• (5.1 compito) Si sviluppera' un linguaggio di specifica algebrico comune (tale ricerca e' effettuata nel contesto della Common Algebraic Framework Initiative, che si articola a livello europeo), che permetta di trattare in modo integrato sia aspetti formali, quali la definizione rigorosa della semantica del linguaggio, che aspetti metodologici e applicazioni a realta' piu' complesse (in particolare saranno prese in considerazione la specifica di sistemi reattivi, concorrenti e distribuiti).
• (5.1 obbiettivi primo anno) Definizione del linguaggio di base COFI, analisi delle sue applicazioni a problemi reali dal punto di vista metodologico e studio degli attuali linguaggi di specifica per sistemi dinamici.
• (5.1 obbiettivi secondo anno) Sviluppo di un metodo di specifica formale logico-algebrico per sistemi dinamici, concorrenti e reattivi.

Corrispondenza tematiche - unita'