Instructor: Professor Cormac Flanagan
Office Hours: Tuesday, 1:30-3PM, BE353A, or
by appointment
Class: Thursday 2-3:45pm, Crown College, room 105
This class will cover
topics of current research in software engineering, and will in part
focus on work of the
Verification and Validation Group
at Nasa Ames.
Schedule of Upcoming Talks
|
February 12
|
- Arnaud Venet and Guillaume Brat on NASA's C Global Surveyor |
|
February 19
|
- Willem Visser on the Java PathFinder |
|
February 26
|
- Klaus Havelund from NASA Ames. Rule-Based Runtime Verification |
|
March 4
|
- Dimitra Giannakopoulou. Automating Compositional Verification: From Design Models to Source Code.
- Corina Pasareanu. Verification of Java Programs Using Symbolic Execution and Loop Invariant Generation. |
|
March 11
|
- Dawson Engler from Stanford. Static Analysis versus Model Checking for Bug Finding |
March 11th
Dawson Engler
Static Analysis versus Model Checking for Bug Finding
Abstract.
This talk describes experiences with software model checking
after several years of using static analysis to find errors.
We initially thought that the tradeoff between the two was clear:
static analysis was easy but would mainly find shallow bugs,
while model checking would require more work but would be strictly
better --- it would find more errors, the errors would be deeper
and the approach would be more powerful. These expectations
were often wrong.
VMCAI04.pdf
March 4th
Dimitra Giannakopoulou
Automating Compositional Verification: From Design Models to Source Code
Abstract.
Model checking is an automated technique that can be
used to determine whether a system satisfies certain required
properties. To address the state explosion problem associated with
this technique, we integrate assume-guarantee verification
at different phases of system development. During design, developers
build abstract behavioral models of the system components and use them
to establish key properties of the system. To increase the
scalability of model checking at this level, we have
developed techniques that automatically decompose the verification
task by generating component assumptions for the properties to hold.
To enable more efficient reasoning of the source code,
design-level assumptions are then used to similarly decompose the
verification of the actual system implementation. We demonstrate
our approach on a significant NASA application.
Biography.
Dimitra Giannakopoulou is a RIACS research scientist at the
NASA Ames Research Center. Her research focuses on scalable
specification and verification techniques for NASA systems.
In particular, she is interested in incremental and compositional
model checking based on software components and architectures.
Prior to that, she was employed on UK and European Union projects
by Imperial College, University of London. Her work involved the
development of methods and tools for the verification of concurrent
systems based on their software architecture. Dr Giannakopoulou graduated
from the Dept. of Computer Engineering and Informatics, University of Patras,
Greece. She holds an MSc with distinction and a PhD, both from the
Dept of Computing, Imperial College, University of London. More
information can be found at http://ase.arc.nasa.gov/people/dimitra/.
Also on March 4th
Corina Pasareanu
Verification of Java Programs Using Symbolic Execution and Loop Invariant Generation
Abstract.
Software verification is recognized as an important and difficult problem. We present a framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method
specifications and loop invariants. We present an iterative technique that uses invariant strengthening and approximation for discovering (some of) these loop invariants automatically. The technique handles different types of
data (e.g. boolean and numeric constraints, dynamically allocated structures and arrays) and it allows for checking universally quantified formulas. Our framework is built on top of the Java PathFinder model checking toolset and
it was used for the verification of several non-trivial Java programs.
Biography.
Corina Pasareanu is a Kestrel research scientist at NASA Ames Research Center, the Automated Software Engineering Group. Her research interests are in using symbolic techniques and automated tools, such as model checkers and
theorem provers, as a base for efficient verification and validation of software. She is also interested in synthesis of code from temporal logic specifications and in assume-guarantee reasoning for the verification of software.
She received her PhD degree from Kansas State University, the Department of Computing and Information Sciences. More information can be found at http://ase.arc.nasa.gov/people/pcorina/.
February 26th
Klaus Havelund
Rule-Based Runtime Verification
Abstract.
We present a rule-based framework, named Eagle, for defining and implementing
finite trace monitoring logics, including future and past time temporal logic,
extended regular expressions, real-time logics, interval logics, forms of
quantified temporal logics, and so on. Our logic is implemented as a Java
library and involves novel techniques for rule definition, manipulation and
execution. Monitoring is done on a state-by-state basis, without storing the
execution trace. The Eagle logic can be used for writing sophisticated
properties about a program, and the Eagle engine can then be used to monitor
program executions. This can either be done on-the-fly, or in batch on
generated trace (log) files.
Biography.
Klaus Havelund is a researcher at Kestrel technology, NASA Ames Research
Center, in the Automated Software Engineering group. His work focuses on the
application of formal methods techniques to the analysis and testing of
software applications. His previous work at NASA Ames includes a first
version of the Java PathFinder model checker, a translator from Java to SPIN.
During the last 3 years, he has done work in runtime monitoring, developing
algorithms for concurrency analysis (deadlocks and data races) and temporal
logic monitoring, and has worked on automated program instrumentation tools.
February 19th
Willem Visser
Model Checking and Symbolic Execution for Test-input Generation
Abstract.
The talk will consist of three parts: a brief introduction to the Java
PathFinder (JPF) model checker, symbolic execution as implemented in
JPF, and how the latter is used to do test-input generation. The
introduction to JPF will include a description of the general
architecture as well as examples of the tool?s usage. The symbolic
execution within JPF is novel since it supports both the more
traditional constraint solving over (linear) integer constraints as well
as structural constraints for arrays, linked lists, red-black trees,
etc. The main part of the talk will focus on the use of symbolic
execution within JPF to generate test-inputs for code manipulating
complex data-structures. Specifically we will show how to generate tests
in a black-box and white-box fashion for the red-black tree
implementation of the Java TreeMap library.
Biography.
Willem Visser received his Ph.D. from the University of Manchester in
1998. His thesis introduced the first efficient automata-theoretic
algorithm for model checking CTL* properties. Prior to his PhD he
received an M.Sc from the University of Stellenbosch (South Africa) for
his work on the development of a model checker for operating system
kernels. After completion of his Ph.D. studies he taught a course on
model checking at the University of Stellenbosch for 3 months and in
October 1998 started work at the Research Institute for Advanced
Computer Science (RIACS) at NASA Ames.
His main research focus is on the application of model checking to
programming languages. To this end he has been the main developer of the
Java PathFinder model checker for Java ? that won the 2003 TGIR
Engineering Innovation award from the Office of Aerospace Technology at
NASA. This model checker is the first model checker that is custom-made
for the Java language. His current work focuses on using symbolic
execution and model checking for test-case generation and program
proofs, environment generation, feasible counter-example detection
during abstraction-based model checking, belief-logics and agent
verification.
February 12th
Arnaud Venet
Rapid Inference of Interprocedural Numerical Invariants for Large C
Programs by Abstract Interpretation
In this talk we will show how to scale classical abstract interpretation
techniques in order to infer interprocedurally valid numerical
invariants for large programs (> 100 KLOC) with an analysis time
comparable to the compile time. Numerical invariants are of the utmost
importance when it comes to designing precise verification engines. We
illustrate the interest of these techniques by showing how this
information can be used to perform static array-bound checking and
achieve a level of false positives < 20%.
The algorithms rely on an adaptive representation of pointer offsets and
numerical invariants using cofibered domains. These techniques form the
algorithmic core of C Global Surveyor a static array-bound checker that
we have developed at NASA Ames. We will introduce the basic concepts of
Abstract Interpretation and show step-by-step how to achieve
scalability. This presentation can therefore be seen as an introduction
to Abstract Interpretation as well.
Guillaume Brat
Software Analysis Opportunities at NASA
Despite the current success of the MER mission, there is
still a strong concern at NASA that the line between a successful and
a failed mission is extremely thin. Moreover, given the increasing
reliance on software, and in particular autonomy software, there is
renewed interest in software reliability and software V&V. Specifically,
it is more and more accepted that NASA has to depart from its traditional
test-based approach to V&V and pay greater attention to automated V&V
techniques, especially those based on formal methods. In this talk,
I will first describe the role static analysis will play in the V&V
of the next big Mars mission (MSL), and then elaborate on the role
other formal verification techniques can play. I will also try to convey
what it takes for formal methods to be accepted by mission managers
and developers. Finally, I'll give a sense of what technology infusion
opportunities are opening up as NASA starts implementing the vision of
the President.