TACL Seminar Spring '05

From CSWiki
Revision as of 15:29, 15 August 2006 by Ddantas (talk | contribs) (Dan Wang)

Jump to: navigation, search

TACL Seminar

Schedule

Date Speaker Title Links
Feb 9 Dan Wang Opportunities and Challenges in End-to-End Verification of Software Systems Abstract
Feb 10 Dinghao Wu Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code Abstract
Feb 16 Gang Tan Structured Verification of Unstructured Machine Code Abstract
Feb 23 NJ PLS
Mar 2 Xinming Ou MulVAL: An Automatic Network Vulnerability Analyzer Abstract
Mar 9 George Reis SWIFT: Software Implemented Fault Tolerance Abstract
Mar 16 Bolei Guo Low-Level Pointer Analysis Abstract
Mar 23 Dominic Duggan - Stevens
Mar 28 Neal Glew - Intel Research Inlining, Dynamic Loading and Type Safety Abstract
Apr 6 Neil Vachharajani Opportunities for Coarse-Grained Parallel Execution Abstract
Apr 13 Yitzhak Mandelbaum A Calculus for Specifying Ad Hoc Data Formats Abstract
Apr 22 IBM PL Day
Apr 27 Rob Simmons Metatheoretic Approaches to Formalizing High-level Languages Abstract
May 25 Aarti Gupta - NEC Verifying C Programs by Model Checking Abstract

Abstracts

Dan Wang

Opportunities and Challenges in End-to-End Verification of Software Systems

I'll start out by taking a brief tour that covers my past experience on various projects and how those experiences shape my current view of the importance and practicality of end-to-end system verification. My basic thesis is that end-to-end system verification is theoretically/technically possible, but often *economically* impractical. More importantly the marketplace for verified software systems is likely to significantly expand within this century.

I'll will also discuss on going research in developing simpler and flexible semantic techniques for the verification of Foundational Proof-Carrying code systems. In particular, I will discuss how to build proofs of type soundness using higher-order abstract encodings of syntax without the need for meta-logical approaches to soundness.

Dinghao Wu

Gang Tan

Xinming Ou

George Reis

Bolei Guo

Neal Glew

Neil Vachharajani

Yitzhak Mandelbaum

Rob Simmons

Aarti Gupta


TACL Seminar