263-2910-00L Automated Techniques for Software Reliability
Semester | Autumn Semester 2012 |
Lecturers | M. Vechev |
Periodicity | yearly recurring course |
Language of instruction | English |
Courses
Number | Title | Hours | Lecturers | ||||
---|---|---|---|---|---|---|---|
263-2910-00 V | Automated Techniques for Software Reliability | 2 hrs |
| M. Vechev | |||
263-2910-00 U | Automated Techniques for Software Reliability | 1 hrs |
| M. Vechev |
Catalogue data
Abstract | This course introduces both theoretical and applied aspects of automatic program analysis. We will cover both: i) Core principles underlying automated analysis. ii) Applications of these techniques to solve challenging practical problems (e.g. in security, reliability, synthesis). |
Objective | The course has 3 main objectives: - Understand the foundational principles behind automated program analysis techniques. - Understand how to use these principles to build a practical working analyzer. This will be helped by a hands-on programming project. - Gain familiarity with the state-of-the-art in the research area. |
Content | The last 10 years have seen an explosion in techniques for automated program analysis. These techniques have enabled a vast range of interesting applications: from ensuring correctness of complex algorithms to finding security violations in mobile applications and even to code synthesis. This course will cover the core principles behind these automated techniques including static and dynamic program analysis, symbolic execution, predicate abstraction, pointer analysis as well as practical analysis frameworks such as Soot. To gain a deeper understanding of how to apply these techniques in practice, the course will involve a small hands-on programming project where based on the principles introduced in class, the students will build a program analyzer for a modern programming language. Topics Include (we will cover only some of these): program semantics: small-step, big-step, concurrency, usage examples dynamic analysis: typestate, race detection abstract interpretation: domains, soundness, precision, fixed points, applications predicate abstraction: classic (Graf-Saidi), boolean programs (SLAM for C code) pointer analysis: flow-insensitive symbolic execution: SMT solvers, concolic, tools (CUTE/DART/KLEE) program synthesis: synthesis of concurrent programs, combining with abstractions inter-procedural analysis: two approaches: Pnueli, Reps. program analysis frameworks: Wala, Soot, LLVM |
Lecture notes | Distributed in class. |
Literature | Distributed in class. |
Prerequisites / Notice | This course is aimed at graduate students, but advanced bachelor students can sign up with lecturer's permission. |
Performance assessment
Performance assessment information (valid until the course unit is held again) | |
Performance assessment as a semester course | |
ECTS credits | 4 credits |
Examiners | M. Vechev |
Type | session examination |
Language of examination | English |
Repetition | The performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling. |
Mode of examination | oral 20 minutes |
Additional information on mode of examination | The grade will be determined by the semester-long project (30%) and final exam (70%). |
This information can be updated until the beginning of the semester; information on the examination timetable is binding. |
Learning materials
Main link | Information |
Only public learning materials are listed. |
Groups
No information on groups available. |
Restrictions
There are no additional restrictions for the registration. |
Offered in
Programme | Section | Type | |
---|---|---|---|
Computer Science Master | Focus Elective Courses Software Engineering | W | |
Certificate of Advanced Studies in Computer Science | Focus Courses and Electives | W |