Software Construction and Verification
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.
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.
João Ricardo Viegas da Costa Seco, Luís Manuel Marques da Costa Caires
Weekly - 4
Total - Available soon
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
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.
Grading consists of two components. A summative part with a weight of 70% in the final grade and a minimum grade of 9,5 points. It consists of two tests of equal weight or an exam. The practical component has a weight of 30% in the final grade and a minimum grade of 9,5 points. 10% of the practical grade corresponds to two exercises, and 20% corresponds to a verification project of medium size.
The first test would occur online, using moodle, proctoring mechanisms and a webcam in a different device. The second test and the exam will be on campus, if possible.
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.
Programs where the course is taught: