Interactive theorem proving and software verification

access_time 05 de dezembro de 2018 às 13:30 até 05 de dezembro de 2018 às 14:30
place IST Alameda - Room 0.19 (Informática II building) and IST TagusPark - Room 2N1.5 (through videoconference)

Image

Successes in the formal verification of sizeable programs, such as the CompCert C compiler, the seL4 microkernel, and the verified implementation of OpenSSL HMAC, show the growing importance of interactive theorem provers (ITPs) such as Coq and Isabelle/HOL. However, verification using ITPs continues to be an expert’s job. In this talk I will present my work on tools and methods that aim to make interactive theorem proving technology and software verification more accessible to non-experts. I will talk about my work on structure editing of handwritten mathematics and the initial steps towards a system that can formally verify handwritten calculational proofs without the need to learn the specific syntax and intricacies of ITPs.

face  Speaker: Prof. Alexandra Mendes  

Biografia: Alexandra holds a degree in Mathematics and Computer Science from Universidade do Minho and received her PhD in Computer Science from the University of Nottingham (UK) in 2012. She was appointed as a Lecturer in Computer Science at York St John University (UK) in 2013 and moved to Teesside University (UK) in early 2015 to become a Senior Lecturer. From January 2019 she will join Universidade da Beira Interior as an Assistant Professor. Her research focuses on innovative user interfaces for formal methods and mathematical approaches to software quality. Through her research work she aims at encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software.