HCSS'13

file

Visible to the public Above and Beyond: seL4 Noninterference and Binary Verification (PT. 1)

Submitted by TimTh on Tue, 05/28/2013 - 1:12pm. Contributors:

ABSTRACT:

In 2009, the L4.verified project completed the world's first verification of functional correctness for a general-purpose OS kernel [2], seL4. Functional correctness here was embodied by a formal theorem of refinement, which stated that the behavior of the C code that implemented the kernel accorded with an abstract specification of how the kernel was meant to function.

file

Visible to the public Separation Logic Modulo Theories

Submitted by TimTh on Tue, 05/28/2013 - 12:51pm. Contributor:

Presented as part of the 2013 HCSS conference.

ABSTRACT:

file

Visible to the public Taming JavaScript with F*

Submitted by TimTh on Tue, 05/28/2013 - 12:47pm. Contributor:

Presented as part of the 2013 HCSS conference.

ABSTRACT: