{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:00:02Z","timestamp":1740132002020,"version":"3.37.3"},"reference-count":95,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"2","license":[{"start":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T00:00:00Z","timestamp":1612137600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T00:00:00Z","timestamp":1612137600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T00:00:00Z","timestamp":1612137600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"DARPA Systems of Systems Integration Technology and Experimentation","award":["FA8650-16-C-7656"],"award-info":[{"award-number":["FA8650-16-C-7656"]}]},{"name":"NASA Compositional Verification of Flight-Critical Systems","award":["NNA13AA21C"],"award-info":[{"award-number":["NNA13AA21C"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2021,2,1]]},"DOI":"10.1109\/tse.2019.2891709","type":"journal-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T19:54:47Z","timestamp":1547063687000},"page":"279-299","source":"Crossref","is-referenced-by-count":1,"title":["Inductive Validity Cores"],"prefix":"10.1109","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3968-8610","authenticated-orcid":false,"given":"Elaheh","family":"Ghassabani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mats","family":"Heimdahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2010.11"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_14"},{"key":"ref71","first-page":"174","article-title":"Faster extraction of high-level minimal unsatisfiable cores","author":"ryvchin","year":"2011","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-2012-0523"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/VLSISoC.2011.6081636"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9084-z"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"ref39","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","article-title":"Compositional verification of architectural models","author":"cofer","year":"2012","journal-title":"Proc 4th NASA Formal Methods Symp"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_2"},{"article-title":"Inductive validity cores","year":"2018","author":"ghassabani","key":"ref38"},{"key":"ref78","first-page":"174","article-title":"Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization","author":"bailey","year":"2005","journal-title":"Proc 7th Int Conf Practical Aspects Declarative Lang"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3098239"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_15"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9146-2"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"ref36","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","article-title":"The MathSAT5 SMT solver","author":"cimatti","year":"2013","journal-title":"Proc 19th Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref35","first-page":"1","article-title":"The YICES SMT solver","volume":"2","author":"dutertre","year":"2006","journal-title":"Tool paper"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref60","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","article-title":"A practical approach to coverage in model checking","author":"chockler","year":"2001","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.32"},{"key":"ref61","first-page":"201","article-title":"Formal methods for analyzing the completeness of an assertion suite against a high-level fault model","author":"das","year":"2005","journal-title":"Proc 18th Int Conf VLSI Des Held Jointly With 4th Int Conf Embedded Syst Des"},{"key":"ref63","first-page":"1176","article-title":"Estimating functional coverage in bounded model checking","author":"gro\u00dfe","year":"2007","journal-title":"Proc Conf Des Autom Test Eur"},{"key":"ref28","first-page":"20","article-title":"The JKind model checker","author":"gacek","year":"2018","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837320"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2002.1114992"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_3"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693070"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9183-0"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_32"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190100"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.288"},{"key":"ref2","first-page":"127","article-title":"Checking safety properties using induction and a sat-solver","author":"sheeran","year":"2000","journal-title":"Proc Int Conf Formal Methods Comput -Aided Des"},{"key":"ref1","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"een","year":"2011","journal-title":"Proc Int Conf Formal Methods Comput -Aided Des"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950346"},{"year":"2015","key":"ref21","article-title":"MathWorks Inc. Simulink Design Verifier"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115632"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2016.35"},{"key":"ref26","first-page":"117","article-title":"Proof certificates for smt-based model checkers for infinite-state systems","author":"mebsout","year":"2016","journal-title":"Proc 16th Conf Formal Methods Comput -Aided Des"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2002.1115010"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2007.195"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.32"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_20"},{"key":"ref92","first-page":"279","author":"beer","year":"1997","journal-title":"Proc 9th Int Conf Comput Aided Verification"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_12"},{"key":"ref59","first-page":"266","article-title":"Development of security software: A high-assurance methodology","author":"hardin","year":"2009","journal-title":"Proc 11th Int Conf Formal Eng Methods"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.39"},{"key":"ref57","article-title":"Automating DO-178C objectives with SpeAR: A case study","author":"wagner","year":"2017","journal-title":"Proc Safe Secure Syst Softw Symp"},{"year":"0","key":"ref56","article-title":"Formal methods supplement to DO-178C and and DO-278A"},{"key":"ref55","first-page":"144","article-title":"Automated analysis of stateflow models","author":"bourbouh","year":"2017","journal-title":"Proc 21st Int Conf Logic Program Artif Intell Reasoning"},{"year":"0","key":"ref54","article-title":"imulink - simulation and model-based design"},{"year":"2018","key":"ref53","article-title":"Esterel-Technologies, “SCADE Suite product description"},{"key":"ref52","first-page":"102","article-title":"Will it work? [requirements engineering]","author":"hammond","year":"2001","journal-title":"Proc 5th IEEE Int Symp Requirements Eng"},{"key":"ref10","first-page":"68","article-title":"Integration of formal analysis into a model-based software development process","author":"whalen","year":"2007","journal-title":"Proc Int Workshop Formal Methods Ind Critical Syst"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.41"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","article-title":"Requirements analysis of a quad-redundant flight control system","volume":"9058","author":"backes","year":"2015","journal-title":"NASA Formal Methods"},{"key":"ref12","article-title":"Extracting small unsatisfiable cores from unsatisfiable boolean formula","author":"zhang","year":"0","journal-title":"SAT '03"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_23"},{"year":"0","key":"ref14","article-title":"Cadence JasperGold Formal Verification Platform"},{"year":"0","key":"ref15","article-title":"RTCA\/DO-178C, “Software considerations in airborne systems and equipment certification."},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987603"},{"year":"1997","key":"ref16","article-title":"Requirements for Safety Related Software in Defence Equipment, Issue 2"},{"key":"ref81","first-page":"50:1","article-title":"Tunable online MUS\/MSS enumeration","author":"bend\u00edk","year":"2016","journal-title":"Proc 36th IARCS Annu Conf Found Softw Technol Theoretical Comput Sci"},{"year":"2016","key":"ref17","article-title":"MathWorks Inc. Simulink Requirements Traceability"},{"year":"0","key":"ref84","article-title":"Synopsys VC Formal Platform"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227244"},{"article-title":"Formal verification coverage metrics for circuit design properties","year":"2014","author":"hanna","key":"ref83"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-540-39724-3_11","article-title":"Coverage metrics for formal verification","volume":"lncs 2860","author":"chockler","year":"2003","journal-title":"Correct Hardware Des Verification Methods"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41591-8_9"},{"key":"ref89","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10703-008-0060-y","article-title":"Before and after vacuity","volume":"34","author":"chockler","year":"2008","journal-title":"Formal Methods Syst Des"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"ref3","first-page":"52","article-title":"A liveness checking algorithm that counts","author":"claessen","year":"2012","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"article-title":"A methodology for hardware verification using compositional model checking","year":"1999","author":"mcmillan","key":"ref5"},{"key":"ref85","first-page":"439","article-title":"Program slicing","author":"weiser","year":"1981","journal-title":"5th Int Conf on Software Engineering"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2015.7381816"},{"key":"ref86","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1145\/93548.93576","article-title":"Dynamic program slicing","volume":"25","author":"agrawal","year":"1990","journal-title":"ACM SIGPLAN Notices"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606556"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/ICRE.2003.1232745"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000008668.12782.6c"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071369"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/ICRE.1994.292398"},{"key":"ref45","article-title":"Slicing lustre programs","author":"gaucher","year":"2003","journal-title":"Tech Rep"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/237432.237434"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2239-5_1"},{"key":"ref42","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","article-title":"Requirements analysis of a quad-redundant flight control system","volume":"9058","author":"backes","year":"2015","journal-title":"NASA Formal Methods"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"ref44","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"tip","year":"1995","journal-title":"J Program Lang"},{"year":"0","key":"ref43","article-title":"IVCs repository"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9352984\/08606278.pdf?arnumber=8606278","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T14:50:09Z","timestamp":1652194209000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8606278\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,1]]},"references-count":95,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.1109\/tse.2019.2891709","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2021,2,1]]}}}