| Compiler Verification and Beyond: Verified Tools for High-Assurance Software |
|
| Verified Compiler Technology and Separation Logic for Reasoning about Concurrent C Programs |
|
| Towards High-Assurance Run-Time Systems |
|
| Using the Cambridge ARM Model to Verify the Concrete Machine Code of seL4 |
|
| Let's Build Secure Systems on a Correct Kernel |
|
| Developing Secure Mobile Architectures: The COTS Challenge |
|
| Applying Formal Methods to Prove Correctness of Surgical Robot Software |
|
| Verifying Timing-Centric Software Systems |
|
| Copilot: Cyber-Physical System Run-Time Verification |
|
| Making High-Confidence Systems Low-Cost |
|
| Dynamic Enforcement of Knowledge-Based Security Policies |
|
| Enforcing Information Flow Policies via Generation of Monitors in Java Card Runtime Environments |
|
| Guardol: A Domain-Specific Language for Guards Supporting Strong Automated Formal Analysis |
|
| Information Security: The Legacy of a Maginot Line in Cyberspace |
|
| Security Inception - Exploiting the Software Ecosystem |
|
| Matching Logic |
|
| Analysis-Based Verification: A Programmer-Oriented Approach to the Assurance of Mechanical Program Properties |
|
| Automatically Identifying Exploitable Bugs |
|
| CAS Static Analysis Tool Study Overview |
|
| The Open World Framework |
|
| Parametric Verification of Address Space Separation |
|
| Proposed Formal Methods Supplement for RTCA DO 178C |
|
| Moving-Target Defense With Configuration-Space Randomization |
|
| High Assurance Crypto-Development with Cryptol |
|
| Software Analysis Workbench (SAW) |
|