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

Português

Prerequisites

.

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

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

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 tests and the exam will be in-person. The tests are closed book. The exam is closed book, but students are allowed to bring a handwritten A4 sheet of paper.

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. Exercises and projects should be carried out in groups of 2.

All grades are rounded to one decimal, except the final grade which is rounded to the unit.

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.

Programs

Programs where the course is taught: