[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday October 31, 2007, 12:00pm-1:30pm
Room 108 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
**note non-standard room and starting time**

CCIS Distinguished Lecture
Machines Reasoning About Machines
J Moore
University of Texas at Austin

Computer hardware and software can be modeled precisely in
mathematical logic.  If expressed appropriately, these models can be
executable.  This allows them to be used as simulation engines or
rapid prototypes.  But because they are formal they can be manipulated
by symbolic means: theorems can be proved about them, directly, with
mechanical theorem provers.  But how practical is this vision of
machines reasoning about machines?  In this highly personal talk, I
will describe the 35 year history of the ``Boyer-Moore Project'' and
discuss progress toward making formal verification practical.  Among
other examples I will describe important theorems about commercial
microprocessor designs, including parts of processors by AMD,
Motorola, IBM, Rockwell-Collins and others.  Some of these
microprocessor models execute at 90% the speed of C models and have
had important functional properties verified.  In addition, I will
describe a model of the Java Virtual Machine, including class loading
and bytecode verification and the proofs of theorems about JVM
methods.


Upcoming Events:

# 11/7 Vassilis Koutavas: The join-calculus and polyphonic C-sharp
# 11/14 Guy Steele: Designing by Accident: a History of Scheme
# Wed 11/21 Thanksgiving; no meeting
# Wed 11/28 Ryan Newton: Language Support for Distributed Stream Processing
# Wed 12/05 Riccardo Pucella: The Manticore project

--Mitch