| Automatic Theorem Proving and SMT |
|
| Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties |
|
| Techniques for Scalable Symbolic Simulation |
|
| Cyber Defense Strategy |
|
| String Solvers for Web Security |
|
| Thwarting Themida: Unpacking Malware with SMT Solvers |
|
| Verified Software-Based Fault Isolation |
|
| Efficient and Verified Checking of Unsatisfiability Proofs |
|
| TrackOS: a Security-Aware RTOS |
|
| Applying Language-Based Static Verification in an ARM Operating System |
|
| Cache and IO-Efficient Functional Algorithms |
|
| Verification of Concurrent Software in the Context of Weak Memory |
|
| Verification of Concurrent Software in the Context of Weak Memory |
|
| Verification of X86 Binary-Level Programs |
|
| Access Control Policy Tool (ACPT), An Assurance Tool That Combines Symbolic Model Checking with Combinatorial Coverage |
|
| Secure Virtualization with Formal Methods |
|
| Verifying the Trusted Platform Module |
|
| Concurrency-Focused Dynamic Analysis |
|
| Security Analysis of LLVM Bitcode Files for Mobile |
|
| A Lazy SMT Bit-vector Solver for Binary Symbolic |
|
| Taming JavaScript with F* |
|
| Separation Logic Modulo Theories |
|
| Above and Beyond: seL4 Noninterference and Binary Verification (PT. 1) |
|
| Above and Beyond: seL4 Noninterference and Binary Verification (PT. 2) |
|
| 2002 HCSS Conference Proceedings |
|