More recently, at JPL, I have become interested in the connections between model checking and (randomized) testing -- including using the same models and tools for both, reusing simulation infrastructure, and hybrid approaches such as randomized testing with the complete nondeterminism of model checking. More "frivolously" I have also become fascinated by the taxonomy and nature of actual bugs in programs, particularly file systems.
More generally, I see model checking (like well-done testing) primarily as a useful tool for program understanding -- the investigative side of software engineering, if you will. Model checking traditionally answers the question: does my (program, protocol, design) have a trace like this? Testing, in a sense, answers the same question. Even at the earliest stages of software design, thinking about how to make answering that question easier not only eventually aids verification, but helps us think about how a program will actually execute. One interesting possibility to consider is the use of model checking and other state-space exploration methods to help visualize the executions of a program. Recent work at IBM has shown the value of visualizing memory configurations of large systems; it seems that program trace-spaces would also be useful in software engineering and performance debugging.
UPDATE (7/1/10): Not updating this site as well as I should... faculty life is busy. On PC for SAVCBS 2010, NASA Formal Methods 2011, FASE 2011... Those research changes mostly involve interest in end-user testing/debugging for machine-learned software, with Margaret Burnett and fellow CMU-er Weng-Keen Wong.
UPDATE (5/1/09): I'll be on the PC for SAVCBS 2009. I'll probably be changing research directions in some new and exciting ways (though also continuing past work) as a faculty member at Oregon State University, starting later this summer.
UPDATE (1/5/09): I'm on the PC for this year's Workshop on Constraints in Formal Verification. Submit away.
UPDATE (8/5/08): Paper for my invited talk at CFV'08 and VERIFY'08 gives a nice overview of the file system verification & testing that's occupied my time the last couple of years, and a lot of what LaRS has been up to in general. Take our conclusions on the success of various methods with a grain of salt -- one lab, a handful of people -- still, I think it's safe to say that for rich properties depending on data, the automated predicate abstraction tools aren't really ready for prime time (unless you have the authors captive, maybe).
UPDATE (6/26/08): I'll be on the PC for SAVCBS 2008. I just (a week ago) joined the MSL Flight Software Internal Test (FIT) team as lead developer/designer for the test automation framework. I don't know how much "research"y testing will be useful here, but after this I might be more worth listening to when I opine that something does or does not work in testing Actual Important Code.
UPDATE (6/10/08): More papers, first a write-up of some work on automated testing of models from AI planners, at MoChArt 2008. More central to what I've been working on lately, there's an ASE paper, "Random Test Run Length and Effectiveness," mostly based on the file system testing here at JPL. Unfortunately, we don't actually propose a solution to the problem of selecting an optimal (or even good) test run length, but the data does demonstrate pretty convincingly (IMO) that this is a major factor in whether random testing is effective for a system. This paper wouldn't have been written if not for Carlos Pacheco asking an innocent question after my ICSE '07 talk. Makes me wonder what else you have to luck into getting right in order for random testing to work (that we're not investigating)...
UPDATE (5/16/08): Papers at WODA 2008 and SPIN 2008. First is on
using SPIN to do both random testing and model checking -- with a
little comparison of the two. Also sort of an "advertisement" paper,
to see if any other dynamic analysis folks want to use SPIN to do this
kind of thing -- I think we do show that it's pretty darn easy to do.
The second one's a tool paper on heuristics for finding bugs with SPIN
(and they do seem to work surprisingly well, perhaps even better than
the paper suggests, says the slightly dubious third author). Other
than that, using the ideas in both these papers to test the heck out
of the MSL file storage
modules, with pretty good results (but we'd like to find EVERY LAST
BUG before we head to Mars).
UPDATE (4/14/08): I'll be the invited speaker at the Constraints in Formal Verification 08 workshop in Australia this August, where I'll discuss "Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving."
UPDATE (2/19/08): Klaus Havelund and I will be teaching CS 119 Reliable Softare: Testing and Monitoring at Caltech starting April 1st. Should be enjoyable --- perhaps I'll know more about how to test sotware after we're done...
UPDATE (2/5/08): Congratulations to my advisor, Ed Clarke, who won this year's ACM Turing Award (along with Emerson and Sifakis) for inventing model checking!
UPDATE (1/12/08): Presented "Extending Model Checking with Dynamic Analysis" at VMCAI '08. Preparing a talk on the same rough topic for this year's SoCal Workshop on Programming Languages and Systems, and giving a talk on some similar themes (at a high level) at Caltech on the 19th. In general, this is all looking at the places where model checking and testing intersect -- when state spaces are too large, and properties too rich (full functional correctness of a file system, for example) for automated abstraction, what can we do? Random testing is useful (I'm looking at how to wisely carve up a test budget into test runs, with Jamie Andrews at Western Ontario and RuGang Xu, summer intern '07 from UCLA), but explicit-state model checking with the expectation that you won't cover the whole state space seems better for programs well fit for a small nondeterministic harness. Where do "design for testability" and "design for verification" lead? Not, probably, to programmers working with temporal logic or theorem provers.
Enjoying reading Andreas Zeller's Why Programs Fail.
I'll be on the program committee for the 1st International Workshop on Verification and Debugging (the site's a bit preliminary right now), to be held with CAV '06 as part of FLOC.
A list of my publications is available.
My research is associated with or I'm directly working on the following tools, which are available for download:
CBMC is a bounded model checker for ANSI-C programs. It
provides verification for array bounds, pointer safety, exceptions and
user-specified assertions.
Coming soon: I will be releasing the explain tool for use in understanding counterexamples produced by CBMC.
MAGIC is a tool for compositional verification of (concurrent) ANSI-C programs, based on a two-level CounterExample-Guided Abstraction Refinment (CEGAR) approach.
I worked with Sagar Chaki, Ofer Strichman, and Edmund Clarke on the predicate minimization algorithm used in MAGIC, and am now implementing distance metric-based error explanation for MAGIC.
The Java PathFinder is a tool based on a novel Java Virtual Machine (JVM) allowing model checking and testing of Java bytecode programs. I worked with NASA Ames Research Center's Automated Software Engineering group on JPF over two summers as a participant in the Summer Student Research Program.
In other news, JPF was open sourced today! It took a while, but Willem and Jon and Peter did it; way to go, guys. The release is here, and the Slashdot story(!) is here. Even I felt the effects -- factor of 10 or more boost in hits on my home page today. I guess Java model checking is famous now?
In the past at CMU I worked some on Sergey Berezin's SyMP system, although Sergey ended up spending more time fixing my code than it would have taken to write it himself, I suspect.
UPDATE (6/16/00): This summer I'm working with Mihalis Yannakakis and Doron Peled at Lucent/Bell Labs on black box checking.
UPDATE (8/29/00): Back at CMU, but continuing work on black-box checking as well as other things.
UPDATE (1/16/02): A couple of papers to be published: "Adaptive Model Checking," by myself, Doron Peled, and Mihalis Yannakakis, to be published in the proceedings of TACAS 2002 and "Heuristic Model Checking for Java Programs," with Willem Visser, to be published in the proceedings of SPIN 2002.
UPDATE (4/26/02): "Model Checking Java Programs using Structural Heuristics" will appear in ISSTA 2002. As the semester finishes at CMU, I'm working with Sagar Chaki on predicate abstraction, in particular analyzing automatically discovered predicates, before returning to NASA Ames this summer.
UPDATE (2/14/03): A couple more papers to be published: "Modular Verification of Software Components in C," by Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith, to be presented at ICSE 2003 and "What Went Wrong: Explaining Counterexamples," with Willem Visser, to appear in SPIN 2003 (SPIN is being held after ICSE this year). I'm currently investigating optimization for predicate abstraction (for Sagar Chaki's MAGIC tool) and methods for automatically explaining counterexamples, possibly in the world of autonomous systems.
UPDATE (5/12/03): Wednesday, May 21st, at 10:00 AM in WH 5409,
I will be presenting my thesis proposal, on the topic: "Explaining
Counterexamples: Causal Analysis and Comparison of Transition
Sequences" (abstract). My
committee members are Edmund Clarke, David Garlan, Reid Simmons, and
Willem Visser.
"Modular Verification of Software Components in
C" was one of two ICSE ACM SIGSOFT Distinguished Paper Award
winners. The MAGIC tool
has been officially released.
UPDATE (6/13/03): My thesis topic has been approved and I am
continuing work on my approach for explaining (and possibly
automatically suggesting fixes for) errors in programs.
"Predicate Abstraction with Minimum
Predicates" was accepted for publication in CHARME 2003.
UPDATE (8/03/03): Initial implementation of error explanation within the CBMC bounded model-checker for ANSI-C programs is complete, but lacking a number of features. CBMC is available now for download, and I hope to have an alpha release of error explanation capabilities before too long. Better handling of arrays and structures and integration with the GUI are the only major features needed before release.
UPDATE (11/21/03): I'll be attending Dagstuhl Seminar 03491, Understanding Program Dynamics right after Thanksgiving, presenting my work on error explanation with distance metrics.
"Efficient Verification of Sequential and Concurrent C Programs," by Sagar Chaki, Edmund Clarke, Joel Ouaknine, Ofer Strichman, Karen Yorav, and myself, has just been accepted for publication in the special Software Model Checking issue of Formal Methods in System Design. "Heuristics for Model Checking Java Programs" by Willem Visser and myself has been accepted for publication in Software Tools for Technology Transfer.
The explain tool is ready for release, but I haven't gotten around to it yet, and would like to better integrate it with the CBMC GUI before putting it on the website.
UPDATE (12/12/03): "Error Explanation with Distance Metrics" was accepted for publication in TACAS 2004.
UPDATE (3/26/04): "Understanding Counterexamples with explain" was accepted for publication in CAV 2004. I'm off tomorrow to Barcelona for ETAPS to present the distance metric paper. In the meantime, I've implemented distance metric based error explanation for MAGIC, and it's working quite nicely.
I forgot to mention the journal version of the ICSE paper also being accepted (see publications page).
UPDATE (6/11/04): "Explaining Abstract Counterexamples" will appear at FSE (Foundations of Software Engineering) in November. "Making the Most of BMC Counterexamples" has been accepted for BMC'04, the second workshop on Bounded Model Checking.
UPDATE (2/17/05): I've scheduled a thesis defense for March 3rd (two weeks from now) and will be starting work at JPL's Laboratory for Reliable Software (LaRS) as soon as I finish up at CMU (and move to California). It should be a great opportunity to do some serious model checking research with real-world (and other-worldly!) examples.
My thesis draft looks to be in good shape for public release, though I expect to be tweaking it until the defense or shortly thereafter.
UPDATE (3/3/05): Successful thesis defense today! I will be making some changes to address a few points that need to be clarified, and then, well, it's on to Mars, so to speak...