HCSS 2021

file

Visible to the public DoD Enterprise DevSecOps Initiative & Platform One

ABSTRACT

file

Visible to the public Verifiable Binary Lifting

ABSTRACT

file

Visible to the public Safe Composition through Dynamic Feature Interaction Resolution

ABSTRACT

file

Visible to the public Proof Robustness in the seL4 Verification

ABSTRACT

file

Visible to the public Retrofitting a type system onto a real world dynamic expression language

ABSTRACT

Customers use AWS IoT Events to monitor their equipment for failures. To do so, they create an event detector, modeled as a state machine, in AWS IoT Events to trigger actions when such failures occur. The state machine consists of states and transitions predicated on conditions written in the IoT Events expression language. Each state machine takes an input value sent by a customer’s IoT device, substitutes input values in its expressions, evaluates them, and triggers other AWS services as its output. 

file

Visible to the public Proof Robustness in ACL2

ABSTRACT

This experience report builds on 20 years of maintaining proofs for the ACL2 theorem prover.

file

Visible to the public On Computing Relevant Parameters of Decision Functions

ABSTRACT

file

Visible to the public KEYNOTE: Robustness of formal verification of x86 microprocessors

ABSTRACT