Formal Methods at Bell Laboratories
Formal Methods at Bell Laboratories
People
-
Glenn Bruns:
verification, temporal logic, concurrency theory
-
Dennis Dams:
abstraction, verification
-
Patrice Godefroid: program specification,
analysis, testing and verification
-
Lalita Jagadeesan: performance and reliability analysis,
testing and verification, multi-modal systems,
software engineering
-
Nils Klarlund:
program analysis, automated reasoning, programming languages, XML, input
interfaces
-
Kedar Namjoshi:
temporal logic, automata theory, verification
Some Tools
Current:
-
Delta-X:
specification of integrity constraints and generation of constraint-checking code.
-
Orion:
static analysis of C and C++ code.
-
VeriSoft:
software model checking and systematic testing.
Recent Past:
-
Spin:
general purpose efficient on-the-fly model checker (formal verification system)
for asynchronous systems based on the Promela verification language
and Linear Time Temporal Logic.
See also the
Spin Newsletters, with announcements of annual Spin Workshops.
-
Ubet:
A requirements capture tool based on message sequence charts.
-
Temporal Logic Automata Generator:
Optimized translator for an extended version of LTL into
Omega automata an Promela (Spin's input language).
-
Timeline Editor:
A visual tool for expressing logic requirements on the behavior
of a distributed system. Generates Spin never claims for verification.
-
Uno:
A simple static analysis tool for ANSI C source code.
-
Modex:
A Spin Model Extraction tool for ANSI C source code.
-
FeaVer:
An overview of the FeaVer system, which is based on
the use of Spin Version 4 and the Modex tool.
alumni
Rajeev Alur -> U Penn
Satish Chandra -> IBM Research, India
Kousha Etessami -> U of Edingburgh, UK
Amy Felty -> Univ. of Ottawa
David Hogan -> deceased
Gerard Holzmann -> JPL Laboratory for reliable software
Doug Howe -> Carleton Univ.
Elsa Gunter -> NJIT
Orna Kupferman -> Hebrew Univ. Israel
Bob Kurshan -> Cadence
David Long -> Cadence
Doron Peled -> U of Warwick, UK
Anuj Puri -> UC Berkeley
Margaret Smith -> JPL
Mihalis Yannakakis -> Columbia Univ.
Last updated on November 30, 2004.