!!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!! !!!
-------------------------------------------------------------------------------
                                       
                                       
                   B O S T O N   U N I V E R S I T Y
                                       
                      Computer Science Department
                                       
                          C O L L O Q U I U M

        Towards Automated Verification of Safety Architectures

                           Carsten Schurmann 
			   
		      Computer Science Department
                       Carnegie Mellon University 


   			   Friday,  April 28 
			       11:00 AM 
                       (Coffee served at 10:45AM)

                                       
                         Seminar Room / MCS 135


    It is very unlikely that software will ever be proven totally correct,
    safe, and secure.  For example, in order to trust that the execution
    of a binary is memory safe, we have to trust the correctness of the
    compiler implementation.  But in general, we can neither expect any
    real compiler to be free of bugs nor can we expect to prove its
    implementation correct.  On the other hand, when compiled code is
    augmented with safety proofs, the execution of the binary will be
    safe; in this case instead of trusting the compiler we must trust the
    safety architecture (e.g. proof-carrying code or typed assembly
    language) which is typically based on logics or type systems.

    In my talk I will present a meta-logical framework and its
    implementation in the Twelf system.  Twelf is a tool that supports the
    design of deductive systems in general and safety architectures in
    particular.  In these domains its automated reasoning power far
    exceeds that of any other theorem prover.  Specifically, Twelf has
    been successfully employed to derive various properties of logics and
    type systems directly relevant to safety architectures, such as the
    consistency of logics and the admissibility of new inference rules
    that shorten the size of safety proofs.  Other results include
    automatic proofs of the Church-Rosser theorem, cut-elimination, and
    type preservation and progress of various operational semantics.
    Using one particular example, I will motivate the design of Twelf.


    Host:  Assaf Kfoury (kfoury@cs.bu.edu)

-------------------------------------------------------------------------------
For colloquium info, including directions, see http://cs-www.bu.edu/colloquium
-------------------------------------------------------------------------------