Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager OPAM (disponível em Homebrew para Max OSX).
Máquina virtual com todas as ferramentas instaladas.
Docente | Foto![]() | Horário | Sala |
---|---|---|---|
Maria João Frade | ![]() | 5a-feira, 14h-17h | Sala E7 1.10 |
NB: poderá haver trocas de horário entre VF e AC de acordo com necessidades de serviço dos docentes das duas disciplinas.
“Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.”
Tratando-se de uma ferramenta de prova inovadora, e não de um verificador de programas, espera-se:
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
Tratando-se de uma ferramenta de prova, e não de um verificador de programas, espera-se:
"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs."
Tratando-se de uma ferramenta de prova que já foi abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories and basic programming data structures. A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 can be easily extended with support for new theorem provers. Why3 can be used as a software library, through an OCaml API."
Tratando-se de uma ferramenta já abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
"Boogie
is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#.
Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.
The Boogie research project is being developed at Microsoft Research."
Espera-se:
Dafny é uma ferramenta da Microsoft Research baseada numa linguagem de programação dedicada para verificação dedutiva (tal como Why3), utilizando como VCGen uma outra ferramenta da Microsoft Research, chamada Boogie.
Espera-se:
O KeY é uma ferramenta de verificação dedutiva bem estabelecida que ganhou recentemente visibilidade acrescida, pelo facto de ter permitido identificar um bug em algoritmos de ordenação implementados em bibliotecas standard (Java, Python). A lógica de programas subjacente é uma lógica dinâmica, em vez da mais comum lógica de Hoare / WP calculus.
Espera-se:
O VeriFast é uma ferramenta de verificação dedutiva tendo por base a lógica de programas conhecida como “separation logic”, o que, em teoria, lhe confere algumas vantagens sobre ferramentas baseadas em lógica de Hoare / WP calculus.
“VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.”
Espera-se:
“Viper (Verification Infrastructure for Permission-based Reasoning) is a suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages, via translations into the Viper language.
The Viper toolchain is designed to make it easy to implement verification techniques for programs with persistent mutable state (including concurrent programs), providing native support for reasoning about the program state using method permissions or ownership, e.g. in the style of separation logic. New verification techniques can be implemented directly as translations to the Viper language, using either of the verifiers provided.”
Trata-se de uma proposta completa, baseada numa linguagem intermédia, front-ends e back-ends. São disponibilizados dois back-ends, um dos quais recorre ao Boogie.
Espera-se naturalmente uma descrição geral da toolset e princípios subjacentes, abordando:
“SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations.
(…) Currently, SMACK leverages the Boogie and Corral verifiers.”
Trata-se de uma ferramenta para a verificação de código C, mas que apenas traduz para BoogiePL, sendo depois necessário utilizar uma das ferramentas referidas como back-end. O grupo deve começar por escolher uma das ferramentas; o trabalho diz respeito ao toolset completo, compreendendo o SMACK e a ferramenta (VCGen) escolhida.
Espera-se:
Nome | Número | Projecto |
---|---|---|
Afonso Rafael Carvalho Sousa | A74196 | Viper |
Jorge Fernando Alves da Cruz | A78895 | Viper |
Alexandre Miguel Costa Dias | A78425 | SMACK |
Gonçalo Medeiros São Pedro Raposo | A77211 | SMACK |
Armando João Isaias Ferreira dos Santos | A77628 | Lean |
Gonçalo Nuno Esteves Duarte | A77508 | Lean |
Artur Jorge Gomes Queiroz | PG38014 | Coq |
Nelson Santos Loureiro | PG37020 | Coq |
Diogo Manuel Macedo e Silva | A79021 | Boogie |
Tiago André Araújo Monteiro | A78961 | Boogie |
Francisco Fernando Vilela Araújo | A79821 | Why3 |
Fábio Rafael Pereira Araújo | A78508 | Why3 |
Joana Fernandes Cunha | PG38929 | Isabelle |
João Manuel da Silva Gomes Fernandes | PG38930 | Isabelle |
José Carlos do Vale e Sousa | A74678 | Verifast |
Patrícia Filipa Bouça Barreira | A79007 | Dafny |
Pedro Henrique Moreira Gomes Fernandes | A77377 | Dafny |
Pedro Faria Durães da Silva | A78434 | KeY |
Pedro Miguel Gomes da Silva | PG38935 | KeY |
Ricardo Guerra Leal | A75411 |