{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T10:36:42Z","timestamp":1761129402562,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,16]],"date-time":"2017-01-16T00:00:00Z","timestamp":1484524800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP16K00109"],"award-info":[{"award-number":["JP16K00109"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018626","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"66-78","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalization of Karp-Miller tree construction on petri nets"],"prefix":"10.1145","author":[{"given":"Mitsuharu","family":"Yamamoto","sequence":"first","affiliation":[{"name":"Chiba University, Japan"}]},{"given":"Shogo","family":"Sekine","sequence":"additional","affiliation":[{"name":"Acrovision, Japan"}]},{"given":"Saki","family":"Matsumoto","sequence":"additional","affiliation":[{"name":"Chiba University, Japan"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Vol. 3","first-page":"168","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky S.","unstructured":"S. Abramsky and A. Jung . Domain theory . In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science ( Vol. 3 ), pages 1\u2013 168 . Oxford University Press, Oxford, UK, 1994. S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 3), pages 1\u2013168. Oxford University Press, Oxford, UK, 1994."},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"298","volume-title":"Proc. ITP","author":"Asperti A.","year":"2012","unstructured":"A. Asperti . A compact proof of decidability for regular expression equivalence . In Proc. ITP , volume 7406 of LNCS , pages 283\u2014- 298 , 2012 . A. Asperti. A compact proof of decidability for regular expression equivalence. In Proc. ITP, volume 7406 of LNCS, pages 283\u2014- 298, 2012."},{"key":"e_1_3_2_1_3_1","volume-title":"Coq\u2019Art: the Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development , Coq\u2019Art: the Calculus of Inductive Constructions . Springer-Verlag , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_26"},{"key":"e_1_3_2_1_6_1","volume-title":"A finset and finmap DRAFT library","author":"Cohen C.","year":"2016","unstructured":"C. Cohen . A finset and finmap DRAFT library , 2016 . C. Cohen. A finset and finmap DRAFT library, 2016."},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"243","volume-title":"Advances in Petri Nets","author":"Finkel A.","year":"1993","unstructured":"A. Finkel . The minimal coverability graph for Petri nets . In G.Rozenberg, editor, Advances in Petri Nets 1993 , volume 674 of LNCS , pages 210\u2013 243 , 1991. A. Finkel. The minimal coverability graph for Petri nets. In G.Rozenberg, editor, Advances in Petri Nets 1993, volume 674 of LNCS, pages 210\u2013243, 1991."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02930-1_16"},{"key":"e_1_3_2_1_9_1","volume-title":"Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28):1\u201335","author":"Finkel A.","year":"2012","unstructured":"A. Finkel and J. Goubault-Larrecq . Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28):1\u201335 , 2012 . A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28):1\u201335, 2012."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054110007180"},{"issue":"2","key":"e_1_3_2_1_11_1","first-page":"95","article-title":"An introduction to small scale reflection in coq","volume":"3","author":"Gonthier G.","year":"2010","unstructured":"G. Gonthier and A. Mahboubi . An introduction to small scale reflection in coq . Journal of Formalized Reasoning , 3 ( 2 ): 95 \u2013 152 , 2010 . G. Gonthier and A. Mahboubi. An introduction to small scale reflection in coq. Journal of Formalized Reasoning, 3(2):95\u2013152, 2010.","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","first-page":"461","volume-title":"Foundations of Software Science and Computation Structures","author":"Hofman P.","year":"2016","unstructured":"P. Hofman , S. Lasota , R. Lazi\u00b4c , J. Leroux , S. Schmitz , and P. Totzke . Coverability trees for Petri nets with unordered data . In Foundations of Software Science and Computation Structures , volume 9634 of LNCS , pages 445\u2013 461 , 2016 . P. Hofman, S. Lasota, R. Lazi\u00b4c, J. Leroux, S. Schmitz, and P. Totzke. Coverability trees for Petri nets with unordered data. In Foundations of Software Science and Computation Structures, volume 9634 of LNCS, pages 445\u2013461, 2016."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(72)90063-5"},{"key":"e_1_3_2_1_15_1","volume-title":"TPHOLs\u201908 Emerging Trends","author":"Lescuyer S.","year":"2008","unstructured":"S. Lescuyer and S. Conchon . A reflexive formalization of a SAT solver in Coq . In TPHOLs\u201908 Emerging Trends , 2008 . S. Lescuyer and S. Conchon. A reflexive formalization of a SAT solver in Coq. In TPHOLs\u201908 Emerging Trends, 2008."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9127-8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1804226.1804231"},{"key":"e_1_3_2_1_20_1","volume-title":"JSSST Workshop on Programming and Programming Languages (PPL\u201907)","author":"Marti N.","year":"2007","unstructured":"N. Marti and R. Affeldt . A certified verifier for a fragment of separation logic . In JSSST Workshop on Programming and Programming Languages (PPL\u201907) , 2007 . N. Marti and R. Affeldt. A certified verifier for a fragment of separation logic. In JSSST Workshop on Programming and Programming Languages (PPL\u201907), 2007."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3405"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2013-781"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2014-1002"},{"key":"e_1_3_2_1_26_1","volume-title":"April","author":"Veldman W.","year":"1993","unstructured":"W. Veldman and M. Bezem . Ramsey\u2019s theorem and the pigeonhole principle in intuitionistic mathematics. J. London Math. Soc., s2-47(2):193\u2013211 , April 1993 . W. Veldman and M. Bezem. Ramsey\u2019s theorem and the pigeonhole principle in intuitionistic mathematics. J. London Math. Soc., s2-47(2):193\u2013211, April 1993."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_17"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9297-2"},{"key":"e_1_3_2_1_29_1","volume-title":"Formalization of Petri nets and forward analysis with Karp-Miller trees","author":"Yamamoto M.","year":"2016","unstructured":"M. Yamamoto , S. Sekine , and S. Matsumoto . Formalization of Petri nets and forward analysis with Karp-Miller trees , 2016 . M. Yamamoto, S. Sekine, and S. Matsumoto. Formalization of Petri nets and forward analysis with Karp-Miller trees, 2016."}],"event":{"name":"CPP '17: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Paris France","acronym":"CPP '17"},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018626","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:59Z","timestamp":1750220639000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":28,"alternative-id":["10.1145\/3018610.3018626","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018626","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}