Valuable Verification: Theorems that Pay

Speaker: Jay McCarthy , Brigham Young University

Date: Thursday, March 06, 2014

Time: 11:00 AM to 12:00 PM Note: all times are in the Eastern Time Zone

Public: Yes

Location: 34-401A

Event Type:

Room Description:

Host: Luca Daniel, MIT EECS

Contact: Adam Chlipala,

Relevant URL:

Speaker URL: None

Speaker Photo:

Reminders to:,

Reminder Subject: TALK: Valuable Verification: Theorems that Pay

Most programmers associate formal verification and mechanical theorem
proving with formalizing mathematics, high assurance software (such as
aerospace control systems), and hardware checking, but not their own work.
Yet, recently these approaches have found success in more commonplace
applications such as C compilers and relational databases. We attribute
this expansion to a greater appreciation of reliable software and a
decrease in the cost of verification.

In this talk, I will describe my own forays into this area with an
emphasis on how formal verification creates practical benefits that would
not have been available if not for the reliability of the theorems. I have
selected a diverse set of applications for this presentation:

- how traditional network services, like load-balancers, must adapt to
handle the unique constraints of cryptographic protocols;

- how simple probabilistic relationships need a foundation in complex
measure theory to understand and automate;

- how modern APIs assume users obey temporal orderings in their uses which
need a new kind of monitoring system to enforce at runtime.

Finally, I will close with a sketch of further ways that this
application of programming language and verification research can improve
software quality and programmer quality of life.

Web site:

Research Areas:

Impact Areas:

This event is not part of a series.

Created by Adam Chlipala Email at Monday, March 03, 2014 at 3:17 PM.