@inproceedings{Beer2015Symbo-31853,
  year={2015},
  doi={10.1007/978-3-319-23404-5_14},
  title={Symbolic Causality Checking Using Bounded Model Checking},
  number={9232},
  isbn={978-3-319-23403-8},
  issn={0302-9743},
  publisher={Springer International Publishing},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Model Checking Software : 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings},
  pages={203--221},
  editor={Fischer, Bernd},
  author={Beer, Adrian and Heidinger, Stephan and Kühne, Uwe and Leitner-Fischer, Florian and Leue, Stefan}
}

<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/31853">
    <dcterms:abstract xml:lang="eng">In precursory work we have developed causality checking, a fault localization method for concurrent system models relying on the Halpern and Pearl counterfactual model of causation that identifies ordered occurrences of system events as being causal for the violation of non-reachability properties. Our first implementation of causality checking relies on explicit-state model checking. In this paper we propose a symbolic implementation of causality checking based on bounded model checking (BMC) and SAT solving. We show that this BMC-based implementation is efficient for large and complex system models. The technique is evaluated on industrial size models and experimentally compared to the existing explicit state causality checking implementation. BMC-based causality checking turns out to be superior to the explicit state variant in terms of runtime and memory consumption for very large system models.</dcterms:abstract>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:creator>Heidinger, Stephan</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-09-29T10:03:13Z</dcterms:available>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Heidinger, Stephan</dc:contributor>
    <dcterms:issued>2015</dcterms:issued>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-09-29T10:03:13Z</dc:date>
    <dc:language>eng</dc:language>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:creator>Kühne, Uwe</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/31853/1/Beer_2-1cqocmbol3jvh3.pdf"/>
    <dc:contributor>Kühne, Uwe</dc:contributor>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/31853"/>
    <dc:contributor>Beer, Adrian</dc:contributor>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Beer, Adrian</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/31853/1/Beer_2-1cqocmbol3jvh3.pdf"/>
    <dcterms:title>Symbolic Causality Checking Using Bounded Model Checking</dcterms:title>
  </rdf:Description>
</rdf:RDF>