BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Verification Challenges in Dynamic Programming Languages
DTSTART:20180829T110000
DTEND:20180829T120000
DTSTAMP:20260407T015958Z
UID:f26ec56e6a6f294cfe5ece8e89fae76d11ed2686246c90f4f25d980e
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Nataliia Stulova\n\nAbstract\nSoftware verification comes i
 n two flavors: static and dynamic. Static program verification takes plac
 e during program analysis and/or compilation\, and it aims to prove the c
 orrectness of the program w.r.t. some criteria. Dynamic one takes place a
 t run time and it's purpose is to detect undesirable program behaviors. I
 t also helpful in scenarios where static analysis is imprecise or when the
  code is loaded /updated dynamically. Nowadays these two tasks are typica
 lly addresses by systems that offer programmers a combination of language
 -level constructs (procedure-level annotations such as assertions/contrac
 ts\, gradual/refinement types\, etc.) and associated tools (such as stati
 c code analyzers and run-time verification frameworks). However\, it is o
 ften the case that these constructs and tools are not used to their full 
 extent in practice due to a number of limitations such as excessive run-t
 ime overhead and/or limited expressiveness.\nThis issue is especially prom
 inent in the context of dynamic languages without an underlying strong ty
 pe system.\n\nIn this talk I will introduce several practical solutions fo
 r minimizing the run-time overhead associated with assertion-based verifi
 cation while keeping the correctness guarantees provided by run-time chec
 ks. The solutions will be presented in the context of the Ciao system (de
 veloped at IMDEA Software). Ciao is a Prolog-based multi-paradigm languag
 e where also a compiler\, an abstract interpretation-based static analyze
 r and run-time verification framework are available.\n\nBio\nNataliia Stu
 lova is a recent PhD graduate from IMDEA Software Institute of Madrid\, S
 pain. \nIn an effort to make software more reliable without compromising 
 its\nperformance\, she explores optimization possibilities for specificati
 on-based program verification\, both in the direction of designing expres
 sive specification languages and in the direction of generating efficient
  run-time checks from them. \nBefore graduate school she was a Master's 
 student at the Technical University of Madrid\, Spain\, and a Bachelor's 
 student at the National Technical University of Ukraine "Igor Sikorsky Ky
 iv Polytechnic Institute ".\n\nMore information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR