{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:24:20Z","timestamp":1763724260875},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,1,7]],"date-time":"2012-01-07T00:00:00Z","timestamp":1325894400000},"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":[[2012,4]]},"DOI":"10.1007\/s10703-011-0134-0","type":"journal-article","created":{"date-parts":[[2012,1,6]],"date-time":"2012-01-06T08:01:01Z","timestamp":1325836861000},"page":"147-169","source":"Crossref","is-referenced-by-count":15,"title":["Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics"],"prefix":"10.1007","volume":"40","author":[{"given":"Satrajit","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kishinevsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,7]]},"reference":[{"key":"134_CR1","first-page":"120","volume-title":"MCAD 2009","author":"J Baumgartner","year":"2009","unstructured":"Baumgartner J et al. (2009) Scalable conditional equivalence checking: An automated invariant-generation based approach. In: MCAD 2009, pp 120\u2013127"},{"issue":"1","key":"134_CR2","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste A et al. (2003) The synchronous language twelve years later. Proc IEEE 91(1):64\u201383","journal-title":"Proc IEEE"},{"key":"134_CR3","unstructured":"Berkeley Logic Synthesis Group. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"issue":"1","key":"134_CR4","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner N, Browne A, Manna Z (1997) Automatic generation of invariants and intermediate assertions. Theor Comput Sci 173(1):49\u201387","journal-title":"Theor Comput Sci"},{"key":"134_CR5","first-page":"70","volume-title":"VMCAI 2011","author":"AR Bradley","year":"2011","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI 2011, pp 70\u201387"},{"key":"134_CR6","first-page":"42","volume-title":"HLDVT 2010","author":"S Chatterjee","year":"2010","unstructured":"Chatterjee S, Kishinevsky M, Ogras UY (2010) Quick formal modeling of communication fabrics to enable verification. In: HLDVT 2010, pp 42\u201349"},{"key":"134_CR7","first-page":"79","volume-title":"Proc. of Appl. and Theory of Petri Nets","author":"JM Colom","year":"1991","unstructured":"Colom JM, Silva M (1991) Convex geometry and semiflows in P\/T nets. In: Proc. of Appl. and Theory of Petri Nets, pp 79\u2013112"},{"key":"134_CR8","volume-title":"Introduction to algorithms","author":"TH Corman","year":"1990","unstructured":"Corman TH et al. (1990) Introduction to algorithms, 2nd edn. MIT Press, Cambridge","edition":"2"},{"key":"134_CR9","volume-title":"Principles and practices of interconnection networks","author":"WJ Dally","year":"2004","unstructured":"Dally WJ, Towles B (2004) Principles and practices of interconnection networks. Morgan Kaufmann, San Mateo"},{"key":"134_CR10","unstructured":"E\u00e9n N, Mishchenko A, Brayton R (2011) Efficient implementation of property directed reachability, IWLS\u201911"},{"key":"134_CR11","first-page":"214","volume-title":"VMCAI 2011","author":"A Gotmanov","year":"2011","unstructured":"Gotmanov A, Chatterjee S, Kishinevsky M (2011) Verifying deadlock freedom of communication fabrics. In: VMCAI 2011, pp 214\u2013231"},{"issue":"10","key":"134_CR12","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580, 583","journal-title":"Commun ACM"},{"key":"134_CR13","first-page":"396","volume-title":"CAV 2011","author":"R Jhala","year":"2001","unstructured":"Jhala R, McMillan KL (2001) Microarchitecture verification by compositional model checking. In: CAV 2011, pp 396\u2013410"},{"key":"134_CR14","first-page":"414","volume-title":"CAV 2009","author":"R Kaivola","year":"2009","unstructured":"Kaivola R et al. (2009) Replacing testing with formal verification in Intel Core i7 processor execution engine validation. In: CAV 2009, pp 414\u2013429"},{"key":"134_CR15","series-title":"LNCS","volume-title":"FMCAD 2000","author":"M Sheeran","year":"2000","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: FMCAD 2000. LNCS, vol 1954."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0134-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0134-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0134-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:52Z","timestamp":1559239552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0134-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,7]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["134"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0134-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,7]]}}}