{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,4]],"date-time":"2022-05-04T16:35:31Z","timestamp":1651682131496},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,5,26]],"date-time":"2011-05-26T00:00:00Z","timestamp":1306368000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,10]]},"DOI":"10.1007\/s10703-011-0119-z","type":"journal-article","created":{"date-parts":[[2011,5,25]],"date-time":"2011-05-25T07:16:33Z","timestamp":1306307793000},"page":"117-143","source":"Crossref","is-referenced-by-count":1,"title":["Exploring structural symmetry automatically in symbolic trajectory evaluation"],"prefix":"10.1007","volume":"39","author":[{"given":"Yongjian","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William N. N.","family":"Hung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naiju","family":"Zeng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,26]]},"reference":[{"key":"119_CR1","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1145\/277044.277189","volume-title":"DAC \u201998: Proceedings of the 35th annual conference on design automation","author":"MD Aagaard","year":"1998","unstructured":"Aagaard MD, Jones RB, Seger C-JH (1998) Combining theorem proving and trajectory evaluation in an industrial environment. In: DAC \u201998: Proceedings of the 35th annual conference on design automation, New York, NY, USA. ACM, New York, pp 538\u2013541"},{"key":"119_CR2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/FAMCAD.2007.27","volume-title":"FMCAD \u201907: Proceedings of the formal methods in computer aided design","author":"S Adams","year":"2007","unstructured":"Adams S, Bjork M, Melham T, Seger C-J (2007) Automatic abstraction in symbolic trajectory evaluation. In: FMCAD \u201907: Proceedings of the formal methods in computer aided design, Washington, DC, USA. IEEE Computer Society, New York, pp 127\u2013135"},{"key":"119_CR3","first-page":"428","volume-title":"CAV \u201996: Proceedings of the 8th international conference on computer aided verification","author":"R Brayton","year":"1996","unstructured":"Brayton R, Hachtel GD, Sangiovanni-Vincentelli A, Somenzi F, Aziz A, Cheng ST, Edwards S (1996) Vis: a system for verification and synthesis. In: CAV \u201996: Proceedings of the 8th international conference on computer aided verification. Springer, Berlin, pp 428\u2013432"},{"issue":"1\u20132","key":"119_CR4","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Enders R, Filkorn T, Jha S (1996) Exploiting symmetry in temporal logic model checking. Form Methods Syst Des 9(1\u20132):77\u2013104","journal-title":"Form Methods Syst Des"},{"key":"119_CR5","doi-asserted-by":"crossref","unstructured":"Darbari A (2006) Symmetry reduction for STE model checking using structured models. PhD thesis, University of Oxford","DOI":"10.1109\/FMCAD.2006.31"},{"issue":"4","key":"119_CR6","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1109\/43.372367","volume":"14","author":"S Hazelhurst","year":"1995","unstructured":"Hazelhurst S, Seger C-JH (1995) A simple theorem prover based on symbolic trajectory evaluation and bdd\u2019s. IEEE Trans CAD Integr Circuits Syst 14(4):413\u2013422","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"key":"119_CR7","volume-title":"6th IEEE\/ACM international workshop on logic synthesis","author":"WNN Hung","year":"1997","unstructured":"Hung WNN, Aziz A, McMillan K (1997) Heuristic symmetry reduction for invariant verification. In: 6th IEEE\/ACM international workshop on logic synthesis, May 1997"},{"issue":"1\u20132","key":"119_CR8","first-page":"41","volume":"9","author":"CN Ip","year":"1996","unstructured":"Ip CN, Dill DL (1996) Better verification through symmetry. Form Methods Syst Des 9(1\u20132):41\u201375","journal-title":"Form Methods Syst Des"},{"key":"119_CR9","unstructured":"Li Y (2009) Formalization of symbolic trajectory semantics. http:\/\/lcs.ios.ac.cn\/~lyj238\/steSymmetry.html"},{"key":"119_CR10","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/BFb0028742","volume-title":"Proc intl conf comp-aided verific","author":"GS Manku","year":"1998","unstructured":"Manku GS, Hojati R, Brayton R (1998) Structural symmetry and model checking. In: Proc intl conf comp-aided verific, pp 159\u2013171"},{"issue":"1\u20133","key":"119_CR11","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"KL McMillan","year":"2000","unstructured":"McMillan KL (2000) A methodology for hardware verification using compositional model checking. Sci Comput Program 37(1\u20133):279\u2013309","journal-title":"Sci Comput Program"},{"key":"119_CR12","first-page":"147","volume":"Q1","author":"J O\u2019Leary","year":"1999","unstructured":"O\u2019Leary J, Zhao X, Gerth R, Seger C-JH (1999) Formally verifying IEEE compliance of floating-point hardware. Intel Technol J Q1:147\u2013190","journal-title":"Intel Technol J"},{"key":"119_CR13","unstructured":"Pandey M (1997) Formal verification of memory arrays. PhD thesis, Pittsburgh, PA, USA. Chair-Bryant, Randal E"},{"key":"119_CR14","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/266021.266056","volume-title":"DAC \u201997: Proceedings of the 34th annual design automation conference","author":"M Pandey","year":"1997","unstructured":"Pandey M, Raimi R, Bryant RE, Abadir MS (1997) Formal verification of content addressable memories using symbolic trajectory evaluation. In: DAC \u201997: Proceedings of the 34th annual design automation conference, New York, NY, USA. ACM, New York, pp 167\u2013172"},{"key":"119_CR15","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the working programmer","author":"LC Paulson","year":"1996","unstructured":"Paulson LC (1996) ML for the working programmer. Springer, Berlin. University of Cambridge Press, Cambridge"},{"issue":"2","key":"119_CR16","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C-JH Seger","year":"1995","unstructured":"Seger C-JH, Bryant RE (1995) Formal verification by symbolic evaluation of partially-ordered trajectories. Form Methods Syst Des 6(2):147\u2013189","journal-title":"Form Methods Syst Des"},{"issue":"9","key":"119_CR17","doi-asserted-by":"crossref","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C-JH Seger","year":"2005","unstructured":"Seger C-JH, Jones RB, O\u2019Leary JW, Melham T, Aagaard MD, Barrett C, Syme D (2005) An industrially effective environment for formal hardware verification. IEEE Trans Comput-Aided Des Integr Circuits Syst 24(9):1381\u20131405","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"issue":"4","key":"119_CR18","doi-asserted-by":"crossref","first-page":"702","DOI":"10.1145\/1011508.1011511","volume":"26","author":"AP Sistla","year":"2004","unstructured":"Sistla AP, Godefroid P (2004) Symmetry and reduced symmetry in model checking. ACM Trans Program Lang Syst 26(4):702\u2013734","journal-title":"ACM Trans Program Lang Syst"},{"key":"119_CR19","unstructured":"Technical Publications and Training, Intel Corporation (2003) Forte\/FL user guide edition"},{"key":"119_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"CAV","author":"R Tzoref","year":"2006","unstructured":"Tzoref R, Grumberg O (2006) Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball T, Jones RB (eds) CAV. Lecture notes in computer science, vol 4144. Springer, Berlin, pp 190\u2013204"},{"issue":"3","key":"119_CR21","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1109\/TVLSI.2003.812320","volume":"11","author":"J Yang","year":"2003","unstructured":"Yang J, Seger C-JH (2003) Introduction to generalized symbolic trajectory evaluation. IEEE Trans VLSI Syst 11(3):345\u2013353","journal-title":"IEEE Trans VLSI Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0119-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0119-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0119-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T00:48:49Z","timestamp":1560214129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0119-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,26]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["119"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0119-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,26]]}}}