Lectures: Tue 12:20, S10 (Pavel Parízek)
Labs: Tue 14:00, S10 (Pavel Parízek)
Page in SIS: NSWI132
Grading: Credit and exam
News
- The third homework assignment is available here. The deadline for submitting your complete solutions is on May 26th, 2024 at 23:59.
- The fourth homework assignment is available here. The deadline for submitting your complete solutions is on June 30th, 2024 at 23:59.
- The fifth homework assignment is available here.
Slides
Lectures
| Date | Title | Downloads |
|---|---|---|
| 20.2.2024 | Introductory lecture | lecture00.pdf |
| 27.2.2024 | Model Checking Programs | lecture01.pdf |
| 5.3.2024 | Concurrency Errors | lecture02.pdf |
| 12.3.2024 | Symbolic Execution, Dynamic Analysis | lecture03.pdf |
| 19.3.2024 | Deductive Methods, Bounded Model Checking | lecture04.pdf |
| 26.3.2024 | Abstraction | lecture05.pdf |
| 2.4.2024 | Contracts: Specification and Verification | lecture06.pdf |
| 23.4.2024 | Static Analysis: Overview, Data-Flow | lecture07.pdf |
| 23.4.2024 | Static Analysis: Pointers and Heap Structures | lecture08.pdf |
| 30.4.2024 | Abstract Interpretation | lecture09.pdf |
| 7.5.2024 | Combining Verification Approaches | lecture10.pdf |
| 7.5.2024 | Program Termination | lecture11.pdf |
| 21.5.2024 | Program Synthesis | lecture12.pdf |
Labs
| Date | Title | Downloads |
|---|---|---|
| 27.2.2024 | Java PathFinder | lab01.pdf |
| 5.3.2024 | Detecting Concurrency Errors with JPF | lab02.pdf, concur_bench.zip |
| 12.3.2024 | Tools for Symbolic Execution and Dynamic Analysis | lab03.pdf |
| 19.3.2024 | SMT Solvers, CBMC | lab04.pdf, smt-examples.zip, bmc-examples.zip |
| 26.3.2024 | CEGAR | lab05.pdf, cegar.tgz |
| 2.4.2024 | Contracts: Dafny, Viper | lab06.pdf, dafny-examples.zip |
| 23.4.2024 | T.J. Watson Libraries for Analysis | lab07.pdf, wala-examples.zip |
| 23.4.2024 | Static Analysis Tools | lab08.pdf, pointers-examples.zip, predator-examples.tgz |
| 30.4.2024 | Realistic Verification Scenarios | lab09.pdf |
Annotation
Basic principles of automated analysis and verification of programs (model checking, static analysis, dynamic analysis, and deductive methods) and their practical applications (e.g., detecting concurrency errors).
Syllabus
- Model checking of programs
- Detecting concurrency errors
- Symbolic execution
- Dynamic analysis
- Introduction to deductive methods
- SAT solvers, SMT solvers
- Bounded model checking
- Predicate abstraction and CEGAR
- Selected applications of deductive methods in software verification
- Verification of program code against contracts
- Static analysis and its usage in program verification
- Abstract interpretation
- Combination of verification techniques
- Program termination
- Program synthesis
Organization
During the lectures we will describe individual program verification and analysis methods, including basic concepts, main algorithms, and their limitations.
The purpose of the lab is to provide students with a hand-on experience with selected verification and analysis tools ( Java Pathfinder, CBMC, Dafny, WALA, ...).
Homework assignments
There will be five assignments, each taking approximately 10-15 hours of homework. You need to do the assignment no. 5 (presentation of some research publication) and two others to get credit (“zápočet”).
Note: 10% of your score will be deducted for every calendar day your solution of the assignment is late. This implies that no solutions will be accepted after 10 calendar days past its due date.
| Date | Title | Downloads |
|---|---|---|
| 2.4.2024 23:59 | Java Pathfinder | hw1-jpf.pdf, daisyfs.zip, elevator.zip, repworkers.zip |
| 30.4.2024 23:59 | Contracts | hw2-contracts.pdf |
| 26.5.2024 23:59 | Static Analysis | hw3-static.pdf |
| 30.6.2024 23:59 | Finding Bugs in Real Software | hw4-realsw.pdf |
| 21.5.2024 | Research Papers | hw5-papers.pdf |
Grading
Final grades will depend on the quality of your homework and on the result of the voluntary final exam as follows:
- Homework assignments (0-20 points for each of them)
- Final exam (0-25 points)
Grades will be based on points in the following way:
| Grade | Required points |
|---|---|
| Excellent: | 85-125 points |
| Very good: | 72-84 points |
| Good: | 60-71 points |
References
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking, MIT Press, 2000
- F. Nielson, H. R. Nielson, and Chris Hankin. Principles of Program Analysis, Springer, 2005
- D. Kroening and O. Strichman. Decision Procedures: An Algorithmic Point of View, Springer, 2008
Archive
Academic year 2015/2016: lectures labs tools & examples