Program Agenda

Visible to the public 

Download zipped folder containing conference presentations, posters, and proceedings booklet.

  Tuesday, May 5
Proof Engineering
Wednesday, May 6
Sustainable Integrity
Thursday, May 7
0900 - 1000

Keynote Presentation:
Proof Engineering: The Soft Side of Hard Proof

Gerwin Klein (NICTA)


Keynote Presentation:
Detecting Malice in Commodity Software

Tim Fraser (DARPA)


Keynote Presentation:
Building Privacy-Aware Computing Systems: An Overview of Current Capabilities and Technical Challenges

Shantanu Rane (PARC)


1000 - 1030 Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11
Kayvan Memarian
(University of Cambridge)
Remote Attestation for Cloud-Based Systems
Perry Alexander
(University of Kansas)
Reconciling Provable Security and Practical Cryptography: A Programming Language Perspective
Gilles Barth (IMDEA)
1030 - 1100 Break Break POSTER SESSION
1100 - 1115 Verifiable C: proving functional correctness of C programs in Coq, e.g. SHA-256 and HMAC
Andrew Appel (Princeton)
Software Defenses Inspired by Biodiversity
Michael Franz (UC Irvine)
1115 - 1130 A Cut Principle for Information Flow
Joshua Guttman
(The MITRE Corporation and WPI)
1130 - 1145 Deep Specifications and Certified Abstraction Layers
Ronghui Gu (Yale)
Not-quite-so-broken TLS: Lessons in Re-engineering a Security Protocol Specification and Implementation
David Kaloper Mersinjak
(Univ. of Cambridge)
1145 - 1200 Models and Games for Quantifying Vulnerability of Secret Information
Piotr Mardziel (University of MD)
1200 - 1215 Lunch (on your own) Lunch (on your own)
1215 - 1330 Lunch (on your own)
1330 - 1345 Qualification of Formal Methods Tools
Darren Cofer (Rockwell Collins)
Rigorous Architectural Modelling for Production Multiprocessors
Shaked Flur, Kathryn Gray, Christopher Pulte
(University of Cambridge)
1345 - 1400 NSA Civil Liberties & Privacy: Bridging the Art and Science of Privacy
Rebecca Richards (NSA)
1400 - 1430 Issues, Challenges and Opportunities in the Qualification of Formal Method Tools
Cesare Tinelli (University of Iowa)
A Formal Specification of x86 Memory Management
Shilpi Goel and Warren Hunt
(UT Austin)
1430 - 1500 Break Language-based Hardware Verification with ReWire: Just Say No! to Semantic Archaeology
William Harrison
(University of Missouri)
High Assurance Cryptography Synthesis with Cryptol
Joseph Kiniry (Galois)
1500 - 1530 Multi-Language and Multi-Prover Verification with SAWScript
Aaron Tomb (Galois)
1530 - 1545 CodeHawk: Sound Static Analysis for Proving the Absence of Memory Related Software Vulnerabilities
Douglas Smith (Kestrel Technology)
Achieving High Speed and High Assurance in a Hardware-Based Cross-Domain System Using Guardol
David Hardin (Rockwell Collins)
1545 - 1600 Privacy through Accountability
Anupam Datta
(Carnegie Mellon University)
1600 - 1630 Adjourn for the day Bringing Hardware Hacking to Life
Colin O'Flynn (Dalhousie University)
1630 - 1700 Adjourn for the day Private Disclosure of Information
Daniel Aranki (UC Berkeley)
1830 Conference Dinner
The Chart House
300 2nd Street
Annapolis, MD 21401
Conference adjourned

Conference Archives: 20012002200320042005200620072008200920102011201220132014