Nadia Polikarpova

Introduction

This page is outdated. Check out my new homepage.

I have completed my PhD under the supervision of Prof. Bertrand Meyer at the Chair of Software Engineering, ETH Zurich. My thesis is about Specified and Verified Reusable Components. I received my Master degree in Applied Mathematics and Informatics in 2008 at Saint Petersburg State University of Information Technologies, Mechanics and Optics (St. Petersburg, Russia). I did my Master's thesis under the supervision of Ilinca Ciupa from ETH.

You can find more information in my curriculum vitae.

Research

My research interests lie in the area of software correctness, at the intersection of formal methods and software engineering. In particular, my research has contributed to auto-active verification, behavioral interface specifications, automated testing, dynamic invariant inference, and user interface for verification.

Here is the list of ongoing or completed projects I've been involved in:

• AutoProof: an auto-active program verifier for Eiffel. I'm working together with Julian Tschannen on a flexible methodology for framing and class invariants called Semantic Collaboration.
• Boogaloo: an interpreter and run-time assertion checker for Boogie [try online]
• EiffelBase2: specified and verified data structure library for Eiffel
• Traffic 4: the supporting software for Introduction to Programming that models and visualizes public transportation in a city
• Dynamic contract inference: CITADEL

Publications

2014

• Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, Bertrand Meyer: Flexible Invariants Through Semantic Collaboration FM'14: 19th International Symposium on Formal Methods, (Singapore), May 2014 [pdf] [supplementary material]

• Nadia Polikarpova: Specified and Verified Reusable Components PhD thesis, April 2014 [pdf]

2013

• Nadia Polikarpova, Carlo A. Furia, Scott West: To Run What No One Has Run Before RV'13: International Conference on Runtime Verification, (Rennes, France), September 2013 [pdf] [supplementary material]
• Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, Bertrand Meyer: What Good Are Strong Specifications? ICSE'13: International Conference on Software Engineering, (San Francisco, USA), May 2013 [pdf] [video] [supplementary material]
• K. Rustan M. Leino, Nadia Polikarpova: Verified Calculations VSTTE'13: Verified Software: Theories, Tools and Experiments, (Atherton, USA), May 2013 [pdf] [supplementary material]

2012

• Nadia Polikarpova, Michał Moskal: Verifying implementations of security protocols by refinement. VSTTE'12: Verified Software: Theories, Tools and Experiments, (Philadelphia, USA), January 2012 [pdf]

2011

• Vladimir Klebanov et. al.: The 1st Verified Software Competition: Experience Report FM'11: 17th International Symposium on Formal Methods, (Limerick, Ireland), June 2011 [pdf] best paper award

2010

• Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer: Specifying Reusable Components. VSTTE'10: Verified Software: Theories, Tools and Experiments, (Edinburgh, Scotland), August 2010 [pdf]

2009

• Nadia Polikarpova, Ilinca Ciupa, Bertrand Meyer: A comparative study of programmer-written and automatically inferred contracts. ISSTA'09: International Conference on Software Testing and Analysis, (Chicago, Illinois, USA), July 2009 [pdf]

Teaching

• Spring 2014: teaching assistant for Java and C# in depth (Dr. Carlo A. Furia, Dr. Marco Piccioni, Prof. Bertrand Meyer)
• Fall 2013: teaching assistant for Introduction to Programming (Prof. Bertrand Meyer)
• Fall 2012: teaching assistant for Introduction to Programming (Prof. Bertrand Meyer)
• Fall 2011: teaching assistant for Introduction to Programming (Prof. Bertrand Meyer)
• Fall 2010: teaching assistant for Introduction to Programming (Prof. Bertrand Meyer)
• Spring 2010: teaching assistant for Java and C# in depth (Prof. Bertrand Meyer, Dr. Carlo A. Furia)
• Fall 2009: head assistant for Introduction to Programming (Prof. Bertrand Meyer)
• Spring 2009: teaching assistant for Software Architecture (Prof. Bertrand Meyer)
• Fall 2008: teaching assistant Introduction to Programming (Prof. Bertrand Meyer)