{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T23:25:04Z","timestamp":1781565904345,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,7]],"date-time":"2020-11-07T00:00:00Z","timestamp":1604707200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100012658","name":"European Research Council","doi-asserted-by":"publisher","award":["638049"],"award-info":[{"award-number":["638049"]}],"id":[{"id":"10.13039\/100012658","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3409669","type":"proceedings-article","created":{"date-parts":[[2020,11,10]],"date-time":"2020-11-10T21:08:44Z","timestamp":1605042524000},"page":"99-110","source":"Crossref","is-referenced-by-count":17,"title":["Inherent vacuity for GR(1) specifications"],"prefix":"10.1145","author":[{"given":"Shahar","family":"Maoz","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafi","family":"Shalom","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,7]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"[n.d.]. Supporting materials website. http:\/\/smlab.cs.tau.ac.il\/syntech\/vacuity\/.  [n.d.]. Supporting materials website. http:\/\/smlab.cs.tau.ac.il\/syntech\/vacuity\/."},{"key":"e_1_3_2_2_2_1"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_7"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_35"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Ilan Beer Shoham Ben-David Cindy Eisner and Yoav Rodeh. 2001. Eficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18 2 ( 2001 ) 141-163. https:\/\/doi.org\/10.1023\/A:1008779610539 10.1023\/A:1008779610539  Ilan Beer Shoham Ben-David Cindy Eisner and Yoav Rodeh. 2001. Eficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18 2 ( 2001 ) 141-163. https:\/\/doi.org\/10.1023\/A:1008779610539 10.1023\/A:1008779610539","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_4"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1266366.1266622"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_16"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_7"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Hana Chockler Arie Gurfinkel and Ofer Strichman. 2013. Beyond vacuity: towards the strongest passing formula. Formal Methods in System Design 43 3 ( 2013 ) 552-571. https:\/\/doi.org\/10.1007\/s10703-013-0192-6 10.1007\/s10703-013-0192-6  Hana Chockler Arie Gurfinkel and Ofer Strichman. 2013. Beyond vacuity: towards the strongest passing formula. Formal Methods in System Design 43 3 ( 2013 ) 552-571. https:\/\/doi.org\/10.1007\/s10703-013-0192-6 10.1007\/s10703-013-0192-6","DOI":"10.1007\/s10703-013-0192-6"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787535"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.157.12"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00351-9"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01702-5_7"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/938135"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_30"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_22"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071369"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0221-y"},{"key":"e_1_3_2_2_26_1","unstructured":"Dexter Kozen. 1983. Results on the Propositional mu-Calculus. Theor. Comput. Sci. 27 ( 1983 ) 333-354. https:\/\/doi.org\/10.1016\/ 0304-3975 ( 82 ) 90125-6 10.1016\/0304-3975(82)90125-6  Dexter Kozen. 1983. Results on the Propositional mu-Calculus. Theor. Comput. Sci. 27 ( 1983 ) 333-354. https:\/\/doi.org\/10.1016\/ 0304-3975 ( 82 ) 90125-6 10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106240"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786824"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.202.5"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950300"},{"key":"e_1_3_2_2_33_1","volume-title":"Spectra: A Specification Language for Reactive Systems. CoRR abs\/","author":"Maoz Shahar","year":"2019"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00106"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486821"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6161470"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2011.22"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_24"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.229.8"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Jocelyn Simmonds Jessica Davies Arie Gurfinkel and Marsha Chechik. 2010. Exploiting resolution proofs to speed up LTL vacuity detection for BMC. STTT 12 5 ( 2010 ) 319-335. https:\/\/doi.org\/10.1007\/s10009-009-0134-1 10.1007\/s10009-009-0134-1  Jocelyn Simmonds Jessica Davies Arie Gurfinkel and Marsha Chechik. 2010. Exploiting resolution proofs to speed up LTL vacuity detection for BMC. STTT 12 5 ( 2010 ) 319-335. https:\/\/doi.org\/10.1007\/s10009-009-0134-1 10.1007\/s10009-009-0134-1","DOI":"10.1007\/s10009-009-0134-1"},{"key":"e_1_3_2_2_41_1","volume-title":"CUDD: BDD package","author":"Somenzi Fabio"},{"key":"e_1_3_2_2_42_1","unstructured":"Spectra [n.d.]. Spectra Website. http:\/\/smlab.cs.tau.ac.il\/syntech\/spectra\/.  Spectra [n.d.]. Spectra Website. http:\/\/smlab.cs.tau.ac.il\/syntech\/spectra\/."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967747"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988498"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Virtual Event USA","acronym":"ESEC\/FSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409669","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3409669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:39Z","timestamp":1750203879000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,7]]},"references-count":44,"alternative-id":["10.1145\/3368089.3409669","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3409669","relation":{},"subject":[],"published":{"date-parts":[[2020,11,7]]}}}