|
 
|
[HMB13] Verifying SystemC with Predicate Abstraction: a Component Based Approach
Conférence Internationale avec comité de lecture : On the 14th International Conference on Information Reuse and Integration (IEEE IRI), August 2013, San Francisco, USA,Mots clés: SystemC, automata, symbolic execution, predicate abstraction,formal verifi cation
Résumé:
The SystemC waiting-state automaton is a compositional abstract
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 rst 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 xed points via predicate abstraction to infer relations between predicates generated during symbolic execution.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| HMB13, | |||
| title | = | "{Verifying SystemC with Predicate Abstraction: a Component Based Approach}", | |
| author | = | " N. Harrath and B. Monsuez and K. Barkaoui ", | |
| booktitle | = | "{On the 14th International Conference on Information Reuse and Integration (IEEE IRI)}", | |
| year | = | 2013, | |
| month | = | "August", | |
| address | = | "San Francisco, USA", | |
| } | |||
