{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:05:31Z","timestamp":1747868731522},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642223051"},{"type":"electronic","value":"9783642223068"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22306-8_7","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T11:25:05Z","timestamp":1309778705000},"page":"90-107","source":"Crossref","is-referenced-by-count":7,"title":["An Analytic Evaluation of SystemC Encodings in Promela"],"prefix":"10.1007","author":[{"given":"Daniele","family":"Campana","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Iman","family":"Narasamdya","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","first-page":"125","volume-title":"QEST","author":"G. Behrmann","year":"2006","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125\u2013126. IEEE, New York (2006)"},{"key":"7_CR2","first-page":"356","volume-title":"ICCAD","author":"N. Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D.: Race Analysis for SystemC using Model Checking. In: ICCAD, pp. 356\u2013363. IEEE, New York (2008)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-78800-3_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: A Tool for the Analysis of SystemC\u00a0Models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 467\u2013470. Springer, Heidelberg (2008)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos: A Software Model Checker for SystemC. In: CAV (to appear, 2011)","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"7_CR5","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a Software Model Checking Approach. In: FMCAD, pp. 51\u201359 (2010)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-19835-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2011","unstructured":"Cimatti, A., Narasamdya, I., Roveri, M.: Boosting lazy abstraction for systemC with partial order reduction. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 341\u2013356. Springer, Heidelberg (2011)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kr\u00f6ning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"7_CR8","first-page":"4167","volume-title":"ISCAS","author":"D. Gro\u00dfe","year":"2005","unstructured":"Gro\u00dfe, D., Drechsler, R.: CheckSyC: An Efficient Property Checker for RTL SystemC Designs. In: ISCAS, vol.\u00a04, pp. 4167\u20134170. IEEE, New York (2005)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Grosse, D., Le, H., Drechsler, R.: Proving Transaction and System-level Properties of Untimed SystemC TLM Designs. In: MEMOCODE, pp. 113\u2013122 (2010)","DOI":"10.1109\/MEMCOD.2010.5558643"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"7_CR11","first-page":"131","volume-title":"CODES+ISSS","author":"P. Herber","year":"2008","unstructured":"Herber, P., Fellmuth, J., Glesner, S.: Model Checking SystemC Designs using Timed Automata. In: CODES+ISSS, pp. 131\u2013136. ACM, New York (2008)"},{"key":"7_CR12","first-page":"78","volume":"65","author":"G.J. Holzmann","year":"2005","unstructured":"Holzmann, G.J.: Software Model Checking with SPIN. Adv. in Comp.\u00a065, 78\u2013109 (2005)","journal-title":"Adv. in Comp."},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197\u2013211. Chapman & Hall, Ltd, London (1995)"},{"key":"7_CR14","first-page":"101","volume-title":"MEMOCODE","author":"D. Kroening","year":"2005","unstructured":"Kroening, D., Sharygina, N.: Formal Verification of SystemC by Automatic Hardware\/Software Partitioning. In: MEMOCODE, pp. 101\u2013110. IEEE, New York (2005)"},{"key":"7_CR15","first-page":"936","volume-title":"DAC","author":"S. Kundu","year":"2008","unstructured":"Kundu, S., Ganai, M.K., Gupta, R.: Partial Order Reduction for Scalable Testing of SystemC TLM Designs. In: DAC, pp. 936\u2013941. ACM, New York (2008)"},{"key":"7_CR16","unstructured":"Marquet, K., Jeannet, B., Moy, M.: Efficient Encoding of SystemC\/TLM in Promela. Technical report, Verimag, Verimag Research Report no TR-2010-7 (2010)"},{"key":"7_CR17","first-page":"26","volume-title":"ACSD","author":"M. Moy","year":"2005","unstructured":"Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. In: ACSD, pp. 26\u201335. IEEE, New York (2005)"},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1145\/1086228.1086286","volume-title":"EMSOFT","author":"M. Moy","year":"2005","unstructured":"Moy, M., Maraninchi, F., Maillet-Contoz, L.: Pinapa: An Extraction Tool for SystemC Descriptions of Systems-on-a-Chip. In: EMSOFT, pp. 317\u2013324. ACM, New York (2005)"},{"key":"7_CR19","first-page":"1","volume-title":"FMCAD","author":"D. Tabakov","year":"2008","unstructured":"Tabakov, D., Kamhi, G., Vardi, M.Y., Singerman, E.: A Temporal Language for SystemC. In: FMCAD, pp. 1\u20139. IEEE, New York (2008)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Tabakov, D., Vardi, M.: Monitoring Temporal SystemC Properties. In: MEMOCODE, pp. 123\u2013132 (2010)","DOI":"10.1109\/MEMCOD.2010.5558640"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-73370-6_14","volume-title":"Model Checking Software","author":"C. Traulsen","year":"2007","unstructured":"Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC\/TLM Semantics in Promela and Its Possible Applications. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 204\u2013222. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22306-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T02:55:09Z","timestamp":1592708109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22306-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642223051","9783642223068"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22306-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}