Practical Software Verification
Event details
| Date | 14.02.2019 |
| Hour | 13:00 › 15:00 |
| Speaker | Solal Pirelli |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. James Larus
Thesis advisor: Prof. George Candea
Co-examiner: Prof. Viktor Kuncak
Abstract
Program verification is one of the main tools for building more dependable software. However, verification often cannot scale to the large programs in use today. This can be because the required human effort is too large, as in theorem provers, or because there are too many program states to consider individually, as in symbolic execution. This report discusses recent efforts and results in verification. To this extent, this report presents KLEE, one of the main symbolic execution engines for real-world code; MultiSE, a technique to improve the design of symbolic execution; and seL4, an example of a real-world verified operating system.
Background papers
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, by Cadar, C., et al.
MultiSE: Multi-Path Symbolic Execution using Value Summaries, by Sen, K., et al.
seL4: Formal Verification of an OS Kernel, by Klein, G., et al.
Exam president: Prof. James Larus
Thesis advisor: Prof. George Candea
Co-examiner: Prof. Viktor Kuncak
Abstract
Program verification is one of the main tools for building more dependable software. However, verification often cannot scale to the large programs in use today. This can be because the required human effort is too large, as in theorem provers, or because there are too many program states to consider individually, as in symbolic execution. This report discusses recent efforts and results in verification. To this extent, this report presents KLEE, one of the main symbolic execution engines for real-world code; MultiSE, a technique to improve the design of symbolic execution; and seL4, an example of a real-world verified operating system.
Background papers
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, by Cadar, C., et al.
MultiSE: Multi-Path Symbolic Execution using Value Summaries, by Sen, K., et al.
seL4: Formal Verification of an OS Kernel, by Klein, G., et al.
Practical information
- General public
- Free