{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T09:07:13Z","timestamp":1648890433315},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,1,25]],"date-time":"2005-01-25T00:00:00Z","timestamp":1106611200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10009-004-0172-7","type":"journal-article","created":{"date-parts":[[2005,1,24]],"date-time":"2005-01-24T15:01:13Z","timestamp":1106578873000},"page":"129-142","source":"Crossref","is-referenced-by-count":2,"title":["Are BDDs still alive within sequential verification?"],"prefix":"10.1007","volume":"7","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,1,25]]},"reference":[{"key":"172_CR1","doi-asserted-by":"crossref","unstructured":"Cabodi G (2001) Meta-BDDs: a decomposed representation for layered symbolic manipulation of Boolean functions. In: Berry G, Comon H, Finkel A (eds) Proc. 17th conference international conference on computer-aided verification, Paris, July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 118\u2013130","DOI":"10.1007\/3-540-44585-4_11"},{"key":"172_CR2","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (1994) Efficient state space pruning in symbolic backward traversal. In: Proc. international conference on computer design, Cambridge, MA, October 1994, pp 230\u2013235","DOI":"10.1109\/ICCD.1994.331895"},{"key":"172_CR3","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (1999) Improving the efficiency of BDD\u2013based operators by means of partitioning. IEEE Trans Comput-Aided Des 18(5):545\u2013556","DOI":"10.1109\/43.759068"},{"key":"172_CR4","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (2000) Improving symbolic reachability analysis by means of activity profiles. IEEE Trans Comput-Aided Des 19(9):1065\u20131075","DOI":"10.1109\/43.863646"},{"key":"172_CR5","doi-asserted-by":"crossref","first-page":"1137","DOI":"10.1016\/S1383-7621(00)00014-X","volume":"46","author":"Cabodi","year":"2000","unstructured":"Cabodi G, Camurati P, Quer S (2000) Symbolic forward\/backward traversals of large finite state machines. J Syst Architect EUROMICRO J 46(12):1137\u20131158","journal-title":"J Syst Architect EUROMICRO J"},{"key":"172_CR6","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (2002) Can BDDs compete with SAT solvers on bounded model checking? In: Proc. 39th conference on design automation, New Orleans, June 2002","DOI":"10.1109\/DAC.2002.1012605"},{"key":"172_CR7","doi-asserted-by":"crossref","unstructured":"Cabodi G, Nocco S, Quer S (2002) Mixing forward and backward traversals in guided-prioritized BDD-based verification. In: Brinksma E, Larsen KG (eds) Proc. international conference on computer-aided verification, Copenhagen, Denmark, July 2002. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 471\u2013484","DOI":"10.1007\/3-540-45657-0_38"},{"key":"172_CR8","unstructured":"Cabodi G, Nocco S, Quer S (2005) Improving SAT-based bounded model checking by means of BDD-based approximate traversals. J Universal Comput Sci (in press)"},{"key":"172_CR9","doi-asserted-by":"crossref","unstructured":"Chauhan P, Clarke E, Kukula J, Sapra S, Veith H, Wang D (2002) Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard MD, O\u2019Leary JW (eds) Proc. 4th international conference on formal methods in computer-aided design, November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp\u200935\u201351","DOI":"10.1007\/3-540-36126-X_3"},{"key":"172_CR10","doi-asserted-by":"crossref","unstructured":"Cho H, Hatchel GD, Macii E, Plessier B, Somenzi F (1996) Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans Comput-Aided Des 15(12):1465\u20131478","DOI":"10.1109\/43.552080"},{"key":"172_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Proc. 13th international conference on computer-aided verification, July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp\u2009495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"172_CR12","doi-asserted-by":"crossref","unstructured":"Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi MY (2001) Benefits of bounded model checking at an industrial setting. In: Berry G, Comon H, Finkel A (eds) Proc. 17th international conference on computer-aided verification, Paris, July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp\u2009435\u2013453","DOI":"10.1007\/3-540-44585-4_43"},{"key":"172_CR13","doi-asserted-by":"crossref","unstructured":"Brayton RK, Hachtel GD, Sangiovanni-Vincentelli A, Somenzi F, Aziz A, Cheng S-T, Edwards SA, Khatri SP, Kuykimoto Y, Pardo A, Qadeer Q, Ranjan RK, Sarwary A, Shiple TR, Swamy G, Villa T (1996) VIS. In: Srivas M, Camilleri A (eds) Proc. international conference on formal methods in computer-aided design, Palo Alto, CA, November 1996. Lecture notes in computer science, vol 1166. Springer, Berlin Heidelberg New York, pp\u2009248\u2013256","DOI":"10.1007\/BFb0031812"},{"key":"172_CR14","doi-asserted-by":"crossref","unstructured":"Fraer R, Kamhi G, Ziv B, Vardi MY, Fix L (2000) Prioritized traversal: efficient reachability analysis for verification and falsification. In: Emerson EA, Prasad Sistla A (eds) Proc. 12th international conference on computer-aided verification, Chicago, July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp\u2009389\u2013402","DOI":"10.1007\/10722167_30"},{"key":"172_CR15","doi-asserted-by":"crossref","unstructured":"Ganai MK, Aziz A, Kuehlmann A (1999) Enhancing simulation with BDDs and ATPG. In: Proc. 36th conference on design automation, New Orleans, November 1999, pp\u2009385\u2013390","DOI":"10.1109\/DAC.1999.781346"},{"key":"172_CR16","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT-solver. In: Proc. Design, Automation and Test in Europe, Paris, February 2002, pp\u2009142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"172_CR17","doi-asserted-by":"crossref","unstructured":"Govindaraju SG, Dill DL (1998) Verification by approximate forward and backward reachability. In: Proc. international conference on computer-aided design, San Jose, CA, November 1998, pp\u2009366\u2013370","DOI":"10.1145\/288548.289055"},{"key":"172_CR18","unstructured":"IBM Formal Verification Benchmark Library. http:\/\/www.haifa.il.ibm.com\/projects\/verification\/rb_homepage\/fvbenchmarks.html"},{"key":"172_CR19","doi-asserted-by":"crossref","unstructured":"Moon I, Jang J, Hachtel GD, Somenzi F, Yuan J, Pixley C (1998) Approximate reachability don\u2019t cares for CTL model checking. In: Proc. international conference on computer-aided design, San Jose, CA, November 1998, pp\u2009351\u2013358","DOI":"10.1145\/288548.289053"},{"key":"172_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proc. 38th conference on design automation, Las Vegas, June 2001","DOI":"10.1145\/378239.379017"},{"key":"172_CR21","doi-asserted-by":"crossref","unstructured":"Narayan A, Isles AJ, Jain J, Brayton RK, Sangiovanni-Vincentelli A (1997) Reachability analysis using partitioned\u2013ROBDDs. In: Proc. international conference on computer-aided design, San Jose, CA, November 1997, pp\u2009388\u2013393","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"172_CR22","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1995) High-density reachability analysis. In: Proc. international conference on computer-aided design, San Jose, CA, November, pp\u2009154\u2013158","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"172_CR23","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1999) Hints to accelerate symbolic traversal. In: conference on correct hardware design and verification methods (CHARME\u201999), Berlin, September 1999. Lecture notes in computer science, vol 1703. Springer, Berlin Heidelberg New York, pp\u2009250\u2013264","DOI":"10.1007\/3-540-48153-2_19"},{"key":"172_CR24","unstructured":"Ryan L (2003) Siege SAT Solver. http:\/\/www.cs.sfu.ca\/\u223cloryan\/personal\/"},{"key":"172_CR25","doi-asserted-by":"crossref","unstructured":"Wang D, Ho P, Long J, Kukula J, Zhu Y, Ma T, Damiano R (2001) Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Proc. 38th conference on design automation, Las Vegas, June 2001","DOI":"10.1145\/378239.378260"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0172-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0172-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0172-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:20Z","timestamp":1559114720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0172-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,25]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["172"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0172-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1,25]]}}}