BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Software Correctness at Scale through Testing and V
 erification
DTSTART:20200309T101500
DTEND:20200309T111500
DTSTAMP:20260406T144424Z
UID:187840d1c9d891a2b54e5a2440612c8e97dcdd139760cafde61f4e88
CATEGORIES:Conferences - Seminars
DESCRIPTION:Par: Leonidas Lampropoulos - University of Maryland - Universi
 ty of Pennsylvania\nIC Faculty candidate\n\nAbstract:\nSoftware correctnes
 s is becoming an increasingly important concern as our society grows more
  and more reliant on computer systems. Even the simplest of software error
 s can have devastating financial or security consequences. How can we find
  errors in real-world applications?  How can we guarantee that such error
 s don't exist?  To even begin to answer these questions we need a specif
 ication: a description of what it means for a piece of code to be correct\
 , stated either explicitly (e.g. my private data are never leaked to third
  parties) or implicitly (e.g. this code will not terminate with an uncaugh
 t exception).\nIn this talk\, I will discuss efficient ways to debug and r
 eason about software and specifications\, focusing on two techniques and t
 heir interplay: property-based testing and mechanized formal verificati
 on. Testing can quickly uncover errors in complex software\, but it cannot
  guarantee their absence.  Formal verification provides strong correctnes
 s guarantees\, but is still very expensive in time and effort.  \nTogeth
 er\, they are a match made in heaven.\n\nBio:\nLeonidas Lampropoulos is a 
 Victor Basili postdoctoral fellow jointly between UMD and UPenn\, under th
 e supervision of Prof. Michael Hicks and Prof. Benjamin Pierce. Before tha
 t\, he got his Ph.D. at the University of Pennsylvania\, advised by Prof. 
 Pierce. His research interests lie in programming languages\, with an emph
 asis on software correctness through both random testing and mechanized ve
 rification. He is the principal author of the fourth volume in the popular
  Software Foundations series of online textbooks: "QuickChick: Property-Ba
 sed Testing in Coq".\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR