Interfaces for Formal Methods

I am interested in innovative interfaces, tools, and methods that make interactive theorem proving technology and software verification more accessible to non-experts. My previous work includes tool support for handwritten calculational proofs using tablet pcs. My current efforts are on formally verifying handwritten proofs without the need to learn the specific syntax and intricacies of interactive theorem provers. See papers below.

Avatar
Alexandra Mendes
Assistant Professor

My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Recently, I started work on usable security, in particular on the impact of formal verification on the use and adoption of formally verified security software products. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn.