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*
|
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 |
|
|
|
|
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 |
|
|
|
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 |
|
||
1530-1600 |
|
|
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 |