@inproceedings{3607cdff4c8e4922971898a5c02ec281,
title = "Verifying SystemC with predicate abstraction: A component based approach",
abstract = "The SystemC waiting-state automaton is a compositional formal model for verifying properties of SystemC at the transaction level within a delta-cycle: the smallest simulation unit time in SystemC. In this paper, we first propose how to extract automata for SystemC components where we distinguish between threads and methods in SystemC. Then, we propose an approach based on a combination of symbolic execution and computing fixed points via predicate abstraction to infer relations between predicates generated during symbolic execution.",
author = "Nesrine Harrath and Bruno Monsuez and Kamel Barkaoui",
year = "2013",
month = jan,
day = "1",
doi = "10.1109/IRI.2013.6642516",
language = "English",
isbn = "9781479910502",
series = "Proceedings of the 2013 IEEE 14th International Conference on Information Reuse and Integration, IEEE IRI 2013",
publisher = "IEEE Computer Society",
pages = "536--545",
booktitle = "Proceedings of the 2013 IEEE 14th International Conference on Information Reuse and Integration, IEEE IRI 2013",
note = "2013 IEEE 14th International Conference on Information Reuse and Integration, IEEE IRI 2013 ; Conference date: 14-08-2013 Through 16-08-2013",
}