About: ISP Formal Verification Tool

An Entity of Type: software, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

ISP ("In-situ Partial Order") is a tool for the formal verification of MPI 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. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool.Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST.Relevant interleavings are computed using a customized dynamic partial order reduction algorithm called POE.

Property Value
dbo:abstract
  • ISP ("In-situ Partial Order") is a tool for the formal verification of MPI 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. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool.Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST.Relevant interleavings are computed using a customized dynamic partial order reduction algorithm called POE. 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 Microsoft MPI libraries. ISP is available for download for linux and Mac OS X; as a Visual Studio plugin for running under Windows, and as an Eclipse plugin.. (en)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 21770993 (xsd:integer)
dbo:wikiPageLength
  • 5224 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 996198227 (xsd:integer)
dbo:wikiPageWikiLink
dcterms:subject
gold:hypernym
rdf:type
rdfs:comment
  • ISP ("In-situ Partial Order") is a tool for the formal verification of MPI 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. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool.Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST.Relevant interleavings are computed using a customized dynamic partial order reduction algorithm called POE. (en)
rdfs:label
  • ISP Formal Verification Tool (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License