{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:49:12Z","timestamp":1743137352943,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642017018"},{"type":"electronic","value":"9783642017025"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-01702-5_11","type":"book-chapter","created":{"date-parts":[[2009,4,18]],"date-time":"2009-04-18T10:01:45Z","timestamp":1240048905000},"page":"68-83","source":"Crossref","is-referenced-by-count":2,"title":["Efficient Decision Procedure for Bounded Integer Non-linear Operations Using SMT( $\\mathcal{LIA}$ )"],"prefix":"10.1007","author":[{"given":"Malay K.","family":"Ganai","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Singerman, E.: Challenges in making decision procedures applicable to industry. In: Proc. of Pragmatics of Decision Procedures in Automated Resonings (2005)"},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-69167-1","volume-title":"SAT-based Scalable Formal Verification Solutions","author":"M.K. Ganai","year":"2007","unstructured":"Ganai, M.K., Gupta, A.: SAT-based Scalable Formal Verification Solutions. Springer Science and Business Media, Heidelberg (2007)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propogation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: Proc. of ICCAD (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL Constructs for MathSAT: a Preliminary Report. In: Proc. of Logic Programming and Automated Reasoning (2006)","DOI":"10.1016\/j.entcs.2005.12.001"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bjorner, N.: 3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Fallah, F., Devdas, S., Keutzer, K.: Functional Vector Generation for HDL Models Using Linear Programming and 3-Satisfiability. In: Proc. of DAC (1998)","DOI":"10.1145\/277044.277187"},{"key":"11_CR10","unstructured":"Brinkmann, R., Drecshler, R.: RTL-Datapath Verification using Integer Linear Programming. In: Proc. of ASPDAC (2002)"},{"key":"11_CR11","unstructured":"Zeng, Z., Kalla, P., Ciesielski, M.: LPSAT: A Unified Approach to RTL Satisfiability. In: Proc. of DATE (2001)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-Based Satisfiability Solving of Presburger Arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding Bit-Vector Arithmetic with Abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of verilog models. In: Proc. of DAC (2004)","DOI":"10.1145\/996566.996629"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Seshia, S., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proc. of DAC (2003)","DOI":"10.1145\/775944.775945"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proc. of DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Ganai, M., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: Proc. of DAC (June 2002)","DOI":"10.1145\/513918.514105"},{"key":"11_CR18","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":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A Lazy and Layered SMT(\n                    \n                      \n                    \n                    $\\mathcal{BV}$\n                  ) Solver for Hard Industrial Verification Problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 547\u2013560. Springer, Heidelberg (2007)"},{"key":"11_CR20","unstructured":"Babic, D., Hutter, F.: Spear Theorem Prover. In: Theory and Applications of Satisfiability Testing (2007)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73368-3_35","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2007","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The Bit-level Analysis Tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 303\u2013306. Springer, Heidelberg (2007)"},{"key":"11_CR22","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)"},{"key":"11_CR23","unstructured":"Babic, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical Report TR-2005-114, Microsoft Reserach Redmond (2005)"},{"key":"11_CR24","unstructured":"Maxima\u00a0Development Team. Maxima, a Computer Algebra System, \n                    \n                      http:\/\/maxima.sourceforge.net"},{"key":"11_CR25","doi-asserted-by":"publisher","DOI":"10.1515\/9781400884179","volume-title":"Linear Programming and its Extensions","author":"G.B. Dantzig","year":"1963","unstructured":"Dantzig, G.B.: Linear Programming and its Extensions. Princeton University Press, Princeton (1963)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Badros, G., Borning, A., Stucky, P.: The Cassowary Linear Arithmetic Constraint solving algorithm. In: ACM Transactions on Computer-Human Interaction (2001)","DOI":"10.1145\/504704.504705"},{"key":"11_CR27","unstructured":"Ganai, M.K.: Conference notes, \n                    \n                      http:\/\/www.nec-labs.com\/~malay\/notes.htm"},{"key":"11_CR28","unstructured":"Zaks, A., Shlyakhter, I., Ivan\u010di\u0107, F., Cadambi, S., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Using range analysis for software verification. In: International Workshop on Software Verification and Validation (2006)"},{"key":"11_CR29","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1989","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.H.: Introduction to Algorithms. MIT Press, Cambridge (1989)"},{"key":"11_CR30","unstructured":"SRI. Yices: An SMT solver, \n                    \n                      http:\/\/fm.csl.sri.com\/yices"},{"key":"11_CR31","unstructured":"Microsoft. Z3: SMT solver, \n                    \n                      http:\/\/research.microsoft.com\/projects\/Z3\/"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"}],"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-642-01702-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:03:57Z","timestamp":1558267437000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01702-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642017018","9783642017025"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01702-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}