Software Construction and Verification
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.
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.
General characterization
Code
11159
Credits
6.0
Responsible teacher
Bernardo Parente Coutinho Fernandes Toninho, Luís Manuel Marques da Costa Caires
Hours
Weekly - 4
Total - 52
Teaching language
Inglês
Prerequisites
.
Bibliography
Dafny Guide : http://dafny.org/latest/DafnyRef/DafnyRef
"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
Teaching method
The course lectures introduce different topics in the course''''s syllabus. Hoare Logic, Separation Logic, and the corresponding usage in software verification tools.
Laboratory classes are composed of exercises using software verification tools and project development using mainstream programming languages and dedicated verification tools.
Evaluation method
The grading is made up of two components: theoretical-practical and practical.
The theoretical-practical component weighs 60% of the final grade and has a minimum requirement of 9.5 points. The grade is made up of two tests of equal weight, or an exam. The tests and the exam are in-person. The tests and the exam are closed book.
The practical component weighs 40% of the final grade and has a minimum requirement of 9.5 points in order to obtain frequência. The practical component is made up of 3 specification and verification exercises (of equal weight). The exercises should be completed in groups of two students and the grades may require an oral or written discussion.
All grades will be rounded to one decimal place, except the final grade which will be rounded to the nearest integer value.
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. Hands On Exercises / Final Project
Sequence of programming challenges, involving tool usage (Dafny, JBoss, Verifast, SPIN; INFER). Final (team work) project.