Verification Challenges in Dynamic Programming Languages

By Nataliia Stulova

Abstract
Software verification comes in two flavors: static and dynamic. Static program verification takes place during program analysis and/or compilation, and it aims to prove the correctness of the program w.r.t. some criteria. Dynamic one takes place at run time and it's purpose is to detect undesirable program behaviors. It also helpful in scenarios where static analysis is imprecise or when the code is loaded /updated dynamically. Nowadays these two tasks are typically addresses by systems that offer programmers a combination of language-level constructs (procedure-level annotations such as assertions/contracts, gradual/refinement types, etc.) and associated tools (such as static code analyzers and run-time verification frameworks). However, it is often 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-time overhead and/or limited expressiveness.
This issue is especially prominent in the context of dynamic languages without an underlying strong type system.

In this talk I will introduce several practical solutions for minimizing the run-time overhead associated with assertion-based verification while keeping the correctness guarantees provided by run-time checks. The solutions will be presented in the context of the Ciao system (developed at IMDEA Software). Ciao is a Prolog-based multi-paradigm language where also a compiler, an abstract interpretation-based static analyzer and run-time verification framework are available.

Bio
Nataliia Stulova is a recent PhD graduate from IMDEA Software Institute of Madrid, Spain. 
In an effort to make software more reliable without compromising its
performance, she explores optimization possibilities for specification-based program verification, both in the direction of designing expressive specification languages and in the direction of generating efficient run-time checks from them. 
Before 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 Kyiv Polytechnic Institute ".

More information