{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T04:48:51Z","timestamp":1764305331129,"version":"3.40.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,19]],"date-time":"2014-08-19T00:00:00Z","timestamp":1408406400000},"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-0334-1","type":"journal-article","created":{"date-parts":[[2014,8,18]],"date-time":"2014-08-18T15:33:58Z","timestamp":1408376038000},"page":"507-518","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["BDD-based software verification"],"prefix":"10.1007","volume":"16","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Stahlbauer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,19]]},"reference":[{"key":"334_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, R.J., Beame, P., Burns, S., Chan, W., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. In: Proc. FSE, pp. 156\u2013166. ACM (1996)","DOI":"10.1145\/250707.239127"},{"key":"334_CR2","doi-asserted-by":"crossref","unstructured":"Apel, S., Beyer, D., Friedberger, K., Raimondi, F., Rhein, A.V.: Domain types: Abstract-domain selection based on variable usage. In: Proc. HVC, LNCS 8244, pp. 262\u2013278. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03077-7_18"},{"key":"334_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking C programs. In: Proc. TACAS, LNCS 2031, pp. 268\u2013283. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45319-9_19"},{"key":"334_CR4","doi-asserted-by":"crossref","unstructured":"Berndl, M., Lhot\u00e1k, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: Proc. PLDI, pp. 103\u2013114. ACM (2003)","DOI":"10.1145\/780822.781144"},{"key":"334_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Proc. FME, LNCS 2021, pp. 318\u2013343. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45251-6_18"},{"key":"334_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Relational programming with CrocoPat. In: Proc. ICSE, pp. 807\u2013810. ACM (2006)","DOI":"10.1145\/1134285.1134420"},{"key":"334_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software verification. In: Proc. TACAS, LNCS 7795, pp. 594\u2013609. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"334_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Status report on software verification. In: Proc. TACAS, LNCS 8413, pp. 373\u2013388. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"334_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proc. FMCAD, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"issue":"5\u20136","key":"334_CR10","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"334_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T. A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS 4590, pp. 504\u2013518. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"334_CR12","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T. A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29\u201338. IEEE (2008)","DOI":"10.1109\/ASE.2008.13"},{"key":"334_CR13","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M. E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV, LNCS 6806, pp. 184\u2013190. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"334_CR14","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"334_CR15","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Proc. CAV, LNCS 2725, pp. 122\u2013125. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_13"},{"key":"334_CR16","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE, LNCS 7793, pp. 146\u2013162. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"334_CR17","doi-asserted-by":"crossref","unstructured":"Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real-time verification? In: Proc. FORTE, LNCS 2767, pp. 193\u2013208. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39979-7_13"},{"key":"334_CR18","doi-asserted-by":"crossref","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Proc. MEMICS, LNCS 7721, pp. 1\u201311. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36046-6_1"},{"key":"334_CR19","unstructured":"Beyer, D., Wendler, P.: Algorithms for software model checking: Predicate abstraction vs. Impact. In: Proc. FMCAD, pp. 106\u2013113. FMCAD (2012)"},{"key":"334_CR20","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS, LNCS 1579, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"334_CR21","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Proc. CAV, LNCS 6174, pp. 354\u2013359. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"issue":"9","key":"334_CR22","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"334_CR23","doi-asserted-by":"crossref","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine. S.: Kronos: A model-checking tool for real-time systems. In: Proc. CAV, LNCS 1427, pp. 546\u2013550. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028779"},{"key":"334_CR24","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8):677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"334_CR25","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"RE Bryant","year":"1991","unstructured":"Bryant, R.E.: On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205\u2013213 (1991)","journal-title":"IEEE Trans. Comput."},{"key":"334_CR26","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Proc. DAC, pp. 46\u201351. ACM (1990)","DOI":"10.1145\/123186.123223"},{"key":"334_CR27","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. In: Proc. LICS, pp. 428\u2013439. IEEE (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"334_CR28","doi-asserted-by":"crossref","unstructured":"Campos, S.V.A., Clarke, E.M.: The Verus language: representing time efficiently with BDDs. In: Proc. ARTS, LNCS 1231, pp. 64\u201378. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63010-4_5"},{"key":"334_CR29","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An open-source tool for symbolic model checking. In: Proc. CAV, LNCS 2404, pp. 359\u2013364. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"334_CR30","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proc. CAV, LNCS 1633, pp. 495\u2013499. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"334_CR31","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos: A software model checker for SystemC. In: Proc. CAV, LNCS 6806, pp. 310\u2013316. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"334_CR32","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS, LNCS 7795, pp. 93\u2013107. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"5","key":"334_CR33","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":"3","key":"334_CR34","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand\u2013Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"334_CR35","unstructured":"Esparza, J.: Building a software model checker. In: Proc. Formal logical methods for system security and correctness, pp. 53\u201387. IOS Press (2008)"},{"key":"334_CR36","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Proc. TACAS, LNCS 3920, pp. 489\u2013503. Springer, Berlin (2006)","DOI":"10.1007\/11691372_35"},{"key":"334_CR37","doi-asserted-by":"crossref","unstructured":"Henzinger, T. A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/964001.964021"},{"key":"334_CR38","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"334_CR39","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: Analysis of event\u2013condition\u2013action systems. In: Proc. ISoLA, LNCS 7609, pp. 608\u2013614. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"334_CR40","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., P\u0103s\u0103reanu, C.S.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Int. J. Softw. Tools Technol. Transfer. doi: 10.1007\/s10009-014-0337-y (2014)","DOI":"10.1007\/s10009-014-0337-y"},{"key":"334_CR41","doi-asserted-by":"crossref","unstructured":"Ivanc\u0306i\u0107, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: Proc. ICCD, pp. 297\u2013308. IEEE (2005)","DOI":"10.1109\/ICCD.2005.77"},{"issue":"3","key":"334_CR42","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1016\/S1571-0661(05)80008-8","volume":"89","author":"F Lerda","year":"2003","unstructured":"Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electr. Notes Theor. Comput. Sci. 89(3), 480\u2013498 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"334_CR43","unstructured":"McMillan, K.L.: The SMV system. Technical Report CMU-CS-92-131. Carnegie Mellon University (1992)"},{"key":"334_CR44","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV, LNCS 4144, pp. 123\u2013136. Springer, Berlin (2006)","DOI":"10.1007\/11817963_14"},{"key":"334_CR45","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC, LNCS 2304, pp. 213\u2013228. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"334_CR46","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Proc. SPIN, LNCS 7976, pp. 341\u2013357. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"key":"334_CR47","doi-asserted-by":"crossref","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. doi: 10.1007\/s10009-014-0336-z (2014)","DOI":"10.1007\/s10009-014-0336-z"},{"key":"334_CR48","unstructured":"von Rhein, A., Apel, S., Raimondi, F.: Introducing binary decision diagrams in the explicit-state verification of Java code. In: Proceedings of Java Pathfinder Workshop (2011)"}],"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-0334-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0334-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0334-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T07:50:06Z","timestamp":1746345006000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0334-1"}},"subtitle":["Applications to event-condition-action systems"],"short-title":[],"issued":{"date-parts":[[2014,8,19]]},"references-count":48,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["334"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0334-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,8,19]]}}}