Libri di Testo:

• Fordamenti di  logica
  
• Marta Cialdea Mayer. Logica - Linguaggio, Ragionamento, Calcolo. Progetto Leonardo. Società Editrice Esculapio, 2002.
  www.inf.uniroma3.it/cialdea/teaching/ai/ai.html

• Metodi Formali

•  Doron A. Peled. Software Reliability Methods. Springer Verlag, 2001

• Abstract State Machines

•  Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003
  

Materiale Didattico:

• introduzione al corso
  
• richiami sulla Logica Proposizionale (gentile concessione della Prof. Marta Cialdea)
• richiami sulla Logica dei Predicati        "
• modellazione di sistemi software (Cap. 4 del Peled)
• PVS :  introduzione ed esempi di teorie
• logica CTL
• model checking in CTL
• SMV ed esempi di specifica e verifica
• Proprietà temporali
• Astrazione e model checking
  

Prove di verifica: