Interactive theorem proving and software verification

access_time December 05, 2018 at 01:30PM until December 05, 2018 at 02:30PM
place IST Alameda - Room 0.19 (Informática II building) and IST TagusPark - Room 2N1.5 (through videoconference)


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  

Biography: 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.