{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:08:42Z","timestamp":1759032522742,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"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":["Software Qual J"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s11219-014-9259-x","type":"journal-article","created":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T08:59:48Z","timestamp":1416560388000},"page":"37-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4368-2772","authenticated-orcid":false,"given":"Petr","family":"Bauch","sequence":"first","affiliation":[]},{"given":"Vojt\u011bch","family":"Havel","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,20]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Armando, A., Mantovani, J., & Platania, L. (2006). Bounded model checking of software using SMT solvers instead of SAT solvers. In SPIN, LNCS (Vol. 3925, pp. 146\u2013162). New York: Springer. doi: 10.1007\/11691617_9 .","key":"9259_CR1","DOI":"10.1007\/11691617_9"},{"unstructured":"Barnat, J., & Bauch, P. (2013). Control explicit-data symbolic model checking: An introduction. Technical report, Masaryk University. http:\/\/arxiv.org\/abs\/1303.7379 .","key":"9259_CR2"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Beran, J., Brim, L., Kratochv\u00edla, T., & Ro\u010dkai, P. (2012). Tool chain to support automated formal verification of avionics simulink designs. In FMICS, LNCS (Vol. 7437, pp. 78\u201392). New York: Springer. doi: 10.1007\/978-3-642-32469-7_6 .","key":"9259_CR3","DOI":"10.1007\/978-3-642-32469-7_6"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., et al. (2013). DiVinE 3.0\u2014Explicit-state model-checker for multithreaded C\/C++ programs. In CAV (pp. 863\u2013868). doi: 10.1007\/978-3-642-39799-8_60 .","key":"9259_CR4","DOI":"10.1007\/978-3-642-39799-8_60"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Bauch, P., & Havel, V. (2014). Temporal verification of simulink diagrams. In Proceedings of the HASE (pp. 81\u201388). doi: 10.1109\/HASE.2014.20 .","key":"9259_CR5","DOI":"10.1109\/HASE.2014.20"},{"unstructured":"Barrett, C., Stump, A., & Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. Technical report, The University of Iowa.","key":"9259_CR6"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the DAC (pp. 317\u2013320). ACM. doi: 10.1145\/309847.309942 .","key":"9259_CR7","DOI":"10.1145\/309847.309942"},{"doi-asserted-by":"crossref","unstructured":"Bradley, A. (2011). SAT-based model checking without unrolling. In VMCAI (pp. 70\u201387). doi: 10.1007\/978-3-642-18275-4_7 .","key":"9259_CR8","DOI":"10.1007\/978-3-642-18275-4_7"},{"unstructured":"Braione, P., Denaro, G., K\u0159ena, B., & Pezz\u00e8, M. (2008). Verifying LTL properties of bytecode with symbolic execution. In Proceedings of the bytecode (pp. 1\u201314). Elsevier Science.","key":"9259_CR9"},{"issue":"2","key":"9259_CR10","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R Bryant","year":"1991","unstructured":"Bryant, R. (1991). On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2), 205\u2013213. doi: 10.1109\/12.73590 .","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"crossref","unstructured":"Bryant, R., & Chen, Y. A. (1995). Verification of arithmetic circuits with binary moment diagrams. In Proceedings of the DAC (pp. 535\u2013541). doi: 10.1145\/217474.217583 .","key":"9259_CR11","DOI":"10.1145\/217474.217583"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., & Pugh, W. (1997). Symbolic model checking of infinite state systems using presburger arithmetic. In CAV, LNCS (Vol. 1254, pp. 400\u2013411). New York: Springer. doi: 10.1007\/3-540-63166-6_39 .","key":"9259_CR12","DOI":"10.1007\/3-540-63166-6_39"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., & League, C. (1998). Verifying systems with integer constraints and Boolean predicates: A composite approach. In Proceedings of the ISSTA (pp. 113\u2013123). doi: 10.1145\/271771.271799 .","key":"9259_CR13","DOI":"10.1145\/271771.271799"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., et al. (2002). NuSMV 2: An OpenSource tool for symbolic model checking. In CAV (pp. 241\u2013268). doi: 10.1007\/3-540-45657-0_29 .","key":"9259_CR14","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"2","key":"9259_CR15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., & Sistla, A. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 244\u2013263. doi: 10.1145\/5397.5399 .","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., & Cousot, R. (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the POPL (pp. 238\u2013252). ACM. doi: 10.1145\/512950.512973 .","key":"9259_CR16","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"de Moura, L., & Bj\u00f8rner, N. (2008). Z3: An efficient SMT solver. In TACAS, LNCS (Vol. 4963, pp. 337\u2013340). New York: Springer. doi: 10.1007\/978-3-540-78800-3_24 .","key":"9259_CR29","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Klai, K., Poitrenaud, D., & Thierry-Mieg, Y. (2011). Self-loop aggregation product\u2014A new hybrid approach to on-the-fly LTL model checking. In ATVA, LNCS (Vol. 6996, pp. 336\u2013350). New York: Springer. doi: 10.1007\/978-3-642-24372-1_24 .","key":"9259_CR17","DOI":"10.1007\/978-3-642-24372-1_24"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P. (2003) Reasoning about abstract open systems with generalized module checking. In EMSOFT, LNCS (Vol. 2855, pp. 223\u2013240). Springer. doi: 10.1007\/978-3-540-45212-6_15 .","key":"9259_CR18","DOI":"10.1007\/978-3-540-45212-6_15"},{"doi-asserted-by":"crossref","unstructured":"Hagen, G., & Tinelli, C. (2008). Scaling up the formal verification of lustre programs with SMT-based techniques. In Proceedings of the FMCAD (pp. 1\u20139). doi: 10.1109\/FMCAD.2008.ECP.19 .","key":"9259_CR19","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"issue":"9","key":"9259_CR20","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., & Pilaud, D. (1991). The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79(9), 1305\u20131320. doi: 10.1109\/5.97300 .","journal-title":"Proceedings of the IEEE"},{"doi-asserted-by":"crossref","unstructured":"Hungar, H., Grumberg, O., & Damm, W. (1995). What if model checking must be truly symbolic. In CHARME, LNCS (Vol. 987, pp. 1\u201320). New York: Springer. doi: 10.1007\/3-540-60385-9_1 .","key":"9259_CR21","DOI":"10.1007\/3-540-60385-9_1"},{"issue":"7","key":"9259_CR22","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J King","year":"1976","unstructured":"King, J. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385\u2013394. doi: 10.1145\/360248.360252 .","journal-title":"Communications of the ACM"},{"key":"9259_CR23","volume-title":"Decision procedures: An algorithmic point of view","author":"D Kroening","year":"2010","unstructured":"Kroening, D., & Strichman, O. (2010). Decision procedures: An algorithmic point of view. New York: Springer."},{"doi-asserted-by":"crossref","unstructured":"Kupferman, O., & Vardi, M. (1996). Module checking. In CAV, LNCS (Vol. 1102, pp. 75\u201386). New York: Springer. doi: 10.1007\/3-540-61474-5_59 .","key":"9259_CR24","DOI":"10.1007\/3-540-61474-5_59"},{"doi-asserted-by":"crossref","unstructured":"Lin, H. (1996). Symbolic transition graph with assignment. In CONCUR, LNCS (Vol. 1119, pp. 50\u201365). New York: Springer. doi: 10.1007\/3-540-61604-7_47 .","key":"9259_CR25","DOI":"10.1007\/3-540-61604-7_47"},{"unstructured":"McMillan, K. (1992). Symbolic model checking. Ph.D. thesis, Carnegie Mellon University.","key":"9259_CR26"},{"doi-asserted-by":"crossref","unstructured":"Meenakshi, B., Bhatnagar, A., & Roy, S. (2006). Tool for translating simulink models into input language of a model checker. In ICFEM, LNCS (Vol. 4260, pp. 606\u2013620). New York: Springer. doi: 10.1007\/11901433_33 .","key":"9259_CR27","DOI":"10.1007\/11901433_33"},{"doi-asserted-by":"crossref","unstructured":"Miller, S., Anderson, E., Wagner, L., Whalen, M., & Heimdahl, M. (2005). Formal verification of flight critical software. In Proceedings of the GNC (pp. 1\u201316).","key":"9259_CR28","DOI":"10.2514\/6.2005-6431"},{"key":"9259_CR30","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., & Gries, D. (1976). An axiomatic proof technique for parallel programs I. Acta Informatica, 6, 319\u2013340. doi: 10.1007\/BF00268134 .","journal-title":"Acta Informatica"},{"doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S., & Vardi, M. (2005). Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking. In CAV, LNCS (Vol. 3576, pp. 100\u2013246). New York: Springer. doi: 10.1007\/11513988_35 .","key":"9259_CR31","DOI":"10.1007\/11513988_35"},{"unstructured":"Vardi, M., & Wolper, P. (1986). An automata\u2014theoretic approach to automatic program verification. In Proceedings of the LICS (pp. 332\u2013344). IEEE Computer Society Press.","key":"9259_CR32"},{"doi-asserted-by":"crossref","unstructured":"Williams, P., Biere, A., Clarke, E., & Gupta, A. (2000). Combining decision diagrams and SAT procedures for efficient symbolic model checking. In CAV, LNCS (Vol. 1855, pp. 124\u2013138). New York: Springer. doi: 10.1007\/10722167_13 .","key":"9259_CR33","DOI":"10.1007\/10722167_13"},{"issue":"1","key":"9259_CR34","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"C Wintersteiger","year":"2013","unstructured":"Wintersteiger, C., Hamadi, Y., & de Moura, L. (2013). Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 42(1), 3\u201323. doi: 10.1007\/s10703-012-0156-2 .","journal-title":"Formal Methods in System Design"},{"doi-asserted-by":"crossref","unstructured":"Xie, T., Marinov, D., Schulte, W., & Notkin, D. (2005). Symstra: A framework for generating object-oriented unit tests using symbolic execution. In TACAS, LNCS (Vol. 3440, pp. 365\u2013381). New York: Springer. doi: 10.1007\/978-3-540-31980-1_24 .","key":"9259_CR35","DOI":"10.1007\/978-3-540-31980-1_24"},{"doi-asserted-by":"crossref","unstructured":"Yang, Z., Wang, C., Gupta, A., & Ivan\u010di\u0107, F. (2006). Mixed symbolic representations for model checking software programs. In Proceedings of the MEMOCODE (pp. 17\u201326). doi: 10.1109\/MEMCOD.2006.1695896 .","key":"9259_CR36","DOI":"10.1109\/MEMCOD.2006.1695896"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-014-9259-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11219-014-9259-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-014-9259-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T06:10:42Z","timestamp":1559369442000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11219-014-9259-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,20]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["9259"],"URL":"https:\/\/doi.org\/10.1007\/s11219-014-9259-x","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2014,11,20]]}}}