{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T09:56:58Z","timestamp":1725875818509},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319516400"},{"type":"electronic","value":"9783319516417"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-51641-7_9","type":"book-chapter","created":{"date-parts":[[2016,12,21]],"date-time":"2016-12-21T07:11:03Z","timestamp":1482304263000},"page":"143-155","source":"Crossref","is-referenced-by-count":2,"title":["Counterexample-Guided Prefix Refinement Analysis for Program Verification"],"prefix":"10.1007","author":[{"given":"Marc","family":"Jasper","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,12,22]]},"reference":[{"key":"9_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., et al.: Principles of Model Checking, vol. 26202649. MIT Press, Cambridge (2008)"},{"issue":"5","key":"9_CR2","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/s10009-014-0333-2","volume":"16","author":"O Bauer","year":"2014","unstructured":"Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Int. J. Softw. Tools Technol. Transfer 16(5), 531\u2013542 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: 23rd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2008, pp. 29\u201338. IEEE (2008)","DOI":"10.1109\/ASE.2008.13"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2013","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 146\u2013162. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37057-1_11"},{"issue":"5","key":"9_CR5","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10009-014-0334-1","volume":"16","author":"D Beyer","year":"2014","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event-condition-action systems. Int. J. Softw. Tools Technol. Transfer 16(5), 507\u2013518 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"5","key":"9_CR6","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM 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 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"1","key":"9_CR7","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Computer Aided Verification","author":"D Dams","year":"1993","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Generation of reduced models for checking fragments of CTL. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 479\u2013490. Springer, Heidelberg (1993). doi: 10.1007\/3-540-56922-7_39"},{"issue":"5","key":"9_CR9","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Int. J. Softw. Tools Technol. Transfer 16(5), 457\u2013464 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Jasper, M.: Counterexample-guided abstraction refinement for the verification of large-scale reactive systems. Bachelor thesis, TU Dortmund University (2015)","DOI":"10.1007\/978-3-319-51641-7_9"},{"issue":"5","key":"9_CR11","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-014-0335-0","volume":"16","author":"J Morse","year":"2014","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS greybox challenge. Int. J. Softw. Tools Technol. Transfer 16(5), 519\u2013529 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"5","key":"9_CR12","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/s10009-014-0324-3","volume":"16","author":"J Pol van de","year":"2014","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful brute-force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 481\u2013491 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"5","key":"9_CR13","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/s10009-014-0338-x","volume":"16","author":"M Schordan","year":"2014","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 493\u2013505 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346\u2013364. Springer, Heidelberg (1991). doi: 10.1007\/3-540-54415-1_54"},{"issue":"5","key":"9_CR15","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465\u2013479 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"}],"container-title":["Communications in Computer and Information Science","Leveraging Applications of Formal Methods, Verification, and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51641-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T17:14:29Z","timestamp":1658250869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51641-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319516400","9783319516417"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51641-7_9","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]}}}