{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:47:12Z","timestamp":1726033632472},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030223472"},{"type":"electronic","value":"9783030223489"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22348-9_19","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T17:04:54Z","timestamp":1561482294000},"page":"310-325","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["JConstraints: A Library for Working with Logic Expressions in Java"],"prefix":"10.1007","author":[{"given":"Falk","family":"Howar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fadi","family":"Jabbour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malte","family":"Mues","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,26]]},"reference":[{"key":"19_CR1","unstructured":"Aharoni, M., Asaf, S., Fournier, L., Koifman, A., Nagel, R.: FPgen-a test generation framework for datapath floating-point verification. In: Eighth IEEE International High-Level Design Validation and Test Workshop, 2003, pp. 17\u201322. IEEE (2003)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Carlier, M., Gori, R., Gotlieb, A.: Symbolic path-oriented test data generation for floating-point programs. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation (ICST), pp. 1\u201310. IEEE (2013)","DOI":"10.1109\/ICST.2013.17"},{"key":"19_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"19_CR4","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885 (2009)"},{"issue":"2","key":"19_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Softw. Test. Verif. Reliab. 16(2), 97\u2013121 (2006)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"19_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209\u2013224 (2008)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-319-10431-7_18","volume-title":"Software Engineering and Formal Methods","author":"S Cassel","year":"2014","unstructured":"Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Learning extended finite state machines. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 250\u2013264. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_18"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P Cousot","year":"2007","unstructured":"Cousot, P., et al.: Combination of abstractions in the ASTR\u00c9E static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272\u2013300. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_23"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-61467-0_1","volume-title":"Tests and Proofs","author":"F Damiani","year":"2017","unstructured":"Damiani, F., H\u00e4hnle, R., Lienhardt, M.: Abstraction refinement for the analysis of software product lines. In: Gabmeyer, S., Johnsen, E.B. (eds.) TAP 2017. LNCS, vol. 10375, pp. 3\u201320. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-61467-0_1"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: ACM SIGPLAN Notices, vol. 49, pp. 235\u2013248. ACM (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"19_CR12","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Dinges, P., Agha, G.: Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of the 22nd ACM SIGSOFT Symposium on Foundations of Software Engineering, Hong Kong, 16\u201321 November 2014. ACM (2014)","DOI":"10.1145\/2635868.2635889"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"19_CR15","unstructured":"Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop 2015 (2015)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-33125-1_18","volume-title":"Static Analysis","author":"D Giannakopoulou","year":"2012","unstructured":"Giannakopoulou, D., Rakamari\u0107, Z., Raman, V.: Symbolic learning of component interfaces. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 248\u2013264. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_18"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"E Goubault","year":"2006","unstructured":"Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18\u201334. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_3"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-18275-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Goubault","year":"2011","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232\u2013247. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-27940-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Howar","year":"2012","unstructured":"Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251\u2013266. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_17"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Ireland, C., Bowers, D., Newton, M., Waugh, K.: A classification of object-relational impedance mismatch. In: First International Conference on Advances in Databases, Knowledge, and Data Applications, DBKDA 2009, pp. 36\u201343. IEEE (2009)","DOI":"10.1109\/DBKDA.2009.11"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-21690-4_32","volume-title":"Computer Aided Verification","author":"M Isberner","year":"2015","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487\u2013495. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_32"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A.F., Zahl, R., Wehrle, K.: Floating-point symbolic execution: a case study in N-version programming. In: 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 601\u2013612. IEEE (2017)","DOI":"10.1109\/ASE.2017.8115670"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-662-49674-9_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Luckow","year":"2016","unstructured":"Luckow, K., et al.: JDart: a dynamic symbolic analysis framework. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 442\u2013459. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_26"},{"key":"19_CR24","unstructured":"Margaria, T., Nagel, R., Steffen, B.: Remote integration and coordination of verification tools in JETI. In: 12th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2005), Greenbelt, MD, USA, 4\u20137 April 2005, pp. 431\u2013436 (2005)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-45927-8_14","volume-title":"Programming Languages and Systems","author":"M Martel","year":"2002","unstructured":"Martel, M.: Propagation of roundoff errors in finite precision computations: a semantics approach. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 194\u2013208. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45927-8_14"},{"key":"19_CR26","unstructured":"Pasareanu, C., d\u2019Amorim, M., Borges, M., Souza, M.: Coral: solving complex constraints for symbolic pathfinder (2010)"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-24738-8_18","volume-title":"Numerical Software with Result Verification","author":"S Putot","year":"2004","unstructured":"Putot, S., Goubault, E., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Numerical Software with Result Verification. LNCS, vol. 2991, pp. 306\u2013313. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24738-8_18"},{"key":"19_CR28","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-46254-7_24","volume-title":"Information and Software Technologies","author":"K Richly","year":"2016","unstructured":"Richly, K., Lorenz, M., Oergel, S.: S4J - integrating SQL into Java at compiler-level. In: Dregvaite, G., Damasevicius, R. (eds.) ICIST 2016. CCIS, vol. 639, pp. 300\u2013315. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46254-7_24"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-319-06200-6_20","volume-title":"NASA Formal Methods","author":"J Schumann","year":"2014","unstructured":"Schumann, J., Schneider, S.-A.: Automated testcase generation for numerical support functions in embedded systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 252\u2013257. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_20"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Sherman, E., Dwyer, M.B.: Exploiting domain and program structure to synthesize efficient and precise data flow analyses (t). In: 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 608\u2013618. IEEE (2015)","DOI":"10.1109\/ASE.2015.41"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-20398-5_26","volume-title":"NASA Formal Methods","author":"M Souza","year":"2011","unstructured":"Souza, M., Borges, M., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S.: CORAL: solving complex constraints for symbolic pathfinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359\u2013374. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_26"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 311\u2013344 (2019)","DOI":"10.1007\/978-3-319-91908-9_17"},{"issue":"1\u20132","key":"19_CR33","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s100090050003","volume":"1","author":"B Steffen","year":"1997","unstructured":"Steffen, B., Margaria, T., Braun, V.: The electronic tool integration platform: concepts and design. STTT 1(1\u20132), 9\u201330 (1997)","journal-title":"STTT"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT\/FSE 2012, Cary, NC, USA, 11\u201316 November 2012, p. 58 (2012)","DOI":"10.1145\/2393596.2393665"}],"container-title":["Lecture Notes in Computer Science","Models, Mindsets, Meta: The What, the How, and the Why Not?"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22348-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,30]],"date-time":"2019-11-30T14:46:06Z","timestamp":1575125166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22348-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030223472","9783030223489"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22348-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"26 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}