{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,20]],"date-time":"2023-08-20T16:53:35Z","timestamp":1692550415525},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,12,20]],"date-time":"2013-12-20T00:00:00Z","timestamp":1387497600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10009-013-0297-7","type":"journal-article","created":{"date-parts":[[2013,12,19]],"date-time":"2013-12-19T07:06:45Z","timestamp":1387436805000},"page":"123-125","source":"Crossref","is-referenced-by-count":1,"title":["Developments in automated verification techniques"],"prefix":"10.1007","volume":"16","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,20]]},"reference":[{"issue":"1","key":"297_CR1","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"297_CR2","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-013-0276-z","DOI":"10.1007\/s10009-013-0276-z"},{"key":"297_CR3","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In Proceedings of CONCUR \u201992, pp. 123\u2013137. Springer, LNCS 630 (1992)","DOI":"10.1007\/BFb0084787"},{"key":"297_CR4","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Pushdown processes: parallel composition and model checking. In: Proceedings of CONCUR \u201994, pp. 98\u2013113. Springer, LNCS 836 (1994)","DOI":"10.1007\/978-3-540-48654-1_9"},{"issue":"1","key":"297_CR5","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":"297_CR6","doi-asserted-by":"crossref","unstructured":"Cox, A., Sankaranarayanan, S., Evan Chang, B.-Y.: A bit too precise? Verification of quantized digital filters. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-013-0279-9","DOI":"10.1007\/s10009-013-0279-9"},{"key":"297_CR7","doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Proceedings of TACAS \u201906, pp. 287\u2013302. Springer, LNCS 3920 (2006)","DOI":"10.1007\/11691372_19"},{"key":"297_CR8","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Proceedings of CAV \u201900, pp. 232\u2013247. Springer, LNCS 1855 (2000)","DOI":"10.1007\/10722167_20"},{"key":"297_CR9","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"297_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of POPL \u201904, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/964001.964021"},{"key":"297_CR11","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-013-0289-7","DOI":"10.1007\/s10009-013-0289-7"},{"key":"297_CR12","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In Proceedings of TACAS \u201905, pp. 93\u2013107. Springer, LNCS 3440 (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"297_CR13","doi-asserted-by":"crossref","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74 (1953)","DOI":"10.2307\/1990888"},{"issue":"3","key":"297_CR14","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS (ACM Trans. Program. Lang. Syst.) 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS (ACM Trans. Program. Lang. Syst.)"},{"key":"297_CR15","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pushdown model-checking for malware detection. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-013-0290-1","DOI":"10.1007\/s10009-013-0290-1"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0297-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0297-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0297-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,5]],"date-time":"2019-08-05T00:34:52Z","timestamp":1564965292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0297-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,20]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["297"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0297-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,20]]}}}