Skip to main content
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
[ptp-dev] ISP Formal Verification Tool
Hello,

I'd like to introduce myself. My name is Alan Humphrey of Formal Methods Research (FMR), headed by Professor Ganesh Gopalakrishnan & Robert M. Kirby at the University of Utah's School of Computing. FMR has developed ISP (In-situ Partial Order), a formal verification tool for MPI programs which verifies the complete state space of a system for a set of safety properties. However, unlike model checkers, ISP performs code level verification. This means that the tool verifies all relevant interleavings of a concurrent program by replaying the actual program code without building verification models.

In summary, the main features of ISP are the following:

  • Supports over 60 MPI 2.1 functions (see user manual for details)
  • Runs under Linux, MAC OS/X, and Windows.
  • The windows version has a Visual Studio plug-in that is also downloadable.
  • Tested with MPICH2, OpenMPI, and Microsoft MPI libraries.
  • Push-button formal verification of thousands of lines of MPI/C code in seconds, for deadlocks, assertion violations, MPI object leaks, and communication races (unexpected communication matches).
  • Comes with 100s of benchmark examples
  • Runs faster on multi-core machines, thanks to OpenMP based parallelization
  • BSD License
  • We can also offer you the ISO image of a LiveCD that you can burn to boot ISP on virtually any machine.
A Wikipedia page on ISP can be found at:
http://en.wikipedia.org/wiki/ISP_Formal_Verification_Tool

ISP is available for download for Linux and Mac OS X; also as a Visual Studio plugin for running under Windows at:
http://www.cs.utah.edu/formal_verification/ISP-release/

Prof. Gopalakrishnan and I have been speaking with Beth Tibbitts about our group's plans for adapting ISP to Eclipse via the PTP External Tools Framework as an extension. We hope to be in contact with as many of you as we can throughout this process, as we'll certainly have questions. Any initial advice/direction would be greatly appreciated.

I'll be calling into this month's PTP status call to meet you. Looking forward to learning more!

-Alan Humphrey
University of Utah
School of Computing

Back to the top