Ricerca di contatti, progetti,
corsi e pubblicazioni

Computer Aided Verification

Descrizione

This course introduces an approach to validation of hardware and software based on formal analysis of system behaviors. Among the formal methods, model checking enjoys considerable popularity because of its high degree of automation and exhaustiveness of its analysis. This approach has been highly effective in the analysis of hardware designs and is becoming a mainstream technology in verifying correctness of software systems. The course presents the foundations of model checking starting from the modelling of systems and properties, and then proceeding with the basic verification algorithms. Among other things, the distinction between branching time and linear time is discussed, safety and liveness properties are defined, and the use of logics and automata as specifications is discussed. Additionally, the innovative solutions to verifying system upgrades and smart contracts will be presented.

 

PREREQUISITES
Algorithms & Complexity

 

REFERENCES

  • Technical papers and reference manuals related to case studies provided by the Professor.

Persone

 

Sharygina N.

Docente titolare del corso

Informazioni aggiuntive

Semestre
Autunnale
Anno accademico
2019-2020
ECTS
6
Lingua
Inglese
Offerta formativa
Master of Science in Financial Technology and Computing, Corso a scelta, Corso, 2° anno

Master of Science in Informatics, Corso a scelta, Corso, 1° anno

Master of Science in Informatics, Corso a scelta, Corso, 2° anno

Dottorato in Scienze informatiche, Corso a scelta, Corso, 1° anno (4 ECTS)

Dottorato in Scienze informatiche, Corso a scelta, Corso, 2° anno (4 ECTS)