{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:52Z","timestamp":1725511852524},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_12","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T06:37:44Z","timestamp":1210142264000},"page":"149-163","source":"Crossref","is-referenced-by-count":3,"title":["Model Classifications and Automated Verification"],"prefix":"10.1007","author":[{"given":"Radek","family":"Pel\u00e1nek","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/378795.378846","volume-title":"Proc. of Programming Language Design and Implementation (PLDI 2001)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: Proc. of Programming Language Design and Implementation (PLDI 2001), pp. 203\u2013213. ACM Press, New York (2001)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/11804192_13","volume-title":"Formal Methods for Components and Objects","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., Cern\u00e1, I.: Cluster-based ltl model checking of large systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 259\u2013279. Springer, Heidelberg (2006)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/ASE.2003.1240299","volume-title":"Proc. Automated Software Engineering (ASE 2003)","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: Proc. Automated Software Engineering (ASE 2003), pp. 106\u2013115. IEEE Computer Society, Los Alamitos (2003)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725. Springer, Heidelberg (2003)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/3-540-45657-0_50","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2002","unstructured":"Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 596\u2013609. Springer, Heidelberg (2002)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.: Model checking coloured petri nets exploiting strongly connected components. Technical Report DAIMI PB \u2013 519, Computer Science Department, University of Aarhus (1997)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"Proc. Workshop on Formal Methods in Software Practice","author":"M.B. Dwyer","year":"1998","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM Press, New York (1998)"},{"issue":"3","key":"12_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1002\/cpe.1068","volume":"19","author":"Y. Eytani","year":"2007","unstructured":"Eytani, Y., Havelund, K., Stoller, S.D., Ur, S.: Toward a Framework and Benchmark for Testing Tools for Multi-Threaded Programs. Concurrency and Computation: Practice and Experience\u00a019(3), 267\u2013279 (2007)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"12_CR12","first-page":"110","volume-title":"Proc. of Principles of programming languages (POPL 2005)","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proc. of Principles of programming languages (POPL 2005), pp. 110\u2013121. ACM Press, New York (2005)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"12_CR14","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Reading (1995)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-540-24732-6_3","volume-title":"Model Checking Software","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 23\u201339. Springer, Heidelberg (2004)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems: An approach to the state-explosion problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems: An approach to the state-explosion problem. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"12_CR18","first-page":"117","volume-title":"Proc. of Foundations of software engineering","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proc. of Foundations of software engineering, pp. 117\u2013127. ACM Press, New York (2006)"},{"key":"12_CR19","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proc. of SPIN Workshop (1997)"},{"key":"12_CR20","volume-title":"The Spin Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts (2003)"},{"key":"12_CR21","first-page":"23","volume-title":"Proc. SPIN Workshop","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. SPIN Workshop, pp. 23\u201332. American Mathematical Society, Providence, RI (1996)"},{"issue":"1\u20132","key":"12_CR22","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design\u00a09(1\u20132), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"key":"12_CR23","series-title":"ENTCS","volume-title":"Proc. of Parallel and Distributed Methods in verifiCation (PDMC 2003)","author":"P. Kr\u010d\u00e1l","year":"2003","unstructured":"Kr\u010d\u00e1l, P.: Distributed explicit bounded ltl model checking. In: Proc. of Parallel and Distributed Methods in verifiCation (PDMC 2003). ENTCS, vol.\u00a089. Elsevier, Amsterdam (2003)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/3-540-45657-0_48","volume-title":"Computer Aided Verification","author":"R.P. Kurshan","year":"2002","unstructured":"Kurshan, R.P., Levin, V., Yenig\u00fcn, H.: Compressing transitions for model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 569\u2013581. Springer, Heidelberg (2002)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-46002-0_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Lang","year":"2002","unstructured":"Lang, F.: Compositional verification using svl scripts. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 465\u2013469. Springer, Heidelberg (2002)"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"issue":"5663","key":"12_CR27","doi-asserted-by":"publisher","first-page":"1538","DOI":"10.1126\/science.1089167","volume":"303","author":"R. Milo","year":"2004","unstructured":"Milo, R., Itzkovitz, S., Kashtan, N., Levitt, R., Shen-Orr, S., Ayzenshtat, I., Sheffer, M., Alon, U.: Superfamilies of evolved and designed networks. Science\u00a0303(5663), 1538\u20131542 (2004)","journal-title":"Science"},{"issue":"5594","key":"12_CR28","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1126\/science.298.5594.824","volume":"298","author":"R. Milo","year":"2002","unstructured":"Milo, R., Shen-Orr, S., Itzkovitz, S., Kashtan, N., Chklovskii, D., Alon, U.: Network motifs: Simple building blocks of complex networks. Science\u00a0298(5594), 824\u2013827 (2002)","journal-title":"Science"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-540-30494-4_12","volume-title":"Formal Methods in Computer-Aided Design","author":"H. Mony","year":"2004","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 159\u2013173. Springer, Heidelberg (2004)"},{"key":"12_CR30","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/S0140-3664(97)00075-3","volume":"20","author":"K. Ozdemir","year":"1997","unstructured":"Ozdemir, K., Ural, H.: Protocol validation by simultaneous reachability analysis. Computer Communications\u00a020, 772\u2013788 (1997)","journal-title":"Computer Communications"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-24732-6_2","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2004","unstructured":"Pel\u00e1nek, R.: Typical structural properties of state spaces. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"12_CR32","unstructured":"Pel\u00e1nek, R.: Evaluation of on-the-fly state space reductions. In: Proc. of Mathematical and Engineering Methods in Computer Science (MEMICS 2005), pp. 121\u2013127 (2005)"},{"key":"12_CR33","unstructured":"Pel\u00e1nek, R.: Reduction and Abstraction Techniques for Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno (2006)"},{"key":"12_CR34","unstructured":"Pel\u00e1nek, R.: Web portal for benchmarking explicit model checkers. Technical Report FIMU-RS-2006-03, Masaryk University Brno (2006), http:\/\/anna.fi.muni.cz\/models\/"},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: Beem: Benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"12_CR36","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/1081180.1081193","volume-title":"Proc. of Formal Methods for Industrial Critical Systems (FMICS 2005)","author":"R. Pel\u00e1nek","year":"2005","unstructured":"Pel\u00e1nek, R., Han\u017el, T., \u010cern\u00e1, I., Brim, L.: Enhancing random walk state space exploration. In: Proc. of Formal Methods for Industrial Critical Systems (FMICS 2005), pp. 98\u2013105. ACM Press, New York (2005)"},{"issue":"4","key":"12_CR37","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G.D. Penna","year":"2004","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Exploiting transition locality in automatic verification of finite state concurrent systems. Software Tools for Technology Transfer (STTT)\u00a06(4), 320\u2013341 (2004)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"issue":"2","key":"12_CR38","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10009-002-0078-1","volume":"4","author":"T.C. Ruys","year":"2003","unstructured":"Ruys, T.C., Brinksma, E.: Managing the verification trajectory. International Journal on Software Tools for Technology Transfer (STTT)\u00a04(2), 246\u2013259 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"12_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/11560548_38","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Sahoo","year":"2005","unstructured":"Sahoo, D., Jain, J., Iyer, S.K., Dill, D., Emerson, E.A.: Predictive reachability using a sample-based approach. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 388\u2013392. Springer, Heidelberg (2005)"},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proc. of Parallel and Distributed Model Checking (PDMC 2003). ENTCS, vol.\u00a089 (2003)","DOI":"10.1016\/S1571-0661(05)80096-9"},{"key":"12_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the Murphi verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"12_CR42","first-page":"332","volume-title":"Proc. of Logic in Computer Science (LICS 1986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Kozen, D. (ed.) Proc. of Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:28:36Z","timestamp":1619522916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_12","relation":{},"subject":[]}}