{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T12:04:12Z","timestamp":1702469052830},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,1,29]],"date-time":"2015-01-29T00:00:00Z","timestamp":1422489600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10703-014-0221-0","type":"journal-article","created":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T08:19:57Z","timestamp":1422433197000},"page":"81-104","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Vacuity in practice: temporal antecedent failure"],"prefix":"10.1007","volume":"46","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fady","family":"Copty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dana","family":"Fisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sitvanit","family":"Ruah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,1,29]]},"reference":[{"key":"221_CR1","volume-title":"Compilers: princiles, techniques, and tools","author":"AV Aho","year":"1986","unstructured":"Aho AV, Sethi R, Ullman JD (1986) Compilers: princiles, techniques, and tools. Addison-Wesley, Boston"},{"key":"221_CR2","doi-asserted-by":"crossref","unstructured":"Armoni R, Fix L, Flaisher A, Grumberg O, Piterman N, Tiemeyer A, Vardi MY (2003) Enhanced vacuity detection in linear temporal logic. In: Proceedings of the 15th international conference on computer aided verification (CAV), Boulder, CO, USA, 8\u201312 July 2003, pp 368\u2013380","DOI":"10.1007\/978-3-540-45069-6_35"},{"key":"221_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Mony H, Paruthi V, Kanzelman R, Janssen G (2006) Scalable sequential equivalence checking across arbitrary design transformations. In: 24th International Conference on Computer Design (ICCD), San Jose, CA, USA, 1\u20134 Oct 2006, pp. 259\u2013266","DOI":"10.1109\/ICCD.2006.4380826"},{"key":"221_CR4","unstructured":"Beatty DL, Bryant RE (1994) Formally verifying a microprocessor using a simulation methodology. In: 31st Design automation conference (DAC), San Diego, CA, USA, 6\u201310 June 1994, pp 596\u2013602"},{"key":"221_CR5","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (1997) Efficient detection of vacuity in ACTL formulas. In: Proceedings of the 9th international conference on computer aided verification (CAV), Haifa, Israel, 22-25 June 1997, pp 279\u2013290","DOI":"10.1007\/3-540-63166-6_28"},{"issue":"2","key":"221_CR6","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in temporal model checking. Form Methods Syst Des 18(2):141\u2013163","journal-title":"Form Methods Syst Des"},{"key":"221_CR7","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Landver A (1998) On-the-fly model checking of RCTL formulas. In: Proceedings of the 10th international conference on computer aided verification (CAV), Vancouver, BC, Canada, 28 June\u20132 1998, pp 184\u2013194","DOI":"10.1007\/BFb0028744"},{"key":"221_CR8","unstructured":"Ben-David S, Fisman D, Ruah S (2004) Automata construction for regular expressions in model checking, June. IBM research report H-0229"},{"key":"221_CR9","unstructured":"Ben-David S, Fisman D, Ruah S (2005) The safety simple subset. In: Hardware and software verification and testing, First international Haifa verification conference (HVC). Haifa, Israel, 13\u201316 Nov 2005, Revised Selected Papers, pp 14\u201329"},{"key":"221_CR10","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(86)90088-5","volume":"48","author":"G Berry","year":"1986","unstructured":"Berry G, Sethi R (1986) From regular expression to deterministic automata. Theo Comput Sci 48:117\u2013126","journal-title":"Theo Comput Sci"},{"key":"221_CR11","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for construction and analysis of systems, 5th international conference (TACAS), held as part of the European joint conferences on the theory and practice of software (ETAPS), Amsterdam, The Netherlands, 22\u201328 March 1999, pp 193\u2013207","DOI":"10.21236\/ADA360973"},{"key":"221_CR12","doi-asserted-by":"crossref","unstructured":"Bjesse P, Claessen K (2000) Sat-based verification without state space traversal. In: 3rd international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 1-3 Nov 2000, pp 372\u2013389","DOI":"10.1007\/3-540-40922-X_23"},{"key":"221_CR13","doi-asserted-by":"crossref","unstructured":"Boule M, Zilic Z (2007) Efficient automata-based assertion-checker synthesis of SEREs for hardware emulation. In: Proceedings of the 12th conference on Asia South Pacific design automation (ASP-DAC), Yokohama, Japan, 23-26 Jan 2007, pp 324\u2013329","DOI":"10.1109\/ASPDAC.2007.358006"},{"key":"221_CR14","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) Sat-based model checking without unrolling. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation (VMCAI), Austin, TX, USA, 23-25 Jan 2011, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"221_CR15","unstructured":"Bryant RE, Chauhan P, Clarke EM, Goel A (2000) A theory of consistency for modular synchronous systems. In: Proceedings of the 3rd international conference on formal methods in computer-aided design, Austin, Texas, USA, 1\u20133 Nov 2000, pp 486\u2013504"},{"key":"221_CR16","unstructured":"Bustan D, Fisman D, Havlicek J (2005) Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science, May 2005"},{"key":"221_CR17","doi-asserted-by":"crossref","unstructured":"Bustan D, Flaisher A, Grumberg O, Kupferman O, Vardi Y (2005) Regular vacuity. In: Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on correct hardware design and verification methods (CHARME\u201905), Saarbriiucken, Germany, 3\u20136 Oct 2005, pp 191\u2013206","DOI":"10.1007\/11560548_16"},{"key":"221_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-6600-1","volume-title":"The power of assertions in SystemVerilog","author":"E Cerny","year":"2010","unstructured":"Cerny E, Dudani S, Havlicek J, Korchemny D (2010) The power of assertions in SystemVerilog. Springer, London"},{"key":"221_CR19","doi-asserted-by":"crossref","unstructured":"Chechik M, Gheorghiu M, Gurfinkel A (2007) Finding environment guarantees. In: Proceedings of the 10th international conference on fundamental approaches to software engineering (FASE), held as part of the joint European conferences on theory and practice of software (ETAPS), Braga, Portugal, 24 March-1 April 2007, pp 352\u2013367","DOI":"10.1007\/978-3-540-71289-3_27"},{"key":"221_CR20","doi-asserted-by":"crossref","unstructured":"Chockler H, Gurfinkel A, Strichman O (2008) Beyond vacuity: towards the strongest passing formula. In: Formal methods in computer-aided design (FMCAD), Portland, Oregon, USA, 17-20 Nov 2008, pp 1\u20138","DOI":"10.1109\/FMCAD.2008.ECP.28"},{"issue":"4\u20135","key":"221_CR21","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s10009-004-0175-4","volume":"8","author":"H Chockler","year":"2006","unstructured":"Chockler H, Kupferman O, Vardi MY (2006) Coverage metrics for formal verification. STTT 8(4\u20135):373\u2013386","journal-title":"STTT"},{"issue":"3","key":"221_CR22","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/s10703-006-0001-6","volume":"28","author":"H Chockler","year":"2006","unstructured":"Chockler H, Kupferman O, Vardi MY (2006) Coverage metrics for temporal logic model checking. Form Methods Syst Des 28(3):189\u2013212","journal-title":"Form Methods Syst Des"},{"key":"221_CR23","doi-asserted-by":"crossref","unstructured":"Chockler H, Strichman O (2007) Easier and more informative vacuity checks. In: 5th ACM & IEEE international conference on formal methods and models for co-design (MEMOCODE), Nice, France, 30 May-1 June, pp 189\u2013198","DOI":"10.1109\/MEMCOD.2007.371225"},{"issue":"1","key":"221_CR24","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10703-008-0060-y","volume":"34","author":"H Chockler","year":"2009","unstructured":"Chockler H, Strichman O (2009) Before and after vacuity. Form Methods Syst Des 34(1):37\u201358","journal-title":"Form Methods Syst Des"},{"key":"221_CR25","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branchingtime temporal logic. In Proceedings of the workshop on logics of programs,Yorktown Heights, New York, May 1981, pp 52\u201371"},{"key":"221_CR26","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. The MIT Press, Cambridge"},{"key":"221_CR27","unstructured":"Dong Y, Saran-Starosta B, Ramakrishnan CR, Smolka SA (2002) Vacuity checking in the modal Mu-claculus. In: Proceeding of the 9th international conference on algebraic methodology and software technology (AMAST), Saint-Gilles-les-Bains, Reunion Island, France, 9-13 Sept 2002, pp 147\u2013162"},{"key":"221_CR28","volume-title":"A practical introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, Berlin"},{"key":"221_CR29","unstructured":"Fisman D, Kupferman O, Sheinvald-Faragy S, Vardi MY (2008) A framework for inherent vacuity. In: Proceedings of the 4th International haifa verification conference (HVC) on hardware and software: verification and testing, Haifa, Israel, 27\u201330 Oct 2008, pp 7\u201322"},{"key":"221_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1070\/RM1961v016n05ABEH004112","volume":"16","author":"VM Glushkov","year":"1953","unstructured":"Glushkov VM (1953) The abstract theory of automata. Russ Math Surv 16:1\u201353","journal-title":"Russ Math Surv"},{"key":"221_CR31","unstructured":"Gro\u00dfe D, Wille R, K\u00fchne U, Drechsler R (2009) Contradictory antecedent debugging in bounded model checking. In: Proceedings of the 19th ACM great lakes symposium on VLSI, Boston Area, MA, USA, 10\u201312 May 2009, pp 173\u2013176"},{"key":"221_CR32","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Chechik M (2004) Extending extended vacuity. In: Proceedings of the 5th international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 15\u201317 Nov 2004, pp 306\u2013321","DOI":"10.1007\/978-3-540-30494-4_22"},{"key":"221_CR33","unstructured":"Gurfinkel A, Chechik M (2004) How vacuous is vacuous? In: Proceedings of the 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS), held as part of the joint European conferences on theory and practice of software (ETAPS), Barcelona, Spain, 29 March-2 April 2004, pp 451\u2013466"},{"key":"221_CR34","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages, and computation. Addison-Wesley Series in Computer Science. Addison-Wesley, Boston"},{"key":"221_CR35","unstructured":"IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850\u2122-2010"},{"key":"221_CR36","unstructured":"IEEE Standard for SystemVerilog\u2014unified hardware design, specification, and verification language, Annex F. IEEE Std 1800\u2122-2009"},{"key":"221_CR37","doi-asserted-by":"crossref","unstructured":"Kupferman O (2006) Sanity checks in formal verification. In: Proceedings of the 17th International conference on concurrency theory (CONCUR), Bonn, Germany, Aug 27\u201330, 2006, pp 37\u201351","DOI":"10.1007\/11817949_3"},{"key":"221_CR38","doi-asserted-by":"crossref","unstructured":"Kupferman O, Li W, Seshia SA (2008) A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: Formal methods in computer-aided design (FMCAD), Portland, Oregon, USA, 17\u201320 Nov 2008, pp 1\u20139","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"key":"221_CR39","doi-asserted-by":"crossref","unstructured":"Kupferman O, Lustig Y (2007) Lattice automata. In: Proceedings of the 8th International Conference on verification, model Checking, and abstract interpretation (VMCAI), Nice, France, 14\u201316 Jan 2007, pp 199\u2013213","DOI":"10.1007\/978-3-540-69738-1_14"},{"key":"221_CR40","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (1999) Vacuity detection in temporal model checking. In: Conference on correct hardware design and verification methods, pp 82\u201396","DOI":"10.1007\/3-540-48153-2_8"},{"issue":"2","key":"221_CR41","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman O, Vardi MY (2003) Vacuity detection in temporal model checking. Softw tools technol trans 4(2):224\u2013233","journal-title":"Softw tools technol trans"},{"key":"221_CR42","unstructured":"Maidl M (2000) The common fragment of CTL and LTL. In: 41st annual symposium on foundations of computer science (FOCS), Redondo Beach, California, USA, 12\u201314 Nov 2000, pp 643\u2013652"},{"issue":"1","key":"221_CR43","first-page":"38","volume":"EC\u20139","author":"R McNaughton","year":"1960","unstructured":"McNaughton R, Yamada H (1960) Regular expressions and state graphs for automata. IEEE Trans Electron Comput EC\u20139(1):38\u201347","journal-title":"IEEE Trans Electron Comput"},{"key":"221_CR44","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Mishchenko A, Brayton RK (2009) Speculative reduction-based scalable redundancy identification. In: Design, automation and test in Europe (DATE), Nice, France, 20\u201324 April 2009, pp 1674\u20131679","DOI":"10.1109\/DATE.2009.5090932"},{"key":"221_CR45","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Paruthi V, Kanzelman R (2005) Exploiting suspected redundancy without proving it. In: Proceedings of the 42nd design automation conference (DAC), San Diego, CA, USA, 13\u201317 June 2005, pp 463\u2013466","DOI":"10.1145\/1065579.1065700"},{"key":"221_CR46","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Paruthi V, Kanzelman R, Kuehlmann A (2004) Scalable automated verification via expert-system guided transformations. In: Proceedings of the 5th international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 15\u201317 Nov 2004, pp 159\u2013173","DOI":"10.1007\/978-3-540-30494-4_12"},{"key":"221_CR47","doi-asserted-by":"crossref","unstructured":"Namjoshi KS (2001) Certifying model checkers. In: Proceedings of the 13th international conference on computer aided verification (CAV), Paris, France, 18-22 July 2001, pp 2\u201313","DOI":"10.1007\/3-540-44585-4_2"},{"key":"221_CR48","doi-asserted-by":"crossref","unstructured":"Namjoshi KS (2004) An efficiently checkable, proof-based formulation of vacuity in model checking. In: Proceedings of the 16th international conference on computer aided verification (CAV), Boston, MA, USA, 13-17 July 2004, pp 57\u201369","DOI":"10.1007\/978-3-540-27813-9_5"},{"key":"221_CR49","doi-asserted-by":"crossref","unstructured":"Peled D, Pnueli A, Zuck LD (2001) From falsification to verification. In FSTTCS: Proceedings of the 21st conference on foundations of software technology and theoretical computer Science, Bangalore, India, 13-15 Dec 2001, pp 292\u2013304","DOI":"10.1007\/3-540-45294-X_25"},{"key":"221_CR50","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 Oct - 1 Nov 1977, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"221_CR51","doi-asserted-by":"crossref","unstructured":"Purandare M, Somenzi F (2002) Vacuum cleaning CTL formulae. In: Proceedings of the 14th international conference on computer aided verification (CAV), Copenhagen, Denmark, 27-31 July 2002, pp 485\u2013499","DOI":"10.1007\/3-540-45657-0_39"},{"key":"221_CR52","doi-asserted-by":"crossref","unstructured":"Purandare M, Wahl T, Kroening D (2009) Strengthening properties using abstraction refinement. In: Design, automation and test in Europe (DATE), Nice, France, 20-24 April 2009, pp 1692\u20131697","DOI":"10.1109\/DATE.2009.5090935"},{"key":"221_CR53","doi-asserted-by":"crossref","unstructured":"Quielle J, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th colloquium international symposium on programming, Torino, Italy, 6-8 April 1982, pp 337\u2013351","DOI":"10.1007\/3-540-11494-7_22"},{"key":"221_CR54","doi-asserted-by":"crossref","unstructured":"Samer M, Veith H (2004) Parameterized vacuity. In: Proceedings of the 5th international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 15-17 Nov 2004, pp 322\u2013336","DOI":"10.1007\/978-3-540-30494-4_23"},{"key":"221_CR55","doi-asserted-by":"crossref","unstructured":"Samer M, Veith H (2007) On the notion of vacuous truth. In: Proceedings of the 14th international conference on logic for programming, articial intelligence, and reasoning (LPAR), Yerevan, Armenia, 15-19 Oct 2007, pp 2\u201314","DOI":"10.1007\/978-3-540-75560-9_2"},{"key":"221_CR56","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a sat-solver. In: Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 1-3 Nov 2000, pp108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"221_CR57","doi-asserted-by":"crossref","unstructured":"Simmonds J, Davies J, Gurfinkel A, Chechik M (2007) Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: Proceedings of the 7th international conference on formal methods in computer-aided design (FMCAD), Austin, Texas, USA, 11-14 Nov 2007, pp 3\u201312","DOI":"10.1109\/FAMCAD.2007.16"},{"key":"221_CR58","unstructured":"Winkelmann K, Trylus H-J, Stoffel D, Fey G (2004) Cost-efficient block verification for a UMTS uplink chip-rate coprocessor. In: Design, automation and test in Europe conference and exposition (DATE), Paris, France, 16-20 Feb 2004, pp 162\u2013167"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0221-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0221-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0221-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T02:10:32Z","timestamp":1566267032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0221-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,29]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["221"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0221-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,29]]}}}