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.
Programma
Logica del primo ordine, deduzione automatica, il linguaggio Prolog, Metodi formali per la verifica di sistemiTesti 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.
Modalità Erogazione
Lezioni in aulaModalità Valutazione
Esame scritto, normalmente. Nel periodo di emergenza COVID-19 l’esame di profitto sarà una prova orale, svolta secondo quanto previsto all’art.1 del Decreto Rettorale n°. 703 del 5 maggio 2020