There are two lectures per week, on Monday and Thursday. Students are encouraged to take their own notes during lectures. A preliminary lecture plan is below.

Week

Monday 15.15-17.00

(see location in TimeEdit)

Thursday 8.00-9.45

(see location in TimeEdit)

45

Course Intro

Admin, motivation, examples for the course.

Testing 1

Triangle quiz, Test Suite Construction, Coverage criteria

Lecture slides
Install Java (Bring your Laptop with you!)
Download this program: TriangleChecker.java
Readings: Ch 1-2, 5 from Book (Get an idea only)

46

Testing 2

Logic coverage criteria, Black box testing: Input space partitioning.

Lecture slides
Menti slides
Readings: Ch6-8 from Book (Get an idea only)

Testing 3

Test Automation: Intro to JUnit, extreme testing, test driven development.
- Lecture slides
- Readings: Ch3 from Book
- Download these classes: Examples.zip

47

Testing 4

Testing Foundations, Failure model, Complexity of Testing.

Lecture slides
Ex solution (depend on the proposed solution)
titan_1999_rpt.doc

Debugging

Input minimisation, systematic debugging, logging etc.

Lecture slides
ex solution
Readings: Ch5 from Book
Code: 5-Examples.zip

48

Formal Specification 1

Introduction and Logic.

Lecture slides
Code: Examples.zip

Formal Specification 2

Introduction to Dafny.

49

Formal Specification 3

Framing and loops in Dafny.

Lecture slides
Code: Examples.zip
Readings: Tutorial

Formal Verification

Weakest pre-condition calculus.

Lecture slides
Readings: Link (notations can be different)

50

Formal Verification continue

Correctness of programs with loops: invariants, variants, partial/total correctness.

Lecture slides
Readings: link
Weakest Precondition: link

More on Specification and Verification

51

Speaker:

Rustan M. Leino

Title:

Program proofs and their use at AWS

Abstract:

Program verification--the process of developing a program along with its proof of correctness--is applied when the cost of a bug in production is high. AWS is using program verification and other forms of automated reasoning for a growing number of applications. In this talk, I will motivate the use of program verification by giving a brief survey of the AWS use of Dafny, a verification-aware programming language. I will then use a tutorial demo for a problem solved by Dafny.

Speaker bio:

Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct. Leino is known for his work on programming methods and program verification tools and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.

20241216-Chalmers.pptx

20241014-FMCAD-2024.pptx

Previous exam tutorial

Sample exams

52

Self-Study

Self-Study