USI - Email

Archive / INF Seminars / INF_2020_03_02_Stulova

USI - Email

	Contracts and comments in program verification

Host: Prof. Mauro Pezzè

Monday

02.03

USI Lugano Campus, room SI-004, Informatics building

15:30 - 16:30


	Nataliia Stulova EPFL, Switzerland

Abstract:
In this talk I will present techniques and tools for program analysis that leverage formal and informal program specifications such as assertions, contracts, and English text source code comments.

In the first part of this talk I will present my work on assertion-based run-time program verification techniques within the framework of the Ciao system. I will demonstrate an approach for specification language extension with higher-order syntax that allows for automatic first-order assertion generation.
I will also present techniques for efficient source code instrumentation with run-time checks generated from assertion-based specifications. For this purpose I will show how static analysis and run-time checking can be combined to simultaneously increase the precision of the former and improve the performance of the latter. I will also present results for run-time overhead reduction for instrumented programs and initial work on automated check cost estimation.

In the second part of the talk I will present my ongoing work on linking program comments and source code. Expected use cases include automatic structured source code summary generation, and detecting code-comment inconsistencies.

Biography:
Nataliia Stulova is a postdoctoral researcher at the Lab for Automated Reasoning and Analysis at École Polytechnique Fédérale de Lausanne (EPFL), Switzerland, working with Viktor Kuncak. Her research interests include applications of natural language processing techniques to the tasks of source code summarization and documentation analysis. She obtained her PhD from IMDEA Software Institute of Madrid, Spain, working on optimization techniques for specification-based program verification with Manuel Hermenegildo and Jose F. Morales. Before that she obtained a Master of Sciences degree in Artificial Intelligence from the Technical University of Madrid (UPM), Spain, and a Bachelor of Sciences degree in Applied System Analysis from the National Technical University of Ukraine "Igor Sikorsky Kyiv Polytechnic Institute".