{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:35Z","timestamp":1749318095235},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115632","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T17:03:57Z","timestamp":1511456637000},"page":"194-199","source":"Crossref","is-referenced-by-count":11,"title":["Proof-based coverage metrics for formal verification"],"prefix":"10.1109","author":[{"given":"Elaheh","family":"Ghassabani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","article-title":"Automating DO-178C objectives with SpeAR: A case study","author":"wagner","year":"2017","journal-title":"Safe and Secure Systems and Software Symposium (S5) AFRL"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.39"},{"journal-title":"Software Considerations in Airborne Systems and Equipment Certification","article-title":"RTCA\/DO-178C","year":"0","key":"ref30"},{"key":"ref10","article-title":"Formal methods for analyzing the completeness of an assertion suite against a high-level fault model","author":"das","year":"0","journal-title":"vlsid"},{"key":"ref11","article-title":"Efficient implementation of property directed reachability","author":"een","year":"2011","journal-title":"FMCAD'11"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950346"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364454"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"ref17","doi-asserted-by":"crossref","DOI":"10.1109\/5.97300","article-title":"The Synchronous Dataflow Programming Language Lustre","author":"halbwachs","year":"1991","journal-title":"Proceedings of the IEEE"},{"journal-title":"Formal verification coverage metrics for circuit design properties","year":"2015","author":"hanna","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_14"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837320"},{"journal-title":"Software Model Checking Takes off","year":"2010","author":"miller","key":"ref27"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.83"},{"key":"ref6","article-title":"Coverage metrics for formal verification","author":"chockler","year":"2003","journal-title":"CHARME"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2016.35"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_7"},{"key":"ref8","first-page":"52","article-title":"A liveness checking algorithm that counts","author":"claessen","year":"2012","journal-title":"FMCAD"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.32"},{"journal-title":"Tools and Experimental Results","year":"0","key":"ref2"},{"key":"ref9","article-title":"Compositional verification of architectural models","author":"cofer","year":"2012","journal-title":"NFM'12"},{"year":"0","key":"ref1"},{"key":"ref20","article-title":"Deviation analysis via model checking","author":"heimdahl","year":"2002","journal-title":"ASE 02"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_15"},{"key":"ref21","article-title":"Coverage estimation for symbolic model checking","author":"hoskote","year":"0","journal-title":"DAC"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_3"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_21"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.29"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","start":{"date-parts":[[2017,10,30]]},"location":"Urbana, IL","end":{"date-parts":[[2017,11,3]]}},"container-title":["2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8106906\/8115603\/08115632.pdf?arnumber=8115632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T14:31:39Z","timestamp":1570372299000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115632\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115632","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}