{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T17:18:15Z","timestamp":1730222295020,"version":"3.28.0"},"reference-count":31,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,11]]},"DOI":"10.1109\/fmcad.2009.5351149","type":"proceedings-article","created":{"date-parts":[[2009,12,11]],"date-time":"2009-12-11T18:55:16Z","timestamp":1260557716000},"page":"9-16","source":"Crossref","is-referenced-by-count":6,"title":["Structure-aware computation of predicate abstraction"],"prefix":"10.1109","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Jori","family":"Dubrovin","sequence":"additional","affiliation":[]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"year":"0","key":"17"},{"year":"0","key":"18"},{"key":"15","first-page":"49","article-title":"Symbolic model checking with partitioned transition relations","author":"burch","year":"1991","journal-title":"ser IFIP Transactions"},{"key":"16","article-title":"Efficient BDD algorithms for FSM synthesis and verification","author":"ranjan","year":"1995","journal-title":"Proc Int Workshop Logic Synthesis"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"journal-title":"HyTech The HYbrid TECHnology tool","year":"0","key":"14"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"20","article-title":"Hybrid BDD and All-SAT Method for Model Checking","author":"grumberg","year":"2006","journal-title":"Symposium on Satisfiability Solvers and Program Verification (SSPV)"},{"year":"0","key":"22"},{"year":"0","key":"23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364481"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"26","first-page":"570","article-title":"SATABS: SAT-based predicate abstraction for ANSI-C","volume":"3440","author":"clarke","year":"2005","journal-title":"ser LNCS"},{"key":"27","first-page":"433","article-title":"Abstraction and counterexample-guided construction of ?-automata for model checking of step-discrete linear hybrid models","volume":"4590","author":"segelken","year":"2007","journal-title":"ser LNCS"},{"key":"28","first-page":"107","article-title":"Sat-based abstraction refinement for realtime systems","volume":"182","author":"kemper","year":"2007","journal-title":"ENTCS"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403578"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065697"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.026"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"year":"0","key":"30"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.35"},{"year":"0","key":"6"},{"key":"5","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"year":"0","key":"31"},{"year":"0","key":"4"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"}],"event":{"name":"2009 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2009,11,15]]},"location":"Austin, TX, USA","end":{"date-parts":[[2009,11,18]]}},"container-title":["2009 Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5344684\/5351113\/05351149.pdf?arnumber=5351149","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,19]],"date-time":"2017-03-19T02:09:14Z","timestamp":1489889354000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5351149\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2009.5351149","relation":{},"subject":[],"published":{"date-parts":[[2009,11]]}}}