2013 HCSS Conference Program Agenda

 

2013 DAILY AGENDA

  TUESDAY, MAY 7 
JavaScript
WEDNESDAY, MAY 8 
SMT
THURSDAY, MAY 9 
The Boundary Between Hardware and Software
FRIDAY, MAY 10 
Design-In Security
0900-0930

Keynote Presentation:    Taming JavaScript with F* 
Nikhil Swamy, Microsoft Research

 

Keynote Presentation: Automatic Theorem Proving and SMT 
Nikolaj Bjørner, Microsoft Research
Keynote Presentation:   Verified Software Fault Isolation 
Greg Morrisett, Harvard University
Access Control Policy Tool (ACPT), An Assurance Tool That Combines Symbolic Model Checking with Combinatorial Coverage 
Vincent Hu, National Institute of Standards and Technology
0930-1000 Verifying the Trusted Processor Module 
Perry Alexander, The University of Kansas
1000-1030 Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection 
Jan Vitek, Purdue
From SMT Solvers to Verifiers 
Aws Albarghouthi, University of Toronto
Efficient and Verified Checking of Unsatisfiability Proofs 
Marijn Heule, The University of Texas at Austin
Secure Virtualization With Formal Methods 
Cynthia Sturton, UC Berkeley
1030-1100


BREAK / Poster Session
 


BREAK 
 


BREAK 
 


BREAK 
 

1100-1130 Protecting Sensitive Data in Web Browsers with ScriptPolice 
Brad Karp, University College London
Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties 
Konrad Slind, Rockwell Collins
TrackOS: A Security-Aware RTOS 
Lee Pike, Galois
Tutorial: Nikolaj Bjørner, Microsoft Research
1130-1200 Dependent Types for JavaScript 
Ravi Chugh, UC San Diego
Techniques for Scalable Symbolic Simulation 
Aaron Tomb, Galois
Above and Beyond: SeL4 Noninterference and Binary Verification (PT. 1, PT.2
Toby Murray and Thomas Sewell, UNSW and NICTA
1200-1230 JSCert: Certifying JavaScript 
Philippa Gardner, Imperial College London
A Lazy SMT Bit-vector Solver for Binary Symbolic Execution 
Clark Barrett, New York University
Applying Language-Based Static Verification in an ARM Operating Systems 
Matthew Danish
1230-1400


LUNCH 
 


LUNCH 
 


LUNCH 
 

Conference Adjourned
1400-1430 Keynote Presentation: What We're Not Working On Susan Alexander, IARPA Keynote Presentation: Cyber Defense Strategy 
Dan Kaufman, DARPA
Keynote Presentation: Enterprise Level Malware Analysis Initiatives 
Joseph C. Opacki, FBI
1430-1500 Keynote Presentation: A Family of Certification Methods for JavaScript and Its Environments 
Shriram Krishnamurthi, Brown University
Cache and IO-Efficient Functional Algorithms 
Robert Harper, Carnegie Mellon University
1500-1530 String Solvers for Web Security 
Vijay Ganesh, University of Waterloo


BREAK 
 

1530-1600


BREAK 
 


BREAK 
 

Verification of Concurrent Software in the Context of Weak Memory 
Jade Alglave, University College London
1600-1630 You Can't Touch This: Dynamic Access Control for JavaScript 
Peter Thiemann, University of Freiburg - Germany
Thwarting Themida: Unpacking Malware with SMT Solvers 
Ian Blumenfeld, CyberPoint
Weak Memory and the Perils of ARM: Using Dynamic Analysis to Probe Concurrency Issues for Safe/Secure Mobiles Applications 
Timothy Halloran, SureLogic
1630-1700 Security Analysis of LLVM Bitcode Files for Mobile Platforms 
Vivek Sarkar, Rice University
Separation Logic Modulo Theories 
Juan Antonio Navarro Perez, University College London
Formal Specification of the X86 ISA 
Warren Hunt, The University of Texas at Austin
1700

Adjourn for the day

 

Adjourn for the day

 

Adjourn for the day

 

1830 Conference Dinner 

The Chart House 
300 2nd Street 
Annapolis, MD 21403