BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Practical Software Verification
DTSTART:20190214T130000
DTEND:20190214T150000
DTSTAMP:20260407T195402Z
UID:8207baf99ff7fa0416011044e889283dd697d5879f29f364e5ec9607
CATEGORIES:Conferences - Seminars
DESCRIPTION:Solal Pirelli\nEDIC candidacy exam\nExam president: Prof. Jame
 s Larus\nThesis advisor: Prof. George Candea\nCo-examiner: Prof. Viktor Ku
 ncak\n\nAbstract\nProgram verification is one of the main tools for buildi
 ng more dependable software. However\, verification often cannot scale to 
 the large programs in use today. This can be because the required human ef
 fort is too large\, as in theorem provers\, or because there are too many 
 program states to consider individually\, as in symbolic execution. This r
 eport 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 symbo
 lic execution\; and seL4\, an example of a real-world verified operating s
 ystem.\n\nBackground papers\nKLEE: Unassisted and Automatic Generation of 
 High-Coverage Tests for Complex Systems Programs\, by Cadar\, C.\, et al.\
 nMultiSE: Multi-Path Symbolic Execution using Value Summaries\, by Sen\, K
 .\, et al.\nseL4: Formal Verification of an OS Kernel\, by Klein\, G.\, e
 t al.\n\n 
LOCATION:INN 326 https://plan.epfl.ch/?room=INN326
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR