{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T03:50:15Z","timestamp":1754020215642,"version":"3.40.3"},"reference-count":97,"publisher":"Springer Science and Business Media LLC","license":[{"start":{"date-parts":[[2012,8,24]],"date-time":"2012-08-24T00:00:00Z","timestamp":1345766400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"DOI":"10.1007\/s10270-012-0281-9","type":"journal-article","created":{"date-parts":[[2012,8,23]],"date-time":"2012-08-23T00:50:38Z","timestamp":1345683038000},"source":"Crossref","is-referenced-by-count":10,"title":["The hidden models of model checking"],"prefix":"10.1007","author":[{"given":"Willem","family":"Visser","sequence":"first","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,24]]},"reference":[{"key":"281_CR1","unstructured":"Cadence Inc. Incisive Enterprise Simulator product web site. http:\/\/www.cadence.com\/products\/sd\/enterprise_simulator"},{"key":"281_CR2","unstructured":"Mentor Graphics Inc. ModelSim product web site. http:\/\/www.mentor.com\/products\/fv\/modelsim"},{"key":"281_CR3","doi-asserted-by":"crossref","unstructured":"Amla, N., Emerson, A.E., Namjoshi, K.S., Trefler, R.J.: Abstract patterns of compositional reasoning. In: CONCUR, pp. 423\u2013438 (2003)","DOI":"10.1007\/978-3-540-45187-7_28"},{"key":"281_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon,\u00a0H., Finkel, A. (eds.) Proceedings of CAV, Paris, France. LNCS, vol. 2102, pp. 260\u2013264. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"key":"281_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proceedings of the 7th International SPIN Workshop on Model Checking and Software Verification, pp. 113\u2013130 (2000)","DOI":"10.1007\/10722468_7"},{"key":"281_CR6","doi-asserted-by":"crossref","unstructured":"Batt, G., Belta, C., Weiss, R.: Model checking liveness properties of genetic regulatory networks. In: Tools and Algorithms for the Construction and Analysis of Systems, vol. 4424, pp. 323\u2013338. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_25"},{"key":"281_CR7","doi-asserted-by":"crossref","unstructured":"Batt, G., Page, M., Cantone, I., Goessler, G., Monteiro, P.T., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18) (2010)","DOI":"10.1093\/bioinformatics\/btq387"},{"key":"281_CR8","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: Model checking the IBM gigahertz processor: an abstraction algorithm for high-performance netlists. In: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 72\u201383 (1999)","DOI":"10.1007\/3-540-48683-6_9"},{"key":"281_CR9","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods Syst. Des. 18, 141\u2013163 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"281_CR10","unstructured":"Berthomieu, B., Garavel, H., Lang, F., Vernadat, F.: Verifying dynamic properties of industrial critical systems using TOPCASED\/FIACRE. ERCIM News 2008(75) (2008)"},{"key":"281_CR11","unstructured":"Bjesse, P., Boralv, A.: Dag-aware circuit compression for formal verification. In: Proceedings of ICCAD \u201904, pp. 42\u201349 (2004)"},{"key":"281_CR12","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proceedings of the 27th Design Automation Conference, pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"key":"281_CR13","first-page":"534","volume":"1993","author":"D Brand","year":"1993","unstructured":"Brand, D.: Verification of large synthesized designs. Proc. ICCAD 1993, 534\u2013537 (1993)","journal-title":"Proc. ICCAD"},{"key":"281_CR14","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI\u201908, Berkeley, CA, USA, pp. 209\u2013224. USENIX Association (2008)"},{"key":"281_CR15","doi-asserted-by":"crossref","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., P\u01ces\u01cereanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: ICSE, pp. 1066\u20131071 (2011)","DOI":"10.1145\/1985793.1985995"},{"key":"281_CR16","doi-asserted-by":"crossref","unstructured":"Calder, M., Gilmore, S., Hillston, J., Vyshemirsky, V.: Formal methods for biochemical signalling pathways. In: Formal Methods: State of the Art and New Directions, pp. 185\u2013215. Springer, Berlin (2010)","DOI":"10.1007\/978-1-84882-736-3_6"},{"issue":"2","key":"281_CR17","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/32.908961","volume":"27","author":"W Chan","year":"2001","unstructured":"Chan, W., Anderson, R.J., Beame, P., Jones, D.H., Notkin, D., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Trans. Softw. Eng. 27(2), 170\u2013190 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"281_CR18","doi-asserted-by":"crossref","unstructured":"Chan, W., Anderson, R.J., Beame, P., Notkin, D.: Improving efficiency of symbolic model checking for state-based system requirements. In: ISSTA, pp. 102\u2013112 (1998)","DOI":"10.1145\/271775.271798"},{"issue":"4","key":"281_CR19","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/s007660200018","volume":"7","author":"Y Choi","year":"2002","unstructured":"Choi, Y., Rayadurgam, S., Heimdahl, M.P.E.: Toward automation for model-checking requirements specifications with numeric constraints. Requir. Eng. 7(4), 225\u2013242 (2002)","journal-title":"Requir. Eng."},{"key":"281_CR20","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: an open source tool for symbolic model checking. In: Proceedings of the International Conference on Computer-Aided Verification (CAV 2002). Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"281_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Lecture Notes in Computer Science, vol. 2988, pp. 168\u2013176. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"281_CR22","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, A.E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on Logics of Programs, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"281_CR23","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"281_CR24","volume-title":"Grumberg. Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M.: Grumberg. Model Checking. MIT Press, Orna (1999)"},{"key":"281_CR25","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation, pp. 85\u201396 (2004)","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"281_CR26","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Zheng, R., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"281_CR27","doi-asserted-by":"crossref","unstructured":"Darringer, A., Joyner, W.H. Jr., Berman, C.L., Trevillyan, L.: Logic synthesis through local transformations. IBM J. Res. Dev. 25(4), 272\u2013280 (1981)","DOI":"10.1147\/rd.254.0272"},{"key":"281_CR28","doi-asserted-by":"crossref","unstructured":"de Halleux, J., Tillmann, N.: Moles: tool-assisted environment isolation with closures. In: Objects, Models, Components, Patterns, pp. 253\u2013270. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13953-6_14"},{"key":"281_CR29","doi-asserted-by":"crossref","unstructured":"Deng, X., Lee, J., Robby: Bogor\/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE (2006)","DOI":"10.1109\/ASE.2006.26"},{"key":"281_CR30","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"281_CR31","unstructured":"Dwyer, M.B., Corbett, J.C., Avrunin, G.: Spec patterns. http:\/\/patterns.projects.cis.ksu.edu (1999)"},{"key":"281_CR32","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Hatcliff, J., Robby, Ranganath, V.P.: Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2-3), 199\u2013240 (2004)","DOI":"10.1023\/B:FORM.0000040028.49845.67"},{"key":"281_CR33","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Berlin (2006)"},{"key":"281_CR34","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Computer Aided Verification, pp. 232\u2013247 (2000)","DOI":"10.1007\/10722167_20"},{"key":"281_CR35","doi-asserted-by":"crossref","unstructured":"Fisher, J., Henzinger, T., Mateescu, M., Piterman, N.: Bounded asynchrony: concurrency for modeling cell\u2013cell interactions. In: Formal Methods in Systems Biology, pp. 17\u201332. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68413-8_2"},{"issue":"11","key":"281_CR36","doi-asserted-by":"crossref","first-page":"1239","DOI":"10.1038\/nbt1356","volume":"25","author":"J Fisher","year":"2007","unstructured":"Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotechnol. 25(11), 1239\u20131249 (2007)","journal-title":"Nat. Biotechnol."},{"key":"281_CR37","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201905, pp. 110\u2013121. ACM, New York (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"281_CR38","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D., (eds.) Proceedings of the 16th International Conference on Computer Aided Verification, CAV\u201904 (Boston, Massachusetts). Lecture Notes in Computer Science, vol. 3114, pp. 175\u2013188. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"281_CR39","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u01ces\u01cereanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: Proceedings of the 26th International Conference on Software Engineering, pp. 211\u2013220 (2004)","DOI":"10.1109\/ICSE.2004.1317443"},{"key":"281_CR40","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: Proceedings of POPL, pp. 174\u2013186. ACM, New York (1997)","DOI":"10.1145\/263699.263717"},{"key":"281_CR41","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60761-7"},{"issue":"6","key":"281_CR42","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. SIGPLAN Not. 40(6), 213\u2013223 (2005)","journal-title":"SIGPLAN Not."},{"key":"281_CR43","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (NDSS). Internet Society (2008)"},{"key":"281_CR44","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72\u201383. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"281_CR45","doi-asserted-by":"crossref","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with Explain. In: CAV, pp. 453\u2013456 (2004)","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"281_CR46","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: SPIN, pp. 121\u2013135 (2003)","DOI":"10.1007\/3-540-44829-2_8"},{"issue":"4","key":"281_CR47","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A Groce","year":"2004","unstructured":"Groce, A., Visser, W.: Heuristics for model checking Java programs. STTT 6(4), 260\u2013276 (2004)","journal-title":"STTT"},{"key":"281_CR48","doi-asserted-by":"crossref","unstructured":"Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Computer Aided Verification\u201423rd International Conference, Proceedings, pp. 396\u2013411. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_31"},{"key":"281_CR49","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Proceedings of the Formal Methods in Computer-Aided Design, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"issue":"4","key":"281_CR50","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. High. Order Symb. Comput. 13(4), 315\u2013353 (2000)","journal-title":"High. Order Symb. Comput."},{"key":"281_CR51","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder (1998)"},{"issue":"3","key":"281_CR52","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"319","author":"J Heath","year":"2008","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 319(3), 239\u2013257 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"281_CR53","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A.: The theory of hybrid automata. Theor. Comput. Sci 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci"},{"key":"281_CR54","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)"},{"key":"281_CR55","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Model Checking Software: 11th International SPIN, Workshop, pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"281_CR56","unstructured":"IEEE Standard 1076\u20132008: VHDL Language Reference Manual. Technical report, Institute of Electrical and Electronics Engineers (2009)"},{"key":"281_CR57","unstructured":"Cadence Incisive Formal Verifier data sheet. Cadence Design Systems, Inc. http:\/\/www.cadence.com\/rl\/Resources\/datasheets\/IncisiveFV_ds.pdf"},{"issue":"4","key":"281_CR58","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/s10009-004-0154-9","volume":"6","author":"R Iosif","year":"2004","unstructured":"Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6(4), 302\u2013319 (2004)","journal-title":"STTT"},{"issue":"2","key":"281_CR59","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/s10703-005-1491-3","volume":"26","author":"R Iosif","year":"2005","unstructured":"Iosif, R., Dwyer, M.B., Hatcliff, J.: Translating Java for multiple model checkers: the Bandera back-end. Formal Methods Syst. Des. 26(2), 137\u2013180 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"281_CR60","unstructured":"Specification and description language. Technical report, International Telecommunication Union, November 1988. ITU Recommendation Z.100"},{"key":"281_CR61","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-based invariant discovery. In: Bobaru, M., Havelundand, K., Holzmann, G., Joshi, R. (eds.) Proceedings of the 3rd NASA Formal Methods Symposium (Pasadena, CA, USA). Lecture Notes in Computer Science, vol. 6617, pp. 192\u2013207. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-20398-5_15"},{"key":"281_CR62","doi-asserted-by":"crossref","unstructured":"Khurshid, S., P\u01ces\u01cereanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS, pp. 553\u2013568 (2003)","DOI":"10.1007\/3-540-36577-X_40"},{"key":"281_CR63","unstructured":"Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: Proceedings 18th Annual IEEE Symposium on Logic in Computer Science (LICS\u201903), pages 351\u2013360. IEEE Computer Society Press, New York (2003). Invited Paper"},{"key":"281_CR64","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"3","key":"281_CR65","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"281_CR66","unstructured":"Lluch, A.: NuSMV examples: the collection. http:\/\/nusmv.fbk.eu\/examples\/examples.html (1999)"},{"key":"281_CR67","unstructured":"Lluch, A.: Promela database. http:\/\/www.albertolluch.com\/research\/promelamodels (2012)"},{"key":"281_CR68","unstructured":"Mathworks Inc. Simulink Design Verifier product web site. http:\/\/www.mathworks.com\/products\/sldesignverifier"},{"key":"281_CR69","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. Technical Report 1999\u201302, Cadence Berkeley Labs, Berkeley, CA 94704 (1999)","DOI":"10.1007\/3-540-48153-2_30"},{"key":"281_CR70","unstructured":"McMillan, K.L.: Symbolic Model Verifer (SMV)\u2014Cadence Berkeley Laboratories Version. Cadence Design Systems, Inc. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv"},{"key":"281_CR71","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"281_CR72","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, Proceedings, pp. 1\u201312 (2005)","DOI":"10.1007\/978-3-540-31980-1_1"},{"issue":"2","key":"281_CR73","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"281_CR74","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proceedings of ICCAD, vol. 2006, pp. 836\u2013843 (2011)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"281_CR75","doi-asserted-by":"crossref","unstructured":"Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. In: ECCB\u201908 Proceedings, Seventh European Conference on Computational Biology, pp. 227\u2013233 (2008)","DOI":"10.1093\/bioinformatics\/btn275"},{"key":"281_CR76","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Chess: Systematic stress testing of concurrent software. In LOPSTR, pp. 15\u201316 (2006)","DOI":"10.1007\/978-3-540-71410-1_2"},{"key":"281_CR77","volume-title":"Developing Drivers with the Windows Driver Foundation","author":"P Orwick","year":"2007","unstructured":"Orwick, P., Smith, G.: Developing Drivers with the Windows Driver Foundation. Microsoft Press, Redmond (2007)"},{"key":"281_CR78","doi-asserted-by":"crossref","unstructured":"Owens, N., Timmis, J., Greensted, A., Tyrrell, A.: Modelling the tunability of early T cell signalling events. In: 7th International Conference on Artificial Immune Systems (ICARIS\u201908), pp. 12\u201323 (2008)","DOI":"10.1007\/978-3-540-85072-4_2"},{"key":"281_CR79","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C., Dwyer, M., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Theoretical and Practical Aspects of SPIN Model Checking, pp. 168\u2013183. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48234-2_14"},{"issue":"3","key":"281_CR80","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS P\u01ces\u01cereanu","year":"2008","unstructured":"P\u01ces\u01cereanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175\u2013205 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"281_CR81","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: ISSTA, pp. 34\u201344 (2011)","DOI":"10.1145\/2001420.2001425"},{"key":"281_CR82","doi-asserted-by":"crossref","unstructured":"Per Bjesse, K.C.: SAT-based verification without state space traversal. In: International Conference on Formal Methods in Computer Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_23"},{"key":"281_CR83","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"281_CR84","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Anatomy of the Pentium bug. In: Proceedings of the 6th International Joint Conference on Theory and Practice of Software Development, pp. 97\u2013107 (1995)","DOI":"10.1007\/3-540-59293-8_189"},{"key":"281_CR85","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: Proceedings of ISSTA (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"281_CR86","doi-asserted-by":"crossref","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: International Symposium on Programming, 5th Colloquium, Proceedings, pp. 337\u2013351 (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"281_CR87","doi-asserted-by":"crossref","unstructured":"Robby, M.B.D., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. ACM SIGSOFT Softw. Eng. Notes 28(5), 267\u2013276 (2003)","DOI":"10.1145\/949952.940107"},{"key":"281_CR88","volume-title":"System Verilog for Design","author":"S Sutherland","year":"2006","unstructured":"Sutherland, S., Davidmann, S., Flake, P.: System Verilog for Design. Springer, Berlin (2006)"},{"key":"281_CR89","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2896-5","volume-title":"The Verilog Hardware Description Language","author":"DE Thomas","year":"1998","unstructured":"Thomas, D.E., Moorby, P.R.: The Verilog Hardware Description Language. Kluwer, Norwell (1998)"},{"key":"281_CR90","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 133\u2013192 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"281_CR91","doi-asserted-by":"crossref","unstructured":"Tillmann, N., De Halleux, J.: Pex: white box test generation for .NET. In: TAP, pp. 134\u2013153. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"281_CR92","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B., P\u01ces\u01cereanu, C.S.: Automated environment generation for software model checking. In: ASE, pp. 116\u2013129 (2003)","DOI":"10.1109\/ASE.2003.1240300"},{"key":"281_CR93","unstructured":"Turpin, M.: The dangers of living with an X. ARM Ltd. http:\/\/www.arm.com\/files\/pdf\/Verilog_X_Bugs.pdf"},{"key":"281_CR94","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science, pp. 332\u2013344 (1986)"},{"issue":"2","key":"281_CR95","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"281_CR96","doi-asserted-by":"crossref","unstructured":"Wang, J., Zhou, H.: An efficient incremental algorithm for min-area retiming. In: Design Automation Conference (2008)","DOI":"10.1145\/1391469.1391603"},{"key":"281_CR97","doi-asserted-by":"crossref","unstructured":"Xie, T., Tillmann, N., de Halleux, P., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. In: Proceedings of the 39th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN 2009), pp. 359\u2013368 (2009)","DOI":"10.1109\/DSN.2009.5270315"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0281-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-012-0281-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0281-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T03:29:36Z","timestamp":1743996576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-012-0281-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,24]]},"references-count":97,"alternative-id":["281"],"URL":"https:\/\/doi.org\/10.1007\/s10270-012-0281-9","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2012,8,24]]}}}