Software Construction and Verification
Code
11159
Academic unit
Faculdade de Ciências e Tecnologia
Department
Departamento de Informática
Credits
6.0
Teacher in charge
Luís Manuel Marques da Costa Caires
Weekly hours
4
Teaching language
Português
Objectives
Knowledge:
Students consolidate their software construction skills for building trustworthy software, in the broad context of modern software systems, where concurrency and security are major concerns.
The CU develops the perspective that verification should be tightly integrated with the software construction process, guided by the use of code analysis tools, such as those made available by Microsoft Research (http://rise4fun.com).
Basic static analysis and software model-checking techniques are also covered, as well as principles and techniques for sofware testing.
Knowledge Application:
Use programming methods and verification techniques to enforce safety of monitor based concurrent programs (using java.util.concurrent) and transactions.
Specify information flow policies for a sofware system and verify that the policies are enforced using assertions and tools.
Develop, in team work, a project of a statically verified and tested (with resonable coverage) medium scale application.
Use logical assertions to specify, check, and reason about program correctness, and associated tools (DAFNY, VERIFAST, JIF).
Specify behavioral specifications (invariants, pre-conditions and post-conditions) for module implementations and their interfaces.
Develop test plans and implement them.
Prerequisites
Programming practice and basic knowledge of object oriented programming, data-structures, and elementary logic.
Subject matter
1. Verified Software Construction
Assertion methods and Hoare and Separation Logic; Assertion Inference; Abstract and Behavioral types. Representation Invariants. Abstract interpretation; Model-checking. Tools.
2. Software Testing Model-based testing; Test selection and test generation; Fault-based testing. Symbolic execution; Automated testing. Tools.
3. Concurrent Programming
Sharing, confinement, ownership. Control of interference. Reasoning about concurrent code with monitors and locks based on resource invariants. Construction of concurrency control code from behavioral specs.
4. Secure Programming
Information flow security and non-interference. Language based security. Programming models for access control. Certification of code. Tools.
5. Hands On Exercises / Final Project
Sequence of programming challenges, involving tool usage (Dafny, JBoss, Verifast, SPIN; Jif). Final (team work) project.
Bibliography
Dafny Guide : http://rise4fun.com/Dafny/tutorial/guide
"Program Development In Java: Abstraction, Specification, And Object-Oriented Design". Liskov/Guttag; MIT Press.
Java Concurrency in Practice, Goetz et al. Addison-Wesley, 2006.
VeriFast for Java: A Tutorial Jan Smans, Bart Jacobs, and Frank Piessens (http://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast-java-tutorial.pdf).
Language Based Information Flow Security, A. Sabelfeld, A. C. Myers, 2004.
Several classical papers by Liskov, Hoare, Dijkstra, Brinch Hansen, Doug Lea, O’Hearn, Schneider.
Related course ar MIT: http://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-005-elements-of-software-construction-fall-2011/index.htm
Evaluation method
Midterm test: 40%
Final Test: 40%
4 small handhouts: 5% each
The two first handouts will be integrated in a single one (worth 10%)