Conoscenze fondamentali della logica classica e di alcune logiche non
classiche e alcune loro applicazioni rilevanti per l'informatica.
classiche e alcune loro applicazioni rilevanti per l'informatica.
scheda docente
materiale didattico
M. Cialdea Mayer. Logica (dispense)
Un qualunque testo di introduzione al Prolog
D. A. Peled. Software Reliability Methods, capitoli 1 e 4
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (dispense).
J.-P. Katoen. Concepts, Algorithms and Tools for Model Checking
Gerd Behrmann, Alexandre David, and Kim G. Larsen A Tutorial on Uppaal 4.0.
G. Behrmann et al. UPPAAL Tiga User-manual.
Programma
Logica del primo ordine e deduzione automatica. Cenni sul linguaggio Prolog. Metodi formali per la verifica di sistemi. Automi temporizzatiTesti Adottati
vedi il sito del corso: http://cialdea.dia.uniroma3.it/teaching/logica/M. Cialdea Mayer. Logica (dispense)
Un qualunque testo di introduzione al Prolog
D. A. Peled. Software Reliability Methods, capitoli 1 e 4
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (dispense).
J.-P. Katoen. Concepts, Algorithms and Tools for Model Checking
Gerd Behrmann, Alexandre David, and Kim G. Larsen A Tutorial on Uppaal 4.0.
G. Behrmann et al. UPPAAL Tiga User-manual.
Modalità Erogazione
Lezioni frontali ed esercitazioni in aula.Modalità Valutazione
Il corso prevede un esame scritto, con la possibilita' di sostituirlo con prove in itinere riservate agli studenti frequentanti.