Objetivos e enquadramento
No desenvolvimento de sistemas informáticos de software ou hardware é essencial garantir a sua correção em relação à especificação inicial. No ciclo de produção, o tempo gasto em verificação tem levado a indústria a procurar a utilização de métodos formais de verificação em detrimento de métodos ad-hoc baseados em testes/simulação, que dificilmente cobrem todos os casos e não permitem garantir de forma rigorosa a fiabilidade e segurança dos sistemas. A verificação, sendo um imperativo na área dos sistemas críticos e de tempo real, tem vindo a ser estendida a outras áreas dos sistemas informáticos (p.e. ao comércio eletrónico). Neste contexto, a unidade curricular de Verificação de Programas tem como objetivo a introdução a técnicas formais de verificação de sistemas informático em sistemas dedutivos. Pretende-se que o aluno:
Goals
In the development of software or hardware computer systems it is essential to ensure their correction in relation to formal specifications.
This course aims to introduce to formal methods using deductive systems for certification of program properties.
Students should:
Programa e conteúdos
O programa da unidade curricular inclui os seguintes tópicos:
No desenvolvimento de sistemas informáticos de software ou hardware é essencial garantir a sua correção em relação à especificação inicial. No ciclo de produção, o tempo gasto em verificação tem levado a indústria a procurar a utilização de métodos formais de verificação em detrimento de métodos ad-hoc baseados em testes/simulação, que dificilmente cobrem todos os casos e não permitem garantir de forma rigorosa a fiabilidade e segurança dos sistemas. A verificação, sendo um imperativo na área dos sistemas críticos e de tempo real, tem vindo a ser estendida a outras áreas dos sistemas informáticos (p.e. ao comércio eletrónico). Neste contexto, a unidade curricular de Verificação de Programas tem como objetivo a introdução a técnicas formais de verificação de sistemas informático em sistemas dedutivos. Pretende-se que o aluno:
- perceba a importância da utilização da lógica e dos sistemas formais no desenvolvimento de sistemas informáticos complexos;
- seja capaz de anotar programas simples duma linguagem imperativa ou orientada a objetos de modo a garantir propriedades de segurança e propriedades funcionais; e de especificar teorias que permitam a modelação de estruturas mais complexas, cuja correção será demonstrada por um demonstrador automático ou interativo;
- adquira conceitos básicos de demonstradores automáticos de teorias lógicas decidíreis (SMT-provers) e demonstradores interactivos
- adquira os princípios básicos de modo a permitir-lhe a utilização das ferramentas adequadas de verificação (formal) na sua vida profissional futura ou o desenvolvimento de trabalhos de investigação na área de métodos formais;
Goals
In the development of software or hardware computer systems it is essential to ensure their correction in relation to formal specifications.
This course aims to introduce to formal methods using deductive systems for certification of program properties.
Students should:
- realize the importance of using logic and formal systems in the development of complex it systems;
- be able to annotate simple programs in an imperative or object-oriented language to ensure safety properties and functional properties; and to specify theories that allow the modeling of more complex structures, the correction of which will be demonstrated by an automatic or interactive theorem prover;
- acquire basic concepts of automatic solvers (SMT-solvers) and interactive theorem provers
- acquire the basic principles in order to allow to use the appropriate (formal) verification tools in future working life or the development of research in the field of formal methods;
Programa e conteúdos
O programa da unidade curricular inclui os seguintes tópicos:
- Breve introdução aos métodos formais e a técnicas de verificação formal.
- Verificação de Dedutiva de Programas
- Cálculos de correção parcial e total (Lógicas de Hoare).
- Pré-condições mais fracas e algoritmos de geração de condições de verificação.
- Verificação de segurança e verificação funcional.
- Ferramentas para a especificação, verificação e certificação de programas imperativos: geradores de condições de verificação.
- Correção de programas simples sobre inteiros e estruturas de dados usuais
- 3 Demonstração Automática e Interactiva
- Satisfazibilidade para a lógica proporcional
- Resolutores DPLL baseados em CDCL (SAT)
- Teorias decidíveis: inteiros, reais, arrays, apontadores, etc.
- SMT, algoritmos de decisão e sua combinação.
- Utilizador de uma ferramenta de demonstração automática (p.e Z3)
- Breve introdução aos tipos dependentes e ao demonstrador interactivo Coq (ou similar)
- Brief introduction to formal methods and formal verification
- Deductive verification
- - Partial and total correctness calculus (Hoare logics) .
- Weak-preconditions and verification condition generators .
- Tools for the speciification, verification and certification programs (Dafny)
- Correction of imperative and object oriented programs with Dafny
- 3 Automatic theorem provers : SAT and SMT solvers
- Proposition satisfiability problem (SAT) . Decidable theories : integers , reals , arrays, pointers etc.
- SMT: Satisfiability modulo theories : algorithms and combination . SMT tools (Z3)
- 4 Brief introduction to interactive theorem provers