{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,26]],"date-time":"2025-07-26T08:54:55Z","timestamp":1753520095575,"version":"3.40.4"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_23","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"348-363","source":"Crossref","is-referenced-by-count":5,"title":["Bounded Model Checking High Level Petri Nets in PIPE+Verifier"],"prefix":"10.1007","author":[{"given":"Su","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reng","family":"Zeng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhuo","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"CPN tools, http:\/\/cpntools.org","key":"23_CR1"},{"unstructured":"High-level Petri Nets - Concepts, Definitions and Graphical Notation (2000)","key":"23_CR2"},{"issue":"1","key":"23_CR3","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A. Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. Int. J. Softw. Tools Technol. Transf.\u00a011(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003); 12th International Conference on Rewriting Techniques and Applications (RTA 2001)","key":"23_CR4","DOI":"10.1016\/S0890-5401(03)00020-8"},{"unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: Slam2: static driver verification with under 4. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Austin, TX, pp. 35\u201342. FMCAD Inc. (2010)","key":"23_CR5"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Barrett, C., De Moura, L., Stump, A.: Design and results of the 1st satisfiability modulo theories competition (smt-comp.). Journal of Automated Reasoning\u00a035, 2005 (2005)","key":"23_CR7","DOI":"10.1007\/s10817-006-9026-1"},{"unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http:\/\/www.SMT-LIB.org","key":"23_CR8"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Chiola, G., Franceschinis, G.: Colored gspn models and automatic symmetry detection. In: PNPM, pp. 50\u201360 (1989)","key":"23_CR11","DOI":"10.1109\/PNPM.1989.68539"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. In: Formal Methods in System Design, p. 2001. Kluwer Academic Publishers (2001)","key":"23_CR13"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 85\u201396. Springer, Heidelberg (2004)"},{"issue":"9","key":"23_CR16","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L. Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura De","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"11","key":"23_CR18","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"E.W. Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM\u00a017(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"unstructured":"Dutertre, B., De Moura, L.: The yices smt solver 2, 2 (2006), Tool paper, http:\/\/yices.csl.sri.com\/tool-paper.pdf","key":"23_CR19"},{"issue":"3","key":"23_CR20","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. Allen Emerson","year":"1987","unstructured":"Allen Emerson, E., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program.\u00a08(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-319-02444-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"\u0141. Fronc","year":"2013","unstructured":"Fronc, \u0141., Duret-Lutz, A.: LTL model checking with neco. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol.\u00a08172, pp. 451\u2013454. Springer, Heidelberg (2013)"},{"unstructured":"Holzmann, G.: Spin model checker, the: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)","key":"23_CR22"},{"issue":"3-4","key":"23_CR23","doi-asserted-by":"crossref","first-page":"229","DOI":"10.3233\/FI-2011-608","volume":"113","author":"S. Hostettler","year":"2011","unstructured":"Hostettler, S., Marechal, A., Linard, A., Risoldi, M., Buchs, D.: High-level petri net model checking with alpina. Fundam. Inf.\u00a0113(3-4), 229\u2013264 (2011)","journal-title":"Fundam. Inf."},{"unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)","key":"23_CR24"},{"issue":"3","key":"23_CR25","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K. Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf.\u00a09(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)","key":"23_CR26"},{"unstructured":"Kordon, F., Linard, A., Becutti, M., Buchs, D., Fronc, L., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodr\u00edgues, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Web report on the model checking contest @ petri net 2013 (June 2013), http:\/\/mcc.lip6.fr","key":"23_CR27"},{"unstructured":"Kordon, F., Linard, A., Beccuti, M., Buchs, D., Fronc, L., Hillah, L.-M., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodr\u00edguez, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Model checking contest @ petri nets, report on the 2013 edition. CoRR, abs\/1309.2485 (2013)","key":"23_CR28"},{"unstructured":"Kr\u00f6ning, D., R\u00fcmmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the smt-lib standard. In: Informal proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE 22 (2009)","key":"23_CR29"},{"unstructured":"Liu, S., Zeng, R., He, X.: Pipe+ - a modeling tool for high level petri nets. In: SEKE, pp. 115\u2013121 (2011)","key":"23_CR30"},{"unstructured":"Liu, S., Zeng, R., Sun, Z., He, X.: Samat - a tool for software architecture modeling and analysis. In: SEKE, pp. 352\u2013358 (2012)","key":"23_CR31"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-10452-7_3","volume-title":"Formal Methods: Foundations and Applications","author":"L. Moura de","year":"2009","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability Modulo Theories: An Appetizer. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 23\u201336. Springer, Heidelberg (2009)"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1007\/978-3-642-02658-4_58","volume-title":"Computer Aided Verification","author":"S. Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: VS3: SMT Solvers for Program Verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 702\u2013708. Springer, Heidelberg (2009)"},{"unstructured":"Stepney, S.: An Electronic Purse: Specification, Refinement, and Proof. Technical monograph. Oxford University Computing Laboratory, Programming Research Group (2000)","key":"23_CR34"},{"doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: A decision procedure for an extensional theory of arrays. In: 16th IEEE Symposium on Logic in Computer Science, pp. 29\u201337. IEEE Computer Society (2001)","key":"23_CR35","DOI":"10.1109\/LICS.2001.932480"},{"key":"23_CR36","volume-title":"Elements of ML programming (ML97 ed.)","author":"J.D. Ullman","year":"1998","unstructured":"Ullman, J.D.: Elements of ML programming (ML97 ed.). Prentice-Hall, Inc., Upper Saddle River (1998)"},{"issue":"2-3","key":"23_CR37","first-page":"149","volume":"3","author":"M. Veanes","year":"2009","unstructured":"Veanes, M., Bj\u00f8rner, N., Gurevich, Y., Schulte, W.: Symbolic bounded model checking of abstract state machines. Int. J. Software and Informatics\u00a03(2-3), 149\u2013170 (2009)","journal-title":"Int. J. Software and Informatics"},{"key":"23_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-68855-6_4","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Bj\u00f8rner, N.S., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol.\u00a05048, pp. 53\u201368. Springer, Heidelberg (2008)"},{"issue":"2","key":"23_CR39","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engg.\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engg."},{"issue":"10","key":"23_CR40","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. Computer\u00a039(10), 57\u201364 (2006)","journal-title":"Computer"},{"issue":"1","key":"23_CR41","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s00165-007-0060-5","volume":"20","author":"J. Woodcock","year":"2008","unstructured":"Woodcock, J., Stepney, S., Cooper, D., Clark, J.A., Jacob, J.: The certification of the mondex electronic purse to itsec level e6. Formal Asp. Comput.\u00a020(1), 5\u201319 (2008)","journal-title":"Formal Asp. Comput."},{"key":"23_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-14808-8_15","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"R. Zeng","year":"2010","unstructured":"Zeng, R., He, X.: Analyzing a formal specification of mondex using model checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 214\u2013229. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Zeng, R., Liu, J., He, X.: A formal specification of mondex using sam. In: IEEE International Symposium on Service-Oriented System Engineering, SOSE 2008, pp. 97\u2013102 (December 2008)","key":"23_CR43","DOI":"10.1109\/SOSE.2008.25"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:24:59Z","timestamp":1746419099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}