{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:44:33Z","timestamp":1763459073634,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-9-0179"],"award-info":[{"award-number":["FA8750-12-9-0179"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NNA13AA21C"],"award-info":[{"award-number":["NNA13AA21C"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1145\/2950290.2950346","type":"proceedings-article","created":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T09:46:03Z","timestamp":1477993563000},"page":"314-325","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Efficient generation of inductive validity cores for safety properties"],"prefix":"10.1145","author":[{"given":"Elaheh","family":"Ghassabani","sequence":"first","affiliation":[{"name":"University of Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[{"name":"Rockwell Collins, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"JKind. http:\/\/loonwerks.com\/tools\/jkind.html."},{"key":"e_1_3_2_1_2_1","unstructured":"Set of Support. https:\/\/github.com\/elaghs\/Working\/tree\/ master\/support\/experiments."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/93548.93576"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"J. Backes D. Cofer S. Miller and M. W. Whalen. Requirements analysis of a quad-redundant flight control system. In K. Havelund G. Holzmann and R. Joshi editors NASA Formal Methods volume 9058 of Lecture Notes in Computer Science pages 82\u201396. Springer International Publishing 2015.","DOI":"10.1007\/978-3-319-17524-9_7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.736003"},{"key":"e_1_3_2_1_6_1","first-page":"174","volume-title":"Principles and Practice of Constraint Programming","author":"Belov A.","unstructured":"A. Belov, M. Janota, I. Lynce, and J. Marques-Silva. On computing minimal equivalent subformulas. In Principles and Practice of Constraint Programming, pages 158\u2013174. Springer, 2012."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2350156.2350163"},{"key":"e_1_3_2_1_8_1","first-page":"162","volume-title":"ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings","author":"Ben-David S.","year":"2013","unstructured":"S. Ben-David and O. Kupferman. A framework for ranking vacuity results. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, pages 148\u2013162, 2013."},{"key":"e_1_3_2_1_9_1","first-page":"125","volume-title":"Coverage metrics for formal verification. Correct hardware design and verification methods","author":"Chockler H.","year":"2003","unstructured":"H. Chockler, O. Kupferman, and M. Vardi. Coverage metrics for formal verification. Correct hardware design and verification methods, pages 111\u2013125, 2003."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0060-y"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1768142.1768174"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_16_1","volume-title":"SRI","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. D. Moura. The YICES SMT solver. Technical report, SRI, 2006."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_1_18_1","volume-title":"VERIMAG","author":"Gaucher F.","year":"2003","unstructured":"F. Gaucher. Slicing lustre programs. Technical report, VERIMAG, Grenoble, February 2003."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/996070.1009924"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071369"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517439"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682947"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986326"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337422"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517449"},{"issue":"2","key":"e_1_3_2_1_28_1","article-title":"Vacuity detection in temporal model checking","volume":"4","author":"Kupferman O.","year":"2003","unstructured":"O. Kupferman and M. Y. Vardi. Vacuity detection in temporal model checking. Journal on Software Tools for Technology Transfer, 4(2), February 2003.","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000008668.12782.6c"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2010.11"},{"key":"e_1_3_2_1_31_1","unstructured":"MathWorks Inc. Simulink Design Verifier. http:\/\/www.mathworks.com\/products\/sldesignverifier 2015."},{"key":"e_1_3_2_1_32_1","unstructured":"MathWorks Inc. Simulink Requirements Traceability. http:\/\/www.mathworks.com\/discovery\/requirementstraceability.html 2016."},{"key":"e_1_3_2_1_33_1","unstructured":"K. L. McMillan. A methodology for hardware verification using compositional model checking. Technical Report 1999-01 Cadence Berkeley Labs Berkeley CA 94704 1999."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765875"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_3_2_1_36_1","volume-title":"Issue 2. UK Ministry of Defence","author":"Safety Related Requirements","year":"1997","unstructured":"Requirements for Safety Related Software in Defence Equipment, Issue 2. UK Ministry of Defence, 1997."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2016.35"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"e_1_3_2_1_39_1","first-page":"294","volume-title":"NASA Formal Methods","author":"Murugesan A.","unstructured":"A. Murugesan, M. W. Whalen, N. Rungta, O. Tkachuk, S. Person, M. P. Heimdahl, and D. You. Are we there yet? Determining the adequacy of formalized requirements and test suites. In NASA Formal Methods, pages 279\u2013294. Springer, 2015."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998537"},{"key":"e_1_3_2_1_41_1","unstructured":"RTCA\/DO-178C. Software considerations in airborne systems and equipment certification."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2023474.2023494"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.32"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_3_2_1_45_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","unstructured":"F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121\u2013189, 1995.","journal-title":"Journal of Programming Languages"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/800078.802557"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486803"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2015.7381816"},{"key":"e_1_3_2_1_50_1","volume-title":"6th International Conference on Theory and Applications of Satisfiability Testing: SAT 2003","author":"Zhang L.","year":"2003","unstructured":"L. Zhang and S. Malik. Extracting small unsatisfiable cores from unsatisfiable boolean formula. In 6th International Conference on Theory and Applications of Satisfiability Testing: SAT 2003, May 2003."}],"event":{"name":"FSE'16: 24nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Seattle WA USA","acronym":"FSE'16"},"container-title":["Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2950290.2950346","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2950290.2950346","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2950290.2950346","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:39:57Z","timestamp":1763458797000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2950290.2950346"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":50,"alternative-id":["10.1145\/2950290.2950346","10.1145\/2950290"],"URL":"https:\/\/doi.org\/10.1145\/2950290.2950346","relation":{},"subject":[],"published":{"date-parts":[[2016,11]]},"assertion":[{"value":"2016-11-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}