Trabalho de revisão
O exame da disciplina é constituído por a realização de um resumo e uma apresentação oral (possivelmente acompanhada de slides) com a duração de cerca de 20 minutos. Data é 11 de Julho de 2012, no anfiteatro 2 a partir das 9 horas.
O exame será cotado para 5 valores, sendo os restantes 15 distribuídos pelos trabalhos práticos apresentados.
O exame será cotado para 5 valores, sendo os restantes 15 distribuídos pelos trabalhos práticos apresentados.
Temas
Cada proposta é constituída por um tema e bibliografia associada, e eventualmente uma aplicação de software. Pretende-se que com base nessas informações o aluno escreva um pequeno resumo sobre um tema proposto (cerca de 6-10 páginas) e depois prepare um apresentação oral (que deverá ser acompanhada de ``slides''). A cada aluno é atribuído um tema diferente. A distribuição abaixo pode ser alterada por troca entre dois alunos ou por substituição do tema por algum não atribuído (ou proposto pelo aluno).A distribuição final será feita a 15 de Junho.
Os resumos deverão ser entregues até 24h antes da data do exame.
Cada proposta é constituída por um tema e bibliografia associada, e eventualmente uma aplicação de software. Pretende-se que com base nessas informações o aluno escreva um pequeno resumo sobre um tema proposto (cerca de 6-10 páginas) e depois prepare um apresentação oral (que deverá ser acompanhada de ``slides''). A cada aluno é atribuído um tema diferente. A distribuição abaixo pode ser alterada por troca entre dois alunos ou por substituição do tema por algum não atribuído (ou proposto pelo aluno).A distribuição final será feita a 15 de Junho.
Os resumos deverão ser entregues até 24h antes da data do exame.
Verificação de programas em C por abstracção de predicadosAtribuição: João Graça
Bilbliografia e Software
Bilbliografia e Software
- Modular Verification of Software Components in C. Transactions on Software Engineering (TSE), Volume 30, Number 6, pages 388-402, June 2004, Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith
- Software Magic
Model Checking para sistemas temporizados: autómatos temporizados
Para a modelação de sistemas de tempo-real um dos formalismos mais usados são os autómatos temporizados que associam a propriedades temporais a noção de relógio.
Atribuição: Hugo Sousa
Bilbliografia e Software
Para a modelação de sistemas de tempo-real um dos formalismos mais usados são os autómatos temporizados que associam a propriedades temporais a noção de relógio.
Atribuição: Hugo Sousa
Bilbliografia e Software
- Timed Automata: Semantics, Algorithms and Tools.Johan Bengtsson and Wang Yi, Uppsala University.
- Software UPPAAL
Anotações e extensões da lógica de Hoare para linguagens orientadas a objectos
A linguagem JML permite a especificação de anotaçõa para programas Java. Pretende-se a identificação das especificações que focam caracteristicas da orientação a objectos: classes, interfaces, invariantes de classe, ``frames'', etc.
Atribuição: José Carvalho
Bilbliografia e Software
A linguagem JML permite a especificação de anotaçõa para programas Java. Pretende-se a identificação das especificações que focam caracteristicas da orientação a objectos: classes, interfaces, invariantes de classe, ``frames'', etc.
Atribuição: José Carvalho
Bilbliografia e Software
- Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006.
- Software JML web page
Verificação de programas orientados a objectos usando o KeY
Atribuição: Gonçalo Martins
Bilbliografia e Software
Atribuição: Gonçalo Martins
Bilbliografia e Software
- KeY Tool,Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. Software and Systems Modeling, Springer 2005
- Software KeY
Lógicas para sistemas Hibrídos - Keymaera
Sistema híbridos modelo sistemas físicos complexos e pretende-se construir controlos computorizados que verifiquem os requisitos estipulados. São sistema dinâmicos onde os estados evoluem no tempo de acordo com a interligação entre leis discretas e contínuas.
Atribuição: André Gaspar
Bilbliografia e Software
Sistema híbridos modelo sistemas físicos complexos e pretende-se construir controlos computorizados que verifiquem os requisitos estipulados. São sistema dinâmicos onde os estados evoluem no tempo de acordo com a interligação entre leis discretas e contínuas.
Atribuição: André Gaspar
Bilbliografia e Software
- Logic and Compositional Verification of Hybrid Systems. André Platzer
- Logical Analysis of Hybrid Systems. Springer 2010. André Platzer (opcional/consulta)
- Software Keymaera
Teorias decidíveis para resolutores SAT-DPPL: arrays e lógica de apontadores
Os resolutores SMT generalizam a resolução SAT, adicionando a capacidade de lidar com um conjunto de teorias decídíveis. Pretende-se um resumo de procedimentos de decisão para lidar com lógica de arrays e de apontadores.
Atribuição:Susana João
Bilbliografia e Software
Os resolutores SMT generalizam a resolução SAT, adicionando a capacidade de lidar com um conjunto de teorias decídíveis. Pretende-se um resumo de procedimentos de decisão para lidar com lógica de arrays e de apontadores.
Atribuição:Susana João
Bilbliografia e Software
- Daniel Kroening and Ofer Strichman. 2008. Decision Procedures:
- An Algorithmic Point of View (1 ed.). Springer Publishing Company,
- Incorporated. Capítulos 7 e 8. (contactar docente)
- Software SMT-LIB (arrays&pointers theories)
Teorias decidíveis para resolutores SAT-DPPL: vectores de bits
Os resolutores SMT generalizam a resolução SAT, adicionando a capacidade de lidar com um conjunto de teorias decídíveis. Pretende-se um resumo de procedimentos de decisão para lidar com lógica de arrays e de apontadores.
Atribuição: Maria Nelson
Bilbliografia e Software
Os resolutores SMT generalizam a resolução SAT, adicionando a capacidade de lidar com um conjunto de teorias decídíveis. Pretende-se um resumo de procedimentos de decisão para lidar com lógica de arrays e de apontadores.
Atribuição: Maria Nelson
Bilbliografia e Software
- Daniel Kroening and Ofer Strichman. 2008. Decision Procedures:
- An Algorithmic Point of View (1 ed.). Springer Publishing Company,
- Incorporated. Capítulo 6 (contactar docente)
- Software SMT-LIB (bit vector theories)
Model Checker SPIN e linguagem de especificação Promela
Atribuição: Armindo Cunha
Bilbliografia e Software
Atribuição: Armindo Cunha
Bilbliografia e Software
- The Model Checker SPIN. G. Holzmann.IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 23, NO. 5, MAY 1997
- Software Spin
SLAM2
Atribuição: João Viana
Bilbliografia e Software
Atribuição: João Viana
Bilbliografia e Software
- SLAM2: Static Driver Verification with Under 4% False Alarms. Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin. FMCAD 2010
- A Decade of Software Model Checking with SLAM. THOMAS BALL, VLADIMIR LEVIn, AnD SRIRAM K. RAJAMANL. Communications of the ACM , july 2011, vol. 54, no. 7(opcional)
- Software SLAM
Nested words e Visibility pushdown languages
Modelação de extensões de model checking de software para sistemas "independentes de contexto".
Atribuição: Francisco Mota
Bilbliografia e Software
Modelação de extensões de model checking de software para sistemas "independentes de contexto".
Atribuição: Francisco Mota
Bilbliografia e Software
- Software model checking using languages of nested trees.Rajeev Alur, Swarat Chaudhuri, P. Madhusudan. ACM Trans. Program. Lang. Syst. 33(5): 15 (2011)
WHY3
Linguagem Why3ML
Atribuição: Nuno Peralta
Bilbliografia e Software
Linguagem Why3ML
Atribuição: Nuno Peralta
Bilbliografia e Software
- Why3: Shepherd Your Herd of Provers. François Bobot, J. C. Filliâtre, Claude Marché, Andrei Paskevich(BOOGIE 2011)
- Verifying Two Lines of C with Why3: an Exercise in Program Verification. J. C. Filliâtre VSTTE12
- Software WHY3
Alloy: Modelação Relacional de Sistemas
Atribuição: Tiago Melo
Bilbliografia e Software
Atribuição: Tiago Melo
Bilbliografia e Software
- Alloy: A Lightweight Object Modelling Notation.Daniel Jackson.ACM Transactions on Software Engineering and Methodology (TOSEM) 2002
- Dependable Software by Design, Daniel Jackson, Scientific American 2006.
- Software Abstractions. Daniel Jackson. The MIT Press,2006.
- Software Alloy
Boogie
Linguagem intermédia e ferramente de verificação para .NET (Spec #)
Atribuição: Armindo Pereira
Bilbliografia e Software
Linguagem intermédia e ferramente de verificação para .NET (Spec #)
Atribuição: Armindo Pereira
Bilbliografia e Software
- Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer et al. editors, Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, volume 4111 of LNCS, pages 364–387. Springer, September 2006.
- Software Boogie
VCC: um verificador para C concurrente
Atribuição: João Proença
Bilbliografia e Software
Atribuição: João Proença
Bilbliografia e Software
- Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies, VCC: A Practical System for Verifying Concurrent C, in Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Springer, 2009
- Software VCC
Dafny: uma linguagem e um verificador para correção funcional
Atribuição:
Bilbliografia e Software
Atribuição:
Bilbliografia e Software
- Getting Started with Dafny: A Guide.Jason KOENIG, K.RustanM.LEINO. 2011
- Software Dafny
Model Checking para sistemas probabilisticos
Para sistemas baseados em cadeias de Markov, pode-se associar uma lógica temporal probabilistica
Atribuição:
Bilbliografia e Software
Para sistemas baseados em cadeias de Markov, pode-se associar uma lógica temporal probabilistica
Atribuição:
Bilbliografia e Software
- Model Checking Linear-Time Properties of Probabilistic Systems. Christel Baier, Marcus Grosser, and Frank Ciesinski. Cap. 13 (1-4) em Handbook of Weighted Automata, M. Droste et al Eds, 2011,