Abstract: I am going to present the work of the Automated Software Engineering Group in program model checking, and I will describe in specific Java PathFinder, a model checker for Java, under development at the NASA Ames Research Center.
Model checking has been successfully applied to hardware system, but the application of the same techniques to software is not always straightforward. Modern programming languages offer features that are not always easy to handle during model checking.
The group is also trying to bridge the gap between model checking and testing. Since the complexity involved in a non trivial software system might be too high to prove its correctness, the group is trying to develop techniques that can reveal bugs in the system in a more systematic way than testing.

Biography: Born on 6/14/75, he holds a M.S. in Computer Engineering (2000) from Politecnico di Torino (Italy). He has been a visiting scientist in the Automated Software Engineering group at the NASA Ames Research Center from November of 1999 to March of 2000. After his graduation, he joined the Software Engineering group at the NASA Ames Research Center. There, he worked on software verification until he started his Ph.D. in Computer Science at Carnegie Mellon University in September of 2001, where he has joined Prof. Edmund M. Clarke research group.