The course covers principles, methods, techniques and tools for the dependable and trustworthy construction and validation of software systems, ensuring as much as possible the absence of programming errors ("bugs"), with a focus on CONCURRENCY and SAFETY.

We will use advanced tools, such as those made available by Microsoft Research in the sitehttp://rise4fun.com and Facebook (INFER), and used by major software companies such as Microsoft, Amazon and Facebook.

This course is a must for all students that wish to master advanced software construction techniques, in particular for concurrent and safe software, an important professional asset.

By the end of the course, students will be able to clearly reason about the correction and safety of developed software, to use sophisticated software analysis tools, to develop and interpret test suites and to write concurrent software.

Example of final project: In 12/13 students developed a concurrent web-server,fully certified for absence of concurrency errors (data races) null reference errors and memory leaks.

The course basic language is Java, but we will also use other programmung languages and tools (e.g., JAVASCRIPT, DAFNY, INFER).

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.

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.

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.

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

Programming practice and basic knowledge of object oriented programming, data-structures, and elementary logic.