About: CPAchecker

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

CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.CPAchecker is based on the idea of configurable program analysiswhich is a concept that allows expression of both model checking and program analysis with one formalism.When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached.

Property Value
dbo:abstract
  • CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.CPAchecker is based on the idea of configurable program analysiswhich is a concept that allows expression of both model checking and program analysis with one formalism.When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached. One application of CPAchecker is the verification of Linux device drivers. (en)
dbo:wikiPageID
  • 37859257 (xsd:integer)
dbo:wikiPageLength
  • 4143 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1090802967 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
gold:hypernym
rdf:type
rdfs:comment
  • CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.CPAchecker is based on the idea of configurable program analysiswhich is a concept that allows expression of both model checking and program analysis with one formalism.When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached. (en)
rdfs:label
  • CPAchecker (en)
owl:sameAs
prov:wasDerivedFrom
foaf:homepage
foaf:isPrimaryTopicOf
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