{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:23:35Z","timestamp":1725798215828},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662441985"},{"type":"electronic","value":"9783662441992"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44199-2_46","type":"book-chapter","created":{"date-parts":[[2014,7,31]],"date-time":"2014-07-31T18:17:11Z","timestamp":1406830631000},"page":"295-302","source":"Crossref","is-referenced-by-count":2,"title":["Quantifier Elimination for Linear Modular Constraints"],"prefix":"10.1007","author":[{"given":"Ajith K.","family":"John","sequence":"first","affiliation":[]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"46_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-642-22110-1_39","volume-title":"Computer Aided Verification","author":"A.K. John","year":"2011","unstructured":"John, A.K., Chakraborty, S.: A quantifier elimination algorithm for linear modular equations and disequations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 486\u2013503. Springer, Heidelberg (2011)"},{"key":"46_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-36742-7_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.K. John","year":"2013","unstructured":"John, A.K., Chakraborty, S.: Extending quantifier elimination to linear inequalities on bit-vectors. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 78\u201392. Springer, Heidelberg (2013)"},{"key":"46_CR3","unstructured":"Bj\u00f8rner, N., Blass, A., Gurevich, Y., Musuvathi, M.: Modular difference logic is hard. CoRR abs\/0811.0987 (2008)"},{"key":"46_CR4","unstructured":"Kroening, D., Strichman, O.: Decision procedures: an algorithmic point of view. Texts in Theoretical Computer Science. Springer (2008)"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: FMCAD 2009 (2009)","DOI":"10.1109\/FMCAD.2009.5351143"},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega Test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 102\u2013114 (1992)","DOI":"10.1145\/135226.135233"},{"key":"46_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Monniaux","year":"2008","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 243\u2013257. Springer, Heidelberg (2008)"},{"key":"46_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"issue":"5","key":"46_CR9","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1275497.1275504","volume":"29","author":"M. Muller-Olm","year":"2007","unstructured":"Muller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Transactions on Programming Languages and Systems\u00a029(5), 29 (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"46_CR10","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"46_CR11","unstructured":"CUDD release 2.4.2 website, \n                    \n                      vlsi.colorado.edu\/fabio\/CUDD"}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44199-2_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T09:30:00Z","timestamp":1558949400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44199-2_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662441985","9783662441992"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44199-2_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}