{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T10:46:45Z","timestamp":1747133205337},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319297774"},{"type":"electronic","value":"9783319297781"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29778-1_18","type":"book-chapter","created":{"date-parts":[[2016,2,19]],"date-time":"2016-02-19T04:16:33Z","timestamp":1455855393000},"page":"287-302","source":"Crossref","is-referenced-by-count":3,"title":["SMT Solving for the Theory of Ordering Constraints"],"prefix":"10.1007","author":[{"given":"Cunjing","family":"Ge","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feifei","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeff","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,20]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: SAT modulo monotonic theories. In: AAAI (2015)","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Cotton, S., Maler, O.: Fast and flexiable difference constraint propagation for DPLL(T). In: SAT (2006)","DOI":"10.1007\/11814948_19"},{"key":"18_CR5","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., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR6","unstructured":"Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report (2006)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Eslamimehr, M., Palsberg, J. Sherlock: Scalable deadlock detection for concurrent programs. In: FSE (2014)","DOI":"10.1145\/2635868.2635918"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: ESEC\/FSE (2013)","DOI":"10.1145\/2491411.2491453"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P., Razavi, N., Sorrentino, F.: Predicting null-pointer dereferences in concurrent programs. In: FSE (2012)","DOI":"10.1145\/2393596.2393651"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Fasttrack: efficient and precise dynamic race detection. In: PLDI (2009)","DOI":"10.1145\/1542476.1542490"},{"key":"18_CR11","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. 4590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38574-2_15","volume-title":"Automated Deduction \u2013 CADE-24","author":"G Gange","year":"2013","unstructured":"Gange, G., S\u00f8ndergaard, H., Stuckey, P.J., Schachte, P.: Solving difference constraints over modular arithmetic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 215\u2013230. Springer, Heidelberg (2013)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-319-11558-0_10","volume-title":"Logics in Artificial Intelligence","author":"M Gebser","year":"2014","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: acyclicity. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 137\u2013151. Springer, Heidelberg (2014)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: Answer set programming as SAT modulo acyclicity. In: ECAI (2014)","DOI":"10.1007\/978-3-319-11558-0_10"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: PLDI (2015)","DOI":"10.1145\/2737924.2737975"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Huang, J., Luo, Q., Rosu, G.: Gpredict: Generic predictive concurrency analysis. In: ICSE (2015)","DOI":"10.1109\/ICSE.2015.96"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: PLDI (2014)","DOI":"10.1145\/2594291.2594315"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Huang, J., Zhang, C.: PECAN: persuasive prediction of concurrency access anomalies. In: ISSTA (2011)","DOI":"10.1145\/2001420.2001438"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Huang, J., Zhang, C., Dolby, J.: CLAP: Recording local executions to reproduce concurrency failures. In: PLDI (2013)","DOI":"10.1145\/2491956.2462167"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-19237-1_15","volume-title":"Hardware and Software: Verification and Testing","author":"D Kroening","year":"2011","unstructured":"Kroening, D., Weissenbacher, G.: An interpolating decision procedure for transitive relations with uninterpreted functions. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 150\u2013168. Springer, Heidelberg (2011)"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Kim, H., Somenzi, F.: Finite instantiations for integer difference logic. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.13"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Lee, D., Said, M., Narayanasamy, S., Yang, Z., Pereira, C.: Offline symbolic analysis for multi-processor execution replay. In: MICRO (2009)","DOI":"10.1145\/1669112.1669182"},{"key":"18_CR24","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 propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-20398-5_23","volume-title":"NASA Formal Methods","author":"M Said","year":"2011","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 313\u2013327. Springer, Heidelberg (2011)"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multi-threaded programs. In: TOCS (1997)","DOI":"10.1145\/265924.265927"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstraction. In: POPL (2011)","DOI":"10.1145\/1926385.1926433"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., Flanagan, C.: Sound predictive race detection in polynomial time. In: POPL (2012)","DOI":"10.1145\/2103656.2103702"},{"issue":"2","key":"18_CR29","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 328\u2013342. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Languages and Compilers for Parallel Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29778-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T22:55:30Z","timestamp":1692226530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29778-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319297774","9783319297781"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29778-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}