{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T11:54:40Z","timestamp":1716465280760},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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":[[2022,6]]},"DOI":"10.1007\/s10009-022-00659-x","type":"journal-article","created":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T15:26:27Z","timestamp":1648826787000},"page":"493-510","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["DivSIM , an interactive simulator for LLVM bitcode"],"prefix":"10.1007","volume":"24","author":[{"given":"Petr","family":"Ro\u010dkai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,4,1]]},"reference":[{"issue":"8","key":"659_CR1","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Inform. 54(8), 789\u2013818 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0275-0","journal-title":"Acta Inform."},{"key":"659_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97\u2013105. ACM (2003)","DOI":"10.1145\/640128.604140"},{"key":"659_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: IFM, LNCS. Springer (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"659_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Beran, J., Brim, L., Kratochv\u00edla, T., Ro\u010dkai, P.: Tool chain to support automated formal verification of avionics Simulink designs. In: FMICS, number 7437 in LNCS, pp. 78\u201392. Springer (2012)","DOI":"10.1007\/978-3-642-32469-7_6"},{"key":"659_CR5","unstructured":"Basu, S., Saha, D., Smolka, S.A.: Getting to the root of the problem: focus statements for the analysis of counter-examples (2012)"},{"key":"659_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"659_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"659_CR8","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Ja\u0161ek, T., Tomovi\u010d, L., Hru\u0161ka, M., \u0160okov\u00e1, V., Ayaziov\u00e1, P., Strej\u010dek, J., Vojnar, T.: Symbiotic 7: Integration of predator and more. In: TACAS, pp. 413\u2013417. Springer, Cham (2020). ISBN 978-3-030-45237-7","DOI":"10.1007\/978-3-030-45237-7_31"},{"key":"659_CR9","doi-asserted-by":"crossref","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Computer Aided Verification, LNCS, pp. 453\u2013456. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"659_CR10","doi-asserted-by":"publisher","unstructured":"G\u00fcnther, H., Laarman, A., Weissenbacher, G.: Vienna Verification Tool: IC3 for parallel software (competition contribution). In: TACAS, pp. 954\u2013957 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_69","DOI":"10.1007\/978-3-662-49674-9_69"},{"key":"659_CR11","unstructured":"Kleiman, R., Brayshaw, M., Eisenstadt, M., Eisenstadt, M.: Tales of debugging from the front lines (1993)"},{"key":"659_CR12","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In PLDI, PLDI, pp. 96\u201310, New York, 2019. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","DOI":"10.1145\/3314221.3314609"},{"key":"659_CR13","doi-asserted-by":"crossref","unstructured":"Lauko, H., Ro\u010dkai, P., Barnat, J.: Symbolic computation via program transformation. In: Theoretical Aspects of Computing\u2014ICTAC, pp. 313\u2013332. Springer, Cham (2018)","DOI":"10.1007\/978-3-030-02508-3_17"},{"key":"659_CR14","doi-asserted-by":"crossref","unstructured":"Lauko, H., \u0160till, V., Ro\u010dkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: TACAS, pp. 204\u2013208. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-17502-3_14"},{"key":"659_CR15","doi-asserted-by":"crossref","unstructured":"Lee, K.: Using LLDB, pp. 415\u2013434. Apress, Berkeley, CA (2013). ISBN 978-1-4302-5051-7","DOI":"10.1007\/978-1-4302-5051-7_21"},{"key":"659_CR16","doi-asserted-by":"crossref","unstructured":"Legay, A., Nowotka, D., Poulsen, D.B., Tranouez, L.-M.: Statistical model checking of llvm code. In: Formal Methods, pp. 542\u2013549. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-95582-7_32"},{"key":"659_CR17","doi-asserted-by":"crossref","unstructured":"Magee, J.: Behavioral analysis of software architectures using LTSA. In: ICSE (1999)","DOI":"10.1145\/302405.302726"},{"key":"659_CR18","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007)","DOI":"10.1145\/1250734.1250746"},{"key":"659_CR19","doi-asserted-by":"crossref","unstructured":"Ro\u010dkai, P., Barnat, J.: A simulator for llvm bitcode. In: Formal Methods for Industrial Critical Systems, pp. 127\u2013142. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-27008-7_8"},{"key":"659_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2018.04.026","volume":"143","author":"P Ro\u010dkai","year":"2018","unstructured":"Ro\u010dkai, P., \u0160till, V., \u010cern\u00e1, I., Barnat, J.: DiVM: model checking with LLVM and graph memory. J. Syst. Softw. 143, 1\u201313 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.04.026","journal-title":"J. Syst. Softw."},{"key":"659_CR21","doi-asserted-by":"publisher","unstructured":"Ro\u010dkai, P., Baranov\u00e1, Z., Mr\u00e1zek, J., Kejstov\u00e1, K., Barnat, J.: Reproducible execution of POSIX programs with DiOS. Software and Systems Modeling, pp. 1\u201320, 10 (2020). https:\/\/doi.org\/10.1007\/s10270-020-00837-y","DOI":"10.1007\/s10270-020-00837-y"},{"key":"659_CR22","unstructured":"Stallman, R., Pesch, R., Shebs, S.: Debugging with gdb (2010)"},{"key":"659_CR23","unstructured":"The LLVM Project. LLVM language reference manual (2016). http:\/\/llvm.org\/docs\/LangRef.html"},{"key":"659_CR24","doi-asserted-by":"crossref","unstructured":"Visan, A.-M., Arya, K.: Gene Cooperman, and Tyler Denniston. URDB: a universal reversible debugger based on decomposing debugging histories. In: PLOS \u201911 (2011)","DOI":"10.1145\/2039239.2039251"},{"key":"659_CR25","doi-asserted-by":"crossref","unstructured":"Visser, W., Groce, A.: What went wrong: Explaining counterexamples. In: SPIN, LNCS, pp. 121\u2013135. Springer (2002)","DOI":"10.1007\/3-540-44829-2_8"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00659-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00659-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00659-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,11]],"date-time":"2022-05-11T10:09:44Z","timestamp":1652263784000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00659-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["659"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00659-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]},"assertion":[{"value":"9 March 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 April 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}