{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:31Z","timestamp":1774440331240,"version":"3.50.1"},"reference-count":57,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[2016,8,1]],"date-time":"2016-08-01T00:00:00Z","timestamp":1470009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"University Research Board"},{"DOI":"10.13039\/100007688","name":"American University of Beirut","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007688","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2016,8,1]]},"DOI":"10.1109\/tse.2016.2520468","type":"journal-article","created":{"date-parts":[[2016,1,21]],"date-time":"2016-01-21T14:56:18Z","timestamp":1453388178000},"page":"741-763","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Software with First Order Logic Specifications Using AIG Solvers"],"prefix":"10.1109","volume":"42","author":[{"given":"Mohammad A.","family":"Noureddine","sequence":"first","affiliation":[]},{"given":"Fadi A.","family":"Zaraket","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"ref32","first-page":"146","article-title":"Bounded model checking of software using SMT solvers instead of SAT solvers","author":"arm","year":"0","journal-title":"Proc International SPIN Workshop on Model Checking of Software"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.31"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.307"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681580"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_32"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.07.005"},{"key":"ref28","first-page":"1108","article-title":"Considering circuit observability don't cares in CNF satisfiability","author":"fu","year":"0","journal-title":"Proc Des Autom Test Eur"},{"key":"ref27","first-page":"731","article-title":"Solving difficult SAT instances in the presence of symmetry","author":"aloul","year":"0","journal-title":"Proc 39th Des Autom Conf"},{"key":"ref29","first-page":"229","article-title":"SAT sweeping with local observability dontcares","author":"zhu","year":"0","journal-title":"Proc 43rd IEEE\/ACM Des Autom Conf"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"ref20","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"een","year":"0","journal-title":"Proc Int Conf Formal Methods Comput -Aided Des"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_13"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_12"},{"key":"ref23","first-page":"120","article-title":"Smart simulation using collaborative formal and simulation engines","author":"ho","year":"0","journal-title":"Proc IEEE\/ACM Int Conf Comput -Aided Des"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_20"},{"key":"ref50","first-page":"2002","author":"nipkow","year":"0","journal-title":"Isabelle\/HOLA Proof Assistant for Higher-Order Logic"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_7"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_14"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_40"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36046-6_1"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693138"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref11","author":"bybell","year":"0"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_10"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065700"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_23"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016043502772"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref19","article-title":"SAT based abstraction refinement for hardware verification","author":"wang","year":"2003"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"ref3","first-page":"405","article-title":"ESBMC 1.22 - (competition contribution)","author":"morse","year":"2014","journal-title":"Proc Conf Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.75"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"ref8","first-page":"159","article-title":"Scalable automated verification via expert-system guided transformations","author":"baumgartner","year":"0","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321650"},{"key":"ref49","article-title":"$Z3^{10}$ : Applications, enablers, challenges and directions","author":"bjrner","year":"0","journal-title":"Proc Int Workshop Constraints Formal Verification (CFV)"},{"key":"ref9","first-page":"1","article-title":"MiniSAT v1. 13-a sat solver with conflict-clause minimization","author":"sorensson","year":"2005","journal-title":"System description for the SAT competition"},{"key":"ref46","first-page":"15","article-title":"Combining unit-level symbolic execution and system-level concrete execution for testing nasa software","author":"p?s?reanu","year":"0","journal-title":"Proc Int'l Symp on Softw Testing and Analysis"},{"key":"ref45","author":"baudin","year":"0","journal-title":"ACSL ANSI C Specification Language (Preliminary Design V1 2)"},{"key":"ref48","article-title":"A toolbox for counter-example analysis and optimization","author":"mishchenko","year":"0","journal-title":"Int Workshop on Logic Synthesis (IWLS)"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250705"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref44","author":"cormen","year":"2009","journal-title":"Introduction to Algorithms"},{"key":"ref43","author":"bradley","year":"2007","journal-title":"The calculus of computation decision procedures with applications to verification"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/7542210\/07389426.pdf?arnumber=7389426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:43:36Z","timestamp":1641987816000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7389426\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,1]]},"references-count":57,"journal-issue":{"issue":"8"},"URL":"https:\/\/doi.org\/10.1109\/tse.2016.2520468","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,8,1]]}}}