Program Analysis and Code Verification

Time and Location: Summer Term 2017/2018
Lecture: Mon 14:00 S7
Lab: Mon 15:40 SW1
Guaranteed by: Department of Distributed and Dependable Systems
Summer Term: 2/2 Zk+Z
Lecturers: Pavel Parízek
e-mail: parizek<at-sign>d3s.mff.cuni.cz
Labs: Pavel Parízek
e-mail: parizek<at-sign>d3s.mff.cuni.cz
Information in SIS: NSWI132

News

  • The third homework assignment is available here. The deadline for submitting your complete solutions is on May 25th, 2018 at 23:59.
  • The fourth homework assignment is available here. The deadline for submitting your complete solutions is on June 30th, 2018 at 23:59.
  • The fifth homework assignment is available here.

Slides

Lectures

DateTopicSlides
19.2.2018Introductory lecturelecture00.pdf
26.2.2018Model Checking Programslecture01.pdf
5.3.2018Concurrency Errorslecture02.pdf
12.3.2018Symbolic Execution, Dynamic Analysislecture03.pdf
19.3.2018Deductive Methods, Bounded Model Checkinglecture04.pdf
26.3.2018Abstractionlecture05.pdf
9.4.2018Contracts: Specification and Verificationlecture06.pdf
16.4.2018Static Analysis: Overview, Data-Flowlecture07.pdf
23.4.2018Static Analysis: Pointers and Heap Structureslecture08.pdf
30.4.2018Abstract Interpretationlecture09.pdf
21.5.2018Combining Verification Approacheslecture10.pdf
21.5.2018Program Terminationlecture11.pdf
21.5.2018Program Synthesislecture12.pdf

Labs

DateTopicSlidesExamples
26.2.2018Java PathFinderlab01.pdf
5.3.2018Detecting Concurrency Errors with JPFlab02.pdfconcur_bench.zip
12.3.2018Symbolic PathFinder, Pex, RoadRunnerlab03.pdf
19.3.2018SMT Solvers, CBMClab04.pdfsmt-examples.zip | bmc-examples.zip
26.3.2018CEGARlab05.pdfcegar.tgz
9.4.2018Code Contractslab06.pdfcontracts-examples.zip
16.4.2018T.J. Watson Libraries for Analysislab07.pdfwala-examples.zip
23.4.2018Static Analysis Toolslab08.pdfpredator-examples.tgz
30.4.2018Realistic Verification Scenarioslab09.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, Code Contracts, 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.

DeadlineTopicSlidesExamples
9.4.2018 23:59Java Pathfinderhw1-jpf.pdfdaisyfs.zip | elevator.zip | repworkers.zip
7.5.2018 23:59Code Contractshw2-contracts.pdf
25.5.2018 23:59Static Analysishw3-static.pdf
30.6.2018 23:59Finding Bugs in Real Softwarehw4-realsw.pdf
21.5.2018Research Papershw5-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:lectureslabstools & examples
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>d3s.mff.cuni.cz
  •  
  • How to find us?
Modified on 2018-02-09