2013 HCSS Conference Program Agenda
DOWNLOAD PRINTER-FRIENDLY VERSION | DOWNLOAD PROCEEDINGS BOOKLET
2013 DAILY AGENDA
TUESDAY, MAY 7 |
WEDNESDAY, MAY 8 |
THURSDAY, MAY 9 |
FRIDAY, MAY 10 |
|
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 |
0930-1000 |
Verifying the Trusted Processor Module |
|||
1000-1030 |
Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection |
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 |
BREAK |
BREAK |
BREAK |
1100-1130 |
Protecting Sensitive Data in Web Browsers with ScriptPolice |
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) |
|
1200-1230 | JSCert: Certifying JavaScript Philippa Gardner, Imperial College London |
A Lazy SMT Bit-vector Solver for Binary Symbolic Execution |
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 |
Keynote Presentation: Enterprise Level Malware Analysis Initiatives |
|
1430-1500 | Keynote Presentation: A Family of Certification Methods for JavaScript and Its Environments Shriram Krishnamurthi, Brown University |
Cache and IO-Efficient Functional Algorithms |
||
1500-1530 |
String Solvers for Web Security |
BREAK |
||
1530-1600 |
BREAK |
BREAK |
Verification of Concurrent Software in the Context of Weak Memory |
|
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 |
|
1630-1700 |
Security Analysis of LLVM Bitcode Files for Mobile Platforms |
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 |