ISP (”In-situ Partial Order”) is a tool for the formal verification of MPI(Message Passing Interface) programs developed within the School of Computing at the University of Utah. Like model checkers, such as SPIN, ISP 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. ISP has been used to successfully verify up to 14,000 lines of MPI/C code for deadlocks and assertion violations. It currently supports over 60 MPI 2.1 functions, and has been tested with MPICH2, OpenMPI,and MicrosoftMPI libraries.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Botbol, Vincent; Chailloux, Emmanuel; Le Gall, Tristan: Static analysis of communicating processes using symbolic transducers (2017)
- Böhm, Stanislav; Běhálek, Marek; Meca, Ondřej; Šurkovský, Martin: Kaira: development environment for MPI applications (2014)
- Li, Guodong; Palmer, Robert; DeLisi, Michael; Gopalakrishnan, Ganesh; Kirby, Robert M.: Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API (2011)
- Siegel, Stephen F.; Zirkel, Timothy K.: Collective assertions (2011)
- Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
- Siegel, Stephen F.; Zirkel, Timothy K.: FEVS: a functional equivalence verification suite for high-performance scientific computing (2011)
- Gopalakrishnan, Ganesh; Kirby, Robert M.: Practical formal verification of MPI and thread programs (2009) ioport
- Vakkalanka, Sarvani; DeLisi, Michael; Gopalakrishnan, Ganesh; Kirby, Robert M.; Thakur, Rajeev; Gropp, William: Implementing efficient dynamic formal verification methods for MPI programs (2008) ioport
- Vakkalanka, Sarvani; Gopalakrishnan, Ganesh; Kirby, Robert M.: Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings (2008)