{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T05:56:09Z","timestamp":1721627769310},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,8,15]],"date-time":"2014-08-15T00:00:00Z","timestamp":1408060800000},"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":[[2014,10]]},"DOI":"10.1007\/s10703-014-0213-0","type":"journal-article","created":{"date-parts":[[2014,8,14]],"date-time":"2014-08-14T04:57:27Z","timestamp":1407992247000},"page":"144-164","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Scalable reachability analysis via automated dynamic netlist-based hint generation"],"prefix":"10.1007","volume":"45","author":[{"given":"Jiazhao","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Williams","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hari","family":"Mony","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason","family":"Baumgartner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,8,15]]},"reference":[{"key":"213_CR1","unstructured":"Burch JR, Clarke EM, Long DE (August 1991) Symbolic model checking with partitioned transition relations. In: International conference on very large scale integration, pp 49\u201358"},{"key":"213_CR2","doi-asserted-by":"crossref","unstructured":"Moon I-H, Hachtel GD, Somenzi F (November 2000) \u2018Border-block triangular form and conjunction schedule in image computation. In: International conference on formal methods in computer-aided design, pp 73\u201390","DOI":"10.1007\/3-540-40922-X_6"},{"key":"213_CR3","doi-asserted-by":"crossref","unstructured":"McMillan K (July 2003) Interpolation and SAT-based model checking. In: International conference on computer-aided verification, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"213_CR4","doi-asserted-by":"crossref","unstructured":"Bradley A (2011) SAT-based model checking without unrolling. In: International conference on verification, model checking, and abstract interpretation, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"213_CR5","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for the construction and analysis of systems, pp 193\u2013207","DOI":"10.21236\/ADA360973"},{"key":"213_CR6","unstructured":"Ho P-H, Shiple T, Harer K, Kukula J, Damiano R, Bertacco V, Taylor J, Long J (2000) Smart simulation using collaborative formal and simulation engines. In: International conference on computer-aided design, pp 120\u2013126"},{"key":"213_CR7","unstructured":"Moon I-H, Kukula JH, Ravi K, Somenzi F (2000) To split or to conjoin: the question in image computation. In: Proceedings of the 37th Annual Design Automation Conference, ACM, pp 23\u201328"},{"key":"213_CR8","doi-asserted-by":"crossref","unstructured":"Clarke E M, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: International conference on computer-aided verification, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"213_CR9","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Mishchenko A, Brayton R (2009) Speculative reduction-based scalable redundancy identification. In: Design, automation and test in Europe, pp 1674\u20131679","DOI":"10.1109\/DATE.2009.5090932"},{"key":"213_CR10","doi-asserted-by":"crossref","unstructured":"Bjesse P, Kukula J (2005) Automatic generalized phase abstraction for formal verification. In: International conference on computer-aided design, pp 1076\u20131082","DOI":"10.1109\/ICCAD.2005.1560220"},{"key":"213_CR11","doi-asserted-by":"crossref","unstructured":"Kuehlmann A, Baumgartner J (2001) Transformation-based verification using generalized retiming. In: International conference on computer-aided verification, pp 104\u2013117","DOI":"10.1007\/3-540-44585-4_10"},{"key":"213_CR12","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: International conference on formal methods in computer-aided design, pp 159\u2013173","DOI":"10.1007\/978-3-540-30494-4_12"},{"key":"213_CR13","unstructured":"Berkeley Logic and Synthesis Group, ABC: A System for Sequential Synthesis and Verification. http:\/\/www.eecs.berkeley.edu\/alanmi\/abc"},{"issue":"2","key":"213_CR14","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Form Methods Syst Des 39(2):205\u2013227","journal-title":"Form Methods Syst Des"},{"key":"213_CR15","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/43.822619","volume":"19","author":"PA Beerel","year":"2000","unstructured":"Beerel PA, Burch JR, McMillan KL (2000) Sibling-substitution-based BDD minimization using don\u2019t cares. IEEE Trans Comput Aided Des 19:44\u201355","journal-title":"IEEE Trans Comput Aided Des"},{"key":"213_CR16","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1999) Hints to accelerate symbolic traversal. In: Correct hardware design and verification methods, pp 250\u2013266","DOI":"10.1007\/3-540-48153-2_19"},{"key":"213_CR17","doi-asserted-by":"crossref","unstructured":"Ward D, Somenzi F (2005) Automatic generation of hints for symbolic traversal. In: Correct hardware design and verification methods, pp 207\u2013221","DOI":"10.1007\/11560548_17"},{"key":"213_CR18","unstructured":"Ward D, Somenzi F (2006) Decomposing image computation for symbolic reachability analysis using control flow information. In: International conference on computer-aided design, pp 779\u2013785"},{"key":"213_CR19","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1995) High-density reachability analysis. In: International conference on computer-aided design, pp 154\u2013158","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"213_CR20","unstructured":"Hardware Model Checking Competition 2011. http:\/\/fmv.jku.at\/hwmcc11 . Accessed Nov 2011"},{"key":"213_CR21","unstructured":"Janssen G (2001) Design of a pointerless BDD package. In: International workshop on logic synthesis"},{"key":"213_CR22","doi-asserted-by":"crossref","unstructured":"Fujii H, Ootomo G, Hori C (1993) Interleaving based variable ordering methods for ordered binary decision diagrams. In: International conference on computer-aided design, pp 38\u201341","DOI":"10.1109\/ICCAD.1993.580028"},{"key":"213_CR23","doi-asserted-by":"crossref","unstructured":"Jin H, Kuehlmann A, Somenzi F (2002) Fine-grain conjunction scheduling for symbolic reachability analysis. In: Tools and algorithms for the construction and analysis of systems, pp 312\u2013326","DOI":"10.1007\/3-540-46002-0_22"},{"key":"213_CR24","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rennson N (2003) Temporal induction by incremental SAT solving. In: Workshop on bounded model checking","DOI":"10.1016\/S1571-0661(05)82542-3"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0213-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0213-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-0213-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T18:28:58Z","timestamp":1565720938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0213-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,15]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["213"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0213-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,15]]}}}