La logica nei sui vari aspetti è 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 [Lau&al04,Ornaghi&al06,Lau&al06];
- trattamento dell'informazione incerta mediante logiche polivalenti tramite analisi computazionali delle loro semantiche algebriche [Aguzzoli&al05,Aguzzoli06];
- 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 (proof carrying code, combinazione di procedure di decisione) [Beringer&al04,Ghilardi&al06,Ghilardi&al05].
La ricerca si propone di approfondire e sviluppare le linee di ricerca sopra esposte. 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 studiare gli strumenti di validazione delle specifiche (in particolare, mediante "snapshot generation") e di verifica dei programmi implicite nella semantica costruttiva adottata.
(b) Studio di semantiche algebriche per una gerarchia di logiche polivalenti basate su T-norme. In particolare si studieranno dualita' spettrali che possono trovare applicazione nello studio delle forme normali e nello studio della complessita' computazionale di queste logiche.
(c) Presentazione di strutture semantiche in termini algebrici. Nell'ottica generale di ottenere descrizioni basate su categorie di comonoidi si intende studiare alcune caratterizzazioni recenti degli L-domini algebrici.
(d) Studio e sviluppo di strumenti di dimostrazione automatica, in vari aspetti. Da un lato si realizzeranno sistemi di verifica specifici (ricerca di controesempi nella meta-teoria di sistemi formali), dall'altro si studieranno sistemi che consentano di combinare modularmente ed integrare procedure di decisione.