Program Analysis and Code Verification (NSWI132)
|
| Time and Location: |
Winter Semester 2011/2012
Lectures: Wed 15:40 S1
Lab: Wed 17:20 SU1
|
| Guaranteed by: |
Department of Distributed and Dependable Systems |
| Winter Term: |
2/2 Zk+Z |
| Lecturers: |
Jan Kofroň
e-mail: jan.kofron<at-sign>d3s.mff.cuni.cz
|
| Lab: |
Pavel Jančík
e-mail: pavel.jancik<at-sign>d3s.mff.cuni.cz
|
| Information in SIS: |
NSWI132 |
News
- There WILL BE a lecture on January, 11.
- The first homework assignment can be found at homework1.pdf. The new deadline for the first homework is Nov 23th 2011, 15:30.
- First (introductory) lesson will take place on 2011-10-05 15:40, room S1
- First labs will take place on 2011-10-12 17:20, room SU1
Slides
Lectures
| Date | Topic | Slides |
|---|
| 05.10.2011 |
Introductory lecture (motivation, organization) |
lecture00.pdf |
| 12.10.2011 |
Model checking of programs |
lecture01.pdf |
| 19.10.2011 |
State space explosion, environment construction |
lecture02.pdf |
| 26.10.2011 |
Counter-example Guided Abstraction Refinement |
lecture03.pdf |
| 02.11.2011 |
Lazy abstraction |
lecture04.pdf |
| 09.11.2011 |
SAT Solvers |
lecture05.pdf |
| 16.11.2011 |
Deductive methods: SMT solvers, Theorem provers |
lecture06.pdf |
| 23.11.2011 |
Verification of program code against contracts: Spec# & Boogie |
lecture07.pdf |
| 30.11.2011 |
Static Analysis – Theoretical Background |
lecture08.pdf |
| 07.12.2011 |
Data-Flow Analysis |
lecture09.pdf |
| 21.12.2011 |
Static analysis of programs with heap and procedures |
lecture10.pdf |
| 04.01.2012 |
Current Trends |
lecture11.pdf |
| 11.01.2012 |
O. Šerý: Bounded Model Checking and Concolic Testing |
|
Labs
Annotation
Basic principles of automated program analysis and verification.
Model checking, theorem proving, and static analysis.
Syllabus
-
Model checking of programs
- Explicit-state model checking (JPF, Zing)
- Predicate abstraction and CEGAR (SLAM, SATABS, Blast)
-
Introduction to deductive methods in software verification and program analysis
- SAT solvers (PicoSAT)
- SMT solvers (Yices, Z3, CVC3)
- Theorem provers (Prover9, Isabelle)
-
Selected applications of deductive methods in software verification
-
Static code analysis
- Theoretical background: lattices, fixed points, control-flow graphs, ...
- Basic data-flow analysis
- Pointer analysis: points-to analysis, escape analysis, shape analysis, ...
- Control-flow analysis
-
Current trends in formal analysis and verification of programs (research and applications)
Lab
The purpose of the lab is to provide students with a hand-on experience with selected verification and analysis tools (
Java PathFinder,
Blast,
JML,
Spec#,
Soot,
...).
Homework assignments
There will be three assignments, each taking approximately 10-15 hours of homework. Solutions for all three of them have to be submitted 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.
Grading
Final grades will be determined by the quality of homework
and the result of the final exam in the following ratio:
- 50% Homework assignments (1-10 points for each of them)
- 50% Final exam (1-30 points)
Grades will be based on points in the following way:
| Grade | Required points |
|---|
| Excellent: | 49-60 points |
| Very good: | 40-48 points |
| Good: | 31-39 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
|
Home
People
Research
Projects
Publications
Teaching
Links
Contact