Sumários
Essay presentations by Students
15 Dezembro 2021, 18:30 • Antónia Lopes
Essay presentations:
- Alloy, A language and tool for exploring software designs BY Duarte Sousa, Tiago Murteira, Tiago Varela
- CBMC A bounded model checker for c and c++ programs BY Gonçalo Lobo, João Serrano
- Frama-C, A platform to make your c code safer and more secure BY Daniel Machado, Luís Gonçalves
- Infer, A tool to detect bugs in Java and c/c++ code BY João Francês, Marisa Mourão, Rodrigo Albino
- PRISM, A probabilistic model checker BY André Silva, Catarina Lima, Cláudio Lamelas
- SideTrail, Verifying Time-balancing of Criptosystems BY Gonçalo Rocha, José Madeira
- UPPAL, Modeling and verification of real-time systems BY João Ferreira
Essay presentation by students
15 Dezembro 2021, 16:30 • Antónia Lopes
Essay presentations:
- Alloy, A language and tool for exploring software designs BY Duarte Sousa, Tiago Murteira, Tiago Varela
- CBMC A bounded model checker for c and c++ programs BY Gonçalo Lobo, João Serrano
- Frama-C, A platform to make your c code safer and more secure BY Daniel Machado, Luís Gonçalves
- Infer, A tool to detect bugs in Java and c/c++ code BY João Francês, Marisa Mourão, Rodrigo Albino
- PRISM, A probabilistic model checker BY André Silva, Catarina Lima, Cláudio Lamelas
- SideTrail, Verifying Time-balancing of Criptosystems BY Gonçalo Rocha, José Madeira
- UPPAL, Modeling and verification of real-time systems BY João Ferreira
Aula não foi lecionada
15 Dezembro 2021, 15:00 • Antónia Lopes
A aula estava reservada para apresentação do ensaio dos alunos, mas face ao reduzido número de alunos que se propuseram apresentar o ensaio, não foi necessário usar esta aula.
Model Checking IV
24 Novembro 2021, 16:30 • Antónia Lopes
- Exploring the search space in presence of an LTL formula
- Never claims for a safety properties
- Never claims for a liveness properties
- Optimizing the performance of verifications
- The sources of complexity of model checking
- Write efficient models
- Understand how Spin allocates memory for the hash table
- Compress the state vector
- Bitstate hashing
- Use a minimal automaton