Rigorous Software Engineering (252-0216)
Course at D-INFK of ETH Zürich, Spring Semester 2020 , Felix Friedrich and Hermann Lehner and Malte Schwerhoff
Course at D-INFK of ETH Zürich, Spring Semester 2020 , Felix Friedrich and Hermann Lehner and Malte Schwerhoff
| Date | Message |
|---|---|
| 12.5.2020 | No exercise sheet published this week. The exercise sessions of week May 18-22 are cancelled! |
| 10.5.2020 | Special guest lecture by Petar Tsankov on testing and verification of smart contracts on 13th May. Q&A and additional demos during the lecture slot; please watch the video ahead of time. |
| 8.5.2020 | Project Q&A on Tuesday, 12th April, at 9:00 sharp on Zoom (otherwise no lecture) |
| --- | |
| 23.4.2020 | We will offer a project Q&A on Wednesday, April 29, starting 4.30pm (the zoom link was sent out by mail). |
| 24.3.2020 | A Zoom session will be held during regular lecture hours. Either video + Q&A, or just Q&A. Link: see below. |
| 23.3.2020 | We have set up a page containing information about the project here. |
| 21.3.2020 | Lecture 24.03. published. Optional Zoom meeting for Q&A starts 24.03. at 8:15, see link below. |
| 13.3.2020 | we have set up a webpage containing all relevant information regarding remote lectures and exercises (see below) |
| 13.2.2020 | exercise sessions start in the second week of the semester (24.02.), no sessions during the first week |
| 28.1.2020 | website first version |
All lectures and exercise sessions are conducted remotely. You can find all information under the link below (use your ETH account to log in).
| Lectures | Room |
|---|---|
| Tuesday 08:15 - 10:00 | (online) |
| Wednesday 10:15 - 12:00 | (online) |
link : includes a forum to ask questions, options to enroll for the projects groups etc:
This is a plan. No plan survives contact with reality. We will constantly update lecture material before the lectures.
| Number | Date | Topic and Slides |
|---|---|---|
| 1 | Tue 18.02. | FF: Introduction: Software Failures, Challenges, Solution Approaches |
| 2 | Wed 19.02. | FF: Requirements Elicitation |
| 3 | Tue 25.02. | HL: Modeling and Specification (1): Code Documentation |
| 4 | Wed 26.02. | HL: Modeling and Specification (2): Informal Models (UML) |
| 5 | Tue 03.03. |
FF: Modeling and Specification (3): Formal Models (Alloy): Examples and Logic Alloy examples: Spouse CeilingsAndFloors LinkedList |
| 6 | Wed 04.03. |
FF:
Modeling and Specification (4): Formal Models (Alloy) : Language and static Models Alloy examples: FileSystem RefCountList |
| 7 | Tue 10.03. |
FF: Modeling and Specification (5): Formal Models (Alloy) dynamic Models / Analyzing Models Alloy examples: FileSystemStatic ArrayUpdate FileSystemDynamic ArrayFind FileSystemInvariants NodeConsistency NodeValidity |
| 8 | Wed 11.03. | HL: Modularity: Coupling and Design Patterns |
| 9 | Tue 17.03. |
HL: Modularity: Adaptation Recording (Login with ETH Account) |
| 10 | Wed 18.03. |
HL: Testing: Test Stages and Strategies Recording (Login with ETH Account) |
| 11 | Tue 24.03. | MS: Introduction to Analysis (Slides, Recordings) |
| 12 | Wed 25.03. | MS: Introduction to Analysis (Slides, Recordings) |
| 13 | Tue 31.03. | MS: Mathematical Background for Analysis (Slides, Recordings) |
| 14 | Wed 01.04. | MS: Mathematical Background for Analysis (Slides, Recordings) |
| 15 | Tue 07.04. |
MS: Mathematical Background for Analysis
(Slides, Recordings),
Applying the Theory - Intervals (Slides, Recordings) |
| 16 | Wed 08.04. | MS: Applying the Theory - Intervals (Slides, Recordings) |
| - | Tue 14.04. | -- Easter Break -- |
| - | Wed 15.04. | -- Easter Break -- |
| 17 | Tue 21.04. | MS: Applying the Theory - Intervals (Slides, Recordings) |
| 18 | Wed 22.04. | MS: Pointer and Alias Analysis (Slides, Recordings) |
| 19 | Tue 28.04. |
MS: Pointer and Alias Analysis
(Slides, Recordings)
Application of Concepts - Analysis of HPC/GPU programs (Slides, Recordings) |
| 20 | Wed 29.04. | MS: Application of Concepts - Analysis of HPC/GPU programs (Slides, Recordings) |
| 21 | Tue 05.05. | MS: Symbolic Execution for Testing (Slides, Recordings) |
| 22 | Wed 06.05. | MS: Symbolic Execution for Testing (Slides, Recordings) |
| 23 | Tue 12.05. |
MS: project Q&A at 9:00 sharp on Zoom
(plus optional video on abstract interpretation) |
| 24 | Wed 13.05. |
PT: Smart Contract Security - Testing and Formal Verification
(Slides, Recordings)
Guest lecture by Petar Tsankov |
| 25 | Tue 19.05. | HL: Testing: Functional Testing |
| 26 | Wed 20.05. | HL: Testing: Structural Testing |
| 27 | Tue 26.05. | HL: Testing: Structural Testing cont'd |
| 28 | Wed 27.05 | HL/FF/MS: Testing, Wrap-up |
| Number | Topic | Exercise | Solution |
|---|---|---|---|
| 1 | Requirements Elicitation and Documentation | Exercise 1 [PDF] | Solution 1 [PDF] |
| 2 | Contracts and UML Class Diagrams | Exercise 2 [PDF] | Solution 2 [PDF] |
| 3 | UML Sequence Diagrams and Alloy | Exercise 3 [PDF], Files [ZIP] | Solution 3 [PDF] |
| 4 | Dynamic Alloy Models | Exercise 4 [PDF], Files [ZIP] | Solution 4 [PDF], Files [ZIP] |
| 5 | Coupling and Design Patterns | Exercise 5 [PDF], Files [ZIP] | Solution 5 [PDF], Files [ZIP] |
| 6 | First Steps with Abstract Interpretation | Exercise 6 [PDF] | Solution 6 [PDF] |
| 7 | Mathematical Concepts | Exercise 7 [PDF] | Solution 7 [PDF] |
| 8 | Abstract Interpretation and Intervals | Exercise 8 [PDF] | Solution 8 [PDF] (updated) |
| 9 | Widening and Pointer Analysis | Exercise 9 [PDF] | Solution 9 [PDF] |
| 10 | Verifying Determinism | Exercise 10 [PDF] | Solution 10 [PDF] |
| 11 | Symbolic Execution | Exercise 11 [PDF] | Solution 11 [PDF] |
| 12 | Testing | Exercise 12 [PDF] | Solution 12 [PDF] |
Please register for an exercise group via MyStudies.
For many kinds of general questions (administrative, technical, theoretical ...) the first option is to ask in the forum we have set up in Moodle.
If this does not help, or you have a question specific for your case, please contact the assistant assigned to you.
If the assistant cannot help you, contact the chef assistant.
If the chef assistant cannot help you, contact one of the lecturers.