[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, October 29, 2008
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Aaron Turon
NU PRL

Spec# and Boogie

The Spec#/Boogie tools are a Microsoft-backed foray into lightweight
software verification.  The aim of the project is similar in spirit to
"extended static checking": go beyond (decidable) type systems to do
more sophisticated, behavioral analysis of code, but stop short of
performing full verification.  A working hypothesis is that there is a
lucrative middle ground between the virtually free structural checks
provided by type checkers, and high-cost verification.  Although the
Spec#/Boogie analysis requires a theorem prover, the system is fully
automated, and programmers interact with the analysis through compiler
errors that refer to specific code locations and specification
failures.

Unlike ESC/Java, the Spec#/Boogie stack provides a sound program analysis.

The project is broken into two modular components, Spec# and Boogie.
Spec# is an extension of the C# language with nonnull types, method
contracts, object invariants, and an ownership model of the heap.
Used in isolation, Spec# compiles annotated code to MSIL bytecode with
dynamic checks.  Boogie, on the other hand, is an intermediate
language for verification, similar to Dijkstra's language of guarded
commands.  The Boogie tool infers loop invariants and generates
verification conditions from a Boogie program.  Boogie can be used
(soundly) as a back-end for the Spec# compiler; if the resulting
analysis succeeds, then no dynamic check in the compiled program will
ever fail.

I will discuss the most important features of both Spec# and Boogie in
detail, and also demonstrate how the tools are used together.


================================================================

Upcoming Events:

# Wed 11/5 Riccardo Pucella: Stateful RCF
# Wed 11/12 no seminar
# Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming
  for sensor networks (tentative)

--Mitch