{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T15:07:44Z","timestamp":1790262464163,"version":"4.1.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"9","license":[{"start":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T00:00:00Z","timestamp":1283299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2010,9]]},"abstract":"<jats:p>A call for the perfect marriage between classical performance evaluation and state-of-the-art verification techniques.<\/jats:p>","DOI":"10.1145\/1810891.1810912","type":"journal-article","created":{"date-parts":[[2010,8,31]],"date-time":"2010-08-31T13:05:55Z","timestamp":1283259955000},"page":"76-85","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Performance evaluation and model checking join forces"],"prefix":"10.1145","volume":"53","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[{"name":"TU Dresden, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Boudewijn R.","family":"Haverkort","sequence":"additional","affiliation":[{"name":"Embedded Systems Institute, Eindhoven, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.008"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/190.191"},{"key":"e_1_2_1_3_1","first-page":"88","article-title":"-P. Discrete-time rewards model-checked. FORMATS","volume":"2791","author":"Andova S.","year":"2003","unstructured":"Andova , S. , Hermanns , H. , and Katoen , J . -P. Discrete-time rewards model-checked. FORMATS , LNCS 2791 , ( 2003 ), 88 -- 104 . Andova, S., Hermanns, H., and Katoen, J.-P. Discrete-time rewards model-checked. FORMATS, LNCS 2791, (2003), 88--104.","journal-title":"LNCS"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.30"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_7_1","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"Baier , C. and Katoen , J-P . Principles of Model Checking . MIT Press , 2008 . Baier, C. and Katoen, J-P. Principles of Model Checking. MIT Press, 2008."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646833.708042"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Intl. Conf. on Dependable Systems and Networks. IEEE CS Press.","author":"Bohnenkamp H.","year":"2003","unstructured":"Bohnenkamp , H. , van der Stok , P. , Hermanns , H. , and Vaandrager , F.W . Cost optimisation of the IPv4 zeroconf protocol . In Proceedings of the Intl. Conf. on Dependable Systems and Networks. IEEE CS Press. 2003 , 531--540. Bohnenkamp, H., van der Stok, P., Hermanns, H., and Vaandrager, F.W. Cost optimisation of the IPv4 zeroconf protocol. In Proceedings of the Intl. Conf. on Dependable Systems and Networks. IEEE CS Press. 2003, 531--540."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/289350"},{"key":"e_1_2_1_11_1","volume-title":"Model Checking","author":"Clarke E.M.","year":"1999","unstructured":"Clarke , E.M. , Grumberg , O. , and Peled , D . Model Checking . MIT Press , 1999 . Clarke, E.M., Grumberg, O., and Peled, D. Model Checking. MIT Press, 1999."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNANO.2007.911319"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_15_1","first-page":"335","article-title":"Reduction and refinement strategies for probabilistic analysis","volume":"2399","author":"D'Argenio P.R.","year":"2002","unstructured":"D'Argenio , P.R. Jeannet , B. , Jensen , H. , and Larsen , K.G . Reduction and refinement strategies for probabilistic analysis . LNCS 2399 ( 2002 ), 335 -- 372 . D'Argenio, P.R. Jeannet, B., Jensen, H., and Larsen, K.G. Reduction and refinement strategies for probabilistic analysis. LNCS 2399 (2002), 335--372.","journal-title":"LNCS"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00343-0"},{"key":"e_1_2_1_17_1","first-page":"3","article-title":"Counter-examples in probabilistic model checking","volume":"36","author":"Han Y.","year":"2010","unstructured":"Han , Y. , Katoen , J.-P. and Damman , B . Counter-examples in probabilistic model checking . IEEE TSE 36 , 3 ( 2010 ), 390--408. Han, Y., Katoen, J.-P. and Damman, B. Counter-examples in probabilistic model checking. IEEE TSE 36, 3 (2010), 390--408.","journal-title":"IEEE TSE"},{"key":"e_1_2_1_18_1","first-page":"5","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson H.","year":"1994","unstructured":"Hansson , H. and Jonsson , B . A logic for reasoning about time and reliability . Formal Aspects of Comp. 6 , 5 ( 1994 ), 512--535. Hansson, H. and Jonsson, B. A logic for reasoning about time and reliability. Formal Aspects of Comp. 6, 5 (1994), 512--535.","journal-title":"Formal Aspects of Comp."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_20_1","unstructured":"www.prismmodelchecker.org.  www.prismmodelchecker.org."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_2_1_22_1","volume-title":"The Art of Computer System Performance Analysis","author":"Jain R.","year":"1991","unstructured":"Jain , R. The Art of Computer System Performance Analysis . Wiley , 1991 . Jain, R. The Art of Computer System Performance Analysis. Wiley, 1991."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_23"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"key":"e_1_2_1_26_1","volume-title":"Symbolic Systems Biology","author":"Kwiatkowska M.Z.","year":"2010","unstructured":"Kwiatkowska , M.Z. , Norman , G. , and Parker , D . Probabilistic model checking for systems biology . Symbolic Systems Biology , 2010 . Kwiatkowska, M.Z., Norman, G., and Parker, D. Probabilistic model checking for systems biology. Symbolic Systems Biology, 2010."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_28_1","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver A.","year":"2005","unstructured":"McIver , A. and Morgan , C . Abstraction, Refinement and Proof for Probabilistic Systems . Springer , 2005 . McIver, A. and Morgan, C. Abstraction, Refinement and Proof for Probabilistic Systems. Springer, 2005."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_9"},{"key":"e_1_2_1_30_1","first-page":"296","article-title":"Symbolic representation and analysis of large probabilistic systems. Validation of Stochastic Systems. A Guide to Current Research","volume":"2925","author":"Miner A.","year":"2005","unstructured":"Miner , A. and Parker , D . Symbolic representation and analysis of large probabilistic systems. Validation of Stochastic Systems. A Guide to Current Research . LNCS 2925 ( 2005 ), 296 -- 338 . Miner, A. and Parker, D. Symbolic representation and analysis of large probabilistic systems. Validation of Stochastic Systems. A Guide to Current Research. LNCS 2925 (2005), 296--338.","journal-title":"LNCS"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0062-0"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.3"},{"key":"e_1_2_1_33_1","first-page":"1","article-title":"Reduced base model construction methods for stochastic activity networks","volume":"9","author":"Sanders W.H.","year":"1991","unstructured":"Sanders , W.H. and Meyer , J.F . Reduced base model construction methods for stochastic activity networks . IEEE J. on Selected Areas in Comms. 9 , 1 ( 1991 ), 25--36. Sanders, W.H. and Meyer, J.F. Reduced base model construction methods for stochastic activity networks. IEEE J. on Selected Areas in Comms. 9, 1 (1991), 25--36.","journal-title":"IEEE J. on Selected Areas in Comms."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1297352.1297359"},{"key":"e_1_2_1_35_1","first-page":"3","article-title":"Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol","volume":"14","author":"Stoelinga M","year":"2003","unstructured":"Stoelinga , M . Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol . Formal Asp. Comp. , 14 , 3 ( 2003 ), 328--337. Stoelinga, M. Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Asp. Comp., 14, 3 (2003), 328--337.","journal-title":"Formal Asp. Comp."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1810891.1810912","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1810891.1810912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:23:01Z","timestamp":1750245781000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1810891.1810912"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":36,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["10.1145\/1810891.1810912"],"URL":"https:\/\/doi.org\/10.1145\/1810891.1810912","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9]]},"assertion":[{"value":"2010-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}