{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:53:31Z","timestamp":1725594811049},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221095"},{"type":"electronic","value":"9783642221101"}],"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-22110-1_24","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T13:08:45Z","timestamp":1309784925000},"page":"310-316","source":"Crossref","is-referenced-by-count":37,"title":["Kratos \u2013 A Software Model Checker for SystemC"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Micheli","sequence":"additional","affiliation":[]},{"given":"Iman","family":"Narasamdya","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","first-page":"25","volume-title":"FMCAD","author":"D. Beyer","year":"2009","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332. IEEE, Los Alamitos (2009)"},{"issue":"5-6","key":"24_CR2","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"24_CR3","first-page":"189","volume-title":"FMCAD","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate Abstraction with Adjustable-Block Encoding. In: FMCAD, pp. 189\u2013197. IEEE, Los Alamitos (2010)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathSAT\u00a04 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"24_CR6","unstructured":"Campana, D., Cimatti, A., Narasamdya, I., Roveri, M.: An Analytic Evaluation of SystemC Encodings in Promela, submitted for publication"},{"issue":"4","key":"24_CR7","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A New Symbolic Model Checker. STTT\u00a02(4), 410\u2013425 (2000)","journal-title":"STTT"},{"key":"24_CR8","first-page":"9","volume-title":"FMCAD","author":"A. Cimatti","year":"2009","unstructured":"Cimatti, A., Dubrovin, J., Junttila, T., Roveri, M.: Structure-aware computation of predicate abstraction. In: FMCAD, pp. 9\u201316. IEEE, Los Alamitos (2009)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos \u2013 A Software Model Checker for SystemC. Tech. rep., FBK-irst (2011), https:\/\/es.fbk.eu\/tools\/kratos","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"24_CR10","first-page":"51","volume-title":"FMCAD","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a Software Model Checking Approach. In: FMCAD, pp. 51\u201359. IEEE, Los Alamitos (2010)"},{"key":"24_CR11","first-page":"1707","volume-title":"Proc. of DATE","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Kalyanasundaram, K., Roveri, M.: Tighter integration of BDDs and SMT for Predicate Abstraction. In: Proc. of DATE, pp. 1707\u20131712. IEEE, Los Alamitos (2010)"},{"key":"24_CR12","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)"},{"issue":"5","key":"24_CR13","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"24_CR14","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, Los Alamitos (2005)"},{"key":"24_CR15","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM, New York (2004)"},{"key":"24_CR16","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM, New York (2002)"},{"key":"24_CR17","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":"24_CR18","first-page":"78","volume":"65","author":"G.J. Holzmann","year":"2005","unstructured":"Holzmann, G.J.: Software model checking with SPIN. Advances in Computers\u00a065, 78\u2013109 (2005)","journal-title":"Advances in Computers"},{"key":"24_CR19","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, Los Alamitos (2005)"},{"key":"24_CR20","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, Los Alamitos (2005)"},{"key":"24_CR21","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":"24_CR22","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, Los Alamitos (2008)"},{"key":"24_CR23","first-page":"123","volume-title":"MEMOCODE","author":"D. Tabakov","year":"2010","unstructured":"Tabakov, D., Vardi, M.Y.: Monitoring Temporal SystemC Properties. In: MEMOCODE, pp. 123\u2013132. IEEE, Los Alamitos (2010)"},{"key":"24_CR24","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","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T23:16:48Z","timestamp":1686179808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}