{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T15:15:01Z","timestamp":1725808501318},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319133379"},{"type":"electronic","value":"9783319133386"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13338-6_5","type":"book-chapter","created":{"date-parts":[[2014,11,2]],"date-time":"2014-11-02T22:35:45Z","timestamp":1414967745000},"page":"54-67","source":"Crossref","is-referenced-by-count":0,"title":["Generating Modulo-2 Linear Invariants for Hardware Model Checking"],"prefix":"10.1007","author":[{"given":"Gadi","family":"Aleksandrowicz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Ivrii","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Margalit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dan","family":"Rasin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Aleksandrowicz, G., Ivrii, A., Margalit, O., Rasin, D.: Generating modulo-2 linear invariants for hardware model checking. Full version with appendix, available at \n                  \n                    http:\/\/researcher.watson.ibm.com\/researcher\/files\/il-ALEXI\/xor.pdf"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: A sat-based algorithm for reparameterization in symbolic simulation. In: DAC, pp. 524\u2013529 (2004)","DOI":"10.21236\/ADA461257"},{"key":"5_CR4","unstructured":"Case, M.L., Mishchenko, A., Brayton, R.K.: Inductively finding a reachable state space over-approximation. In: IWLS (2006)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Case, M.L., Mishchenko, A., Brayton, R.K.: Automated extraction of inductive invariants to aid model checking. In: FMCAD, pp. 165\u2013172 (2007)","DOI":"10.1109\/FMCAD.2007.4401996"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Boosting the role of inductive invariants in model checking. In: DATE, pp. 1319\u20131324 (2007)","DOI":"10.1109\/DATE.2007.364480"},{"key":"5_CR7","unstructured":"CryptoMiniSat, \n                  \n                    http:\/\/www.msoos.org\/cryptominisat2\/"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-02658-4_23","volume-title":"Computer Aided Verification","author":"O. Fuhrmann","year":"2009","unstructured":"Fuhrmann, O., Hoory, S.: On extending bounded proofs to inductive proofs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 278\u2013290. Springer, Heidelberg (2009)"},{"key":"5_CR10","unstructured":"Hardware Model Checking Competition (2011), \n                  \n                    http:\/\/fmv.jku.at\/hwmcc11"},{"key":"5_CR11","unstructured":"Hardware Model Checking Competition (2013), \n                  \n                    http:\/\/fmv.jku.at\/hwmcc13"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-70545-1_26","volume-title":"Computer Aided Verification","author":"A. King","year":"2008","unstructured":"King, A., S\u00f8ndergaard, H.: Inferring congruence equations using SAT. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 281\u2013293. Springer, Heidelberg (2008)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-11319-2_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. King","year":"2010","unstructured":"King, A., S\u00f8ndergaard, H.: Automatic abstraction for congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Mishchenko, A., Brayton, R.K.: Speculative reduction-based scalable redundancy identification. In: DATE, pp. 1674\u20131679 (2009)","DOI":"10.1109\/DATE.2009.5090932"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-30494-4_12","volume-title":"Formal Methods in Computer-Aided Design","author":"H. Mony","year":"2004","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 159\u2013173. Springer, Heidelberg (2004)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275504"},{"issue":"7","key":"5_CR18","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1109\/43.851997","volume":"19","author":"C.A.J. Eijk van","year":"2000","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking based on structural similarities. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a019(7), 814\u2013819 (2000)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13338-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T08:34:13Z","timestamp":1559032453000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13338-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319133379","9783319133386"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13338-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}