, , 2008.
Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories, IFIP AICT, vol.403, pp.116-127, 2013. ,
DOI : 10.1007/978-3-642-38853-8_11
URL : https://hal.archives-ouvertes.fr/hal-01466667
Software Model Checking SystemC, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.32, issue.5, pp.774-787, 2013. ,
DOI : 10.1109/TCAD.2012.2232351
A Tool for Checking ANSI-C Programs, TACAS. LNCS, pp.168-176, 2004. ,
DOI : 10.1007/978-3-540-24730-2_15
Improving systemlevel verification of systemc models with spin, pp.74-79, 2013. ,
Verification of an industrial SystemC/TLM model using LOTOS and CADP, 2009 7th IEEE/ACM International Conference on Formal Methods and Models for Co-Design, pp.46-55, 2009. ,
DOI : 10.1109/MEMCOD.2009.5185377
URL : https://hal.archives-ouvertes.fr/inria-00408283
Proving transaction and system-level properties of untimed SystemC TLM designs, Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp.113-122, 2010. ,
DOI : 10.1109/MEMCOD.2010.5558643
Generating Finite State Machines from SystemC, Design, Automation and Test in Europe, pp.76-81, 2006. ,
DOI : 10.1109/date.2006.243777
URL : http://www.date-conference.com/proceedings/PAPERS/2006/DATE06/DF_FILES/06D_2.PDF
TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox, Leibniz Transactions on Embedded Systems, vol.1, issue.1, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00429070
Model checking SystemC designs using timed automata, Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, CODES/ISSS '08, pp.131-136, 2008. ,
DOI : 10.1145/1450135.1450166
URL : http://www.cecs.uci.edu/~papers/esweek08/codes/p131.pdf
, IEEE Standards Association: IEEE Std Open SystemC Language Reference Manual, pp.1666-2011, 2011.
Formal Verification of SystemC Designs Using a Petri-Net Based Representation, Proceedings of the Design Automation & Test in Europe Conference, pp.1228-1233, 2006. ,
DOI : 10.1109/DATE.2006.244076
The UCLID Decision Procedure, LNCS, vol.3114, pp.475-478, 2004. ,
DOI : 10.1007/978-3-540-27813-9_40
Model Checking Memory-Related Properties of Hardware/Software Co-designs, IFIP AICT, vol.403, pp.92-103, 2013. ,
DOI : 10.1007/978-3-642-38853-8_9
URL : https://hal.archives-ouvertes.fr/hal-01466696
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, TACAS. LNCS, 2009. ,
DOI : 10.1007/978-3-540-78800-3_24
Checking Safety Properties Using Induction and a SAT-Solver, FMCAD, LNCS, 2000. ,
DOI : 10.1007/3-540-40922-X_8