{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T10:24:30Z","timestamp":1648981470289},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,1]],"date-time":"2014-08-01T00:00:00Z","timestamp":1406851200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10009-014-0335-0","type":"journal-article","created":{"date-parts":[[2014,7,31]],"date-time":"2014-07-31T07:56:01Z","timestamp":1406793361000},"page":"519-529","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Applying symbolic bounded model checking to the 2012 RERS greybox challenge"],"prefix":"10.1007","volume":"16","author":[{"given":"Jeremy","family":"Morse","sequence":"first","affiliation":[]},{"given":"Lucas","family":"Cordeiro","sequence":"additional","affiliation":[]},{"given":"Denis","family":"Nicole","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Fischer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,1]]},"reference":[{"key":"335_CR1","first-page":"95","volume":"7241","author":"T Babiak","year":"2012","unstructured":"Babiak, T., Kr\u0306et\u00ednsk\u00fd, M., Reh\u00e1k, V., Strejc\u0306ek, J.: LTL to B\u00fcchi Automata translation: fast and more deterministic. TACAS, LNCS 7241, 95\u2013109 (2012)","journal-title":"TACAS, LNCS"},{"key":"335_CR2","first-page":"881","volume":"215","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Haslum, P.: LTL goal specifications revisited. ECAI\u201910 Front. Artif. Intell. Appl. 215, 881\u2013886 (2010)","journal-title":"ECAI\u201910 Front. Artif. Intell. Appl."},{"issue":"3","key":"335_CR3","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"335_CR4","first-page":"174","volume":"5505","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. TACAS, LNCS 5505, 174\u2013177 (2009)","journal-title":"TACAS, LNCS"},{"key":"335_CR5","doi-asserted-by":"crossref","unstructured":"Chai, M., Li, X., Zhao, L.: Runtime verification based on 4-valued past time LTL. In: Intl. Conf. Computer Science and Information Processing, pp. 567\u2013570 (2012)","DOI":"10.1109\/CSIP.2012.6308917"},{"key":"335_CR6","first-page":"168","volume":"2988","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. TACAS, LNCS 2988, 168\u2013176 (2004)","journal-title":"TACAS, LNCS"},{"key":"335_CR7","first-page":"639","volume":"13","author":"E Clarke","year":"2007","unstructured":"Clarke, E., Lerda, F.: Model checking: software and beyond. J. Univ. Computer Sci. 13, 639\u2013649 (2007)","journal-title":"J. Univ. Computer Sci."},{"key":"335_CR8","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE, pp. 331\u2013340 (2011)","DOI":"10.1145\/1985793.1985839"},{"issue":"4","key":"335_CR9","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"335_CR10","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-bounded model checking with ESBMC 1.17. TACAS, LNCS 7214, 533\u2013536 (2012)","DOI":"10.1007\/978-3-642-28756-5_42"},{"key":"335_CR11","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: An efficient SMT solver:Z3. TACAS, LNCS 4963, 337\u2013340 (2008)"},{"key":"335_CR12","first-page":"53","volume":"2102","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. CAV, LNCS 2102, 53\u201365 (2001)","journal-title":"CAV, LNCS"},{"key":"335_CR13","volume-title":"The SPIN Model Checker\u2014Primer and Reference Manual","author":"G Holzmann","year":"2004","unstructured":"Holzmann, G.: The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"issue":"3","key":"335_CR14","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods Syst. Design 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Design"},{"key":"335_CR15","first-page":"657","volume":"83","author":"L Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic? Inf. Process. 83, 657\u2013668 (1983)","journal-title":"Inf. Process."},{"key":"335_CR16","doi-asserted-by":"crossref","unstructured":"Li, X., Chai, M., Zhao, L., Tang, T., Xu, T.: Safety monitoring for ETCS with 4-valued LTL. In: Intl. Symposium Autonomous Decentralized Systems, pp. 86\u201391 (2011)","DOI":"10.1109\/ISADS.2011.18"},{"key":"335_CR17","first-page":"302","volume":"7041","author":"J Morse","year":"2011","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Context-bounded model checking of LTL properties for ANSI-C software. SEFM, LNCS 7041, 302\u2013317 (2011)","journal-title":"SEFM, LNCS"},{"key":"335_CR18","doi-asserted-by":"crossref","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Model checking LTL properties over ANSI-C programs with bounded traces. J. Softw. Syst. Model (2013) (Online first)","DOI":"10.1007\/s10270-013-0366-0"},{"key":"335_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"335_CR20","doi-asserted-by":"crossref","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful Brute force attack of the RERS 2012 and 2013 challenges. STTT, this volume (2014)","DOI":"10.1007\/s10009-014-0324-3"},{"key":"335_CR21","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. STTT. doi: 10.1007\/s10009-014-0336-z (2014)","DOI":"10.1007\/s10009-014-0336-z"},{"key":"335_CR22","unstructured":"Visser, W.: Personal communication (2012)"}],"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-014-0335-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0335-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0335-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T07:54:37Z","timestamp":1565682877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0335-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,1]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["335"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0335-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,1]]}}}