Opções de inscrição
Como garantir que um sistema de software se comportará corretamente mesmo diante de situações complexas e inesperadas? Este curso apresenta os fundamentos da verificação de modelos (Model Checking), uma das principais técnicas formais para analisar automaticamente se sistemas satisfazem propriedades desejadas.
Iniciaremos com os conceitos fundamentais de sistemas de transição e com o estudo de propriedades de safety, liveness e fairness. Em seguida, exploraremos as lógicas temporais LTL e CTL, discutindo suas diferenças, expressividade e os principais algoritmos utilizados para a verificação de modelos. Avançaremos então para técnicas de verificação de sistemas probabilísticos, incluindo DTMCs (Discrete-Time Markov Chains) e MDPs (Markov Decision Processes), além de abordar os fundamentos da verificação simbólica de modelos, essenciais para lidar com sistemas de maior escala. Ao longo do curso, os conceitos teóricos serão complementados por exercícios e atividades práticas, permitindo aos alunos experimentar as técnicas e algoritmos estudados. O curso também inclui um projeto individual, no qual os conhecimentos adquiridos serão aplicados à análise de um sistema ou problema concreto. A participação ativa dos alunos nas aulas de exercícios será parte importante do processo de aprendizagem.
Ao final do curso, espera-se que os alunos sejam capazes de compreender os fundamentos da verificação de modelos, formular propriedades utilizando lógicas temporais e aplicar diferentes técnicas de model checking a sistemas determinísticos e probabilísticos.
