La logica nei sui vari aspetti e' uno strumento efficace nella specifica formale e verifica di programmi, come testimoniato dalla vasta letteratura. I proponenti hanno gia' ottenuto risultati nelle seguenti aree:
- logica intermedie costruttive nella specificazione e validazione di sistemi modulari
e OO [Ornaghi&al06,Lau&al06,Ferrari&al08];
- trattamento dell'informazione incerta mediante logiche polivalenti tramite rappresentazioni combinatorie delle strutture duali delle loro semantiche algebriche e algoritmi per la produzione e la manipolazione di queste rappresentazioni [Aguzzoli&al07].
- metodi categoriali in semantica: completamenti di categorie in connessione con topologia formale e teoria dei domini [Bucalo&al06a,Bucalo&al06b];
- dimostrazione automatica e sue applicazioni (combinazione di procedure di decisione) [Ghilardi&al05,Ghilardi&al07].
La ricerca si propone di proseguire lo studio in tali ambiti, estendendo, ampliando ed applicando i risultati ottenuti nello scorso anno. In particolare si intendono conseguire i seguenti obiettivi:
(a) Logica costruttiva come base semantica nella specifica di un linguaggio di modellizzazione orientato agli oggetti. Si intendono rafforzare i risultati ottenuti nella validazione delle specifiche mediante "snapshot generation" [Ferrari&al08] e applicare tali risultati in ambiti specifici, in particolare nella generazione di casi di test nell'ambito della MDA (Model Driven Architecture). Si intende proseguire nello studio dell'applicazione di tali tecniche nell'ambito dei linguaggi di azioni.
(b) Studio di semantiche algebriche per logiche polivalenti. In particolar modo si intende proseguire lo studio delle rappresentazioni spettrali duali, sviluppando applicazioni delle stesse nella teoria della misura e della probabilita'.
(c) Presentazione di strutture semantiche. Si intende proseguire lo studio di possibili applicazioni del recente approccio alla topologia formale in termini di strutture in categorie ottenute tramite costruzioni libere. In particolare si investigheranno possibili estensioni alla teoria dei domini con lo scopo di ottenere una descrizione unitaria per semantiche distinte.
(d) Studio e sviluppo di strumenti di dimostrazione automatica in vari aspetti. Lo studio dei sistemi che consentano di combinare modularmente ed integrare procedure di decisione rende possibile lo sviluppo di nuovi strumenti nell'ambito del model-checking di sistemi a stati infiniti. Partendo dai risultati ottenuti in [Ghilardi&al07], si intende concentrare la ricerca su particolari sistemi a stati infiniti (fra cui una larga classe di sistemi parametrici) e sviluppare per questi procedure per il problema di model-checking.