BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Formal Verification of Concurrent Software
DTSTART:20220825T133000
DTEND:20220825T153000
DTSTAMP:20260501T063211Z
UID:bf88571553a395cdb0065a031dec9d4a61fd584249feea15401d7188
CATEGORIES:Conferences - Seminars
DESCRIPTION:Yugesh Kothari\nEDIC candidacy exam\nExam president: Prof. Mar
 tin Odersky\nThesis advisor: Prof. Sanidhya Kashyap\nCo-examiner: Prof.Geo
 rge Candea\n\nAbstract\nConcurrency is hard. Writing high performance\nsaf
 e concurrent code is challenging even for seasoned developers.\nMoreover\,
  high performance applications are increasingly trying\nto leverage kernel
  customization (via eBPF or kernel modules)\nto juice out performance for 
 specific target workloads. Such a\ncustomisable surface increases chances 
 for specification violations\nboth in terms of safety and liveness. In thi
 s thesis\, I motivate these\npoints and make a case for developing techniq
 ues for verifying\nliveness of concurrent software.\n\n\nBackground papers
 \n\n	Armada: Low-Effort Verification of High-Performance Concurrent Progra
 ms\n	High performance locks for multi-level NUMA systems\n	Application-Inf
 ormed Kernel Synchronization Primitives.\n
LOCATION:BC 329 https://plan.epfl.ch/?room==BC%20329
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR