A disciplina visa introduzir o estudante na vida universitária pela compreensão do processo de formação docente na área de Computação, em especial, no contexto das licenciaturas, da regulação e da avaliação de cursos de graduação e dos campos profissionais de ação e de pesquisa docente.
Essa disciplina visa estudar conceitos de linguagens de programação e implicações deles na construção de softwares. O entendimento desses conceitos facilita ao programador desenvolver softwares mais eficientes e com menos erros.
Ao final do curso o aluno deverá saber comparar linguagens de programação; compreender os paradigmas procedural, lógico e funcional; ter noção de programação em Hugs e em Prolog; e conhecer modelos básicos utilizados na tradução de linguagens de programação e no controle de subprogramas.
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.
