Presentation

Abstract:

Abstract:

Modern software systems are ubiquitous and complex, often running on critical platforms ranging from human implant devices to nuclear power plant controls. How can we be sure that these programs will behave as intended? Programmers must first specify the correct behavior of their programs, and one widely accepted specification language is temporal logic. Despite decades of research in finite-state contexts and some adaptations of finite-state algorithms, we still lack scalable tools for proving temporal logic properties of software.

Abstract:

Cryptography is essential for ensuring that sensitive information can be securely stored and transmitted without risk of tampering or disclosure to untrusted parties. Although typically only a very small part of an overall system, cryptographic implementations are often highly complex due to a variety of performance optimizations, and may have many edge cases or diffcult to understand implementation tricks.

Abstract:

I will describe a new approach to the old problem of automatic temporal property verification. As well as leading to dramatic performance improvements over existing techniques, this approach also brings some light to a couple of age-old questions.

Biography:

Abstract: