{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T16:43:55Z","timestamp":1776357835197,"version":"3.51.2"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319489889","type":"print"},{"value":"9783319489896","type":"electronic"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_28","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"460-478","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Towards Concolic Testing for Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Pingfan","family":"Kong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jingyi","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"28_CR1","unstructured":"http:\/\/sav.sutd.edu.sg\/?page_id=2803"},{"key":"28_CR2","unstructured":"http:\/\/sav.sutd.edu.sg\/SMC\/"},{"key":"28_CR3","volume-title":"Handbook of Mathematical Functions, With Formulas, Graphs, and Mathematical Tables","author":"M Abramowitz","year":"1974","unstructured":"Abramowitz, M.: Handbook of Mathematical Functions, With Formulas, Graphs, and Mathematical Tables. Dover Publications, New York (1974). Incorporated"},{"key":"28_CR4","unstructured":"Aziz, M.A., Wassal, A.G., Darwish, N.M.: A machine learning technique for hardness estimation of QFBV SMT problems. In: 10th International Workshop on Satisfiability Modulo Theories (SMT), pp. 57\u201366 (2012)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-28756-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Barbot","year":"2012","unstructured":"Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331\u2013346. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_23"},{"key":"28_CR6","unstructured":"Barbot, B., Haddad, S., Picaronny, C., et al.: Importance sampling for model checking of continuous time markov chains. In: SIMUL, pp. 30\u201335 (2012)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, M., Paul, S.: On the efficiency of automated testing. In: 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), pp. 632\u2013642 (2014)","DOI":"10.1145\/2635868.2635923"},{"key":"28_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 209\u2013224 (2008)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-662-46681-0_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Chistikov","year":"2015","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320\u2013334. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_26"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A Fehnker","year":"2004","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326\u2013341. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24743-2_22"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-23404-5_15","volume-title":"Model Checking Software","author":"A Filieri","year":"2015","unstructured":"Filieri, A., Frias, M.F., P\u0103s\u0103reanu, C.S., Visser, W.: Model counting for complex data structures. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 222\u2013241. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-23404-5_15"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), pp. 437\u2013448 (2014)","DOI":"10.1145\/2635868.2635899"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Chen, W., Clarke, E.: Delta-complete analysis for bounded reachability of hybrid systems. arXiv preprint arXiv:1404.7171 (2014)","DOI":"10.21236\/ADA613813"},{"key":"28_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). doi: 10.1007\/978-3-642-38574-2_14"},{"issue":"6","key":"28_CR15","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. SIGPLAN Not. 40(6), 213\u2013223 (2005)","journal-title":"SIGPLAN Not."},{"key":"28_CR16","volume-title":"Physics for Scientists and Engineers","author":"J Gordon","year":"2007","unstructured":"Gordon, J., Serway, R., McGrew, R.: Physics for Scientists and Engineers, vol. 2. Cengage Learning, Boston (2007)"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Bioinformatics)","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-26916-0_6","volume-title":"Hybrid Systems Biology","author":"BM Gyori","year":"2015","unstructured":"Gyori, B.M., Liu, B., Paul, S., Ramanathan, R., Thiagarajan, P.S.: Approximate probabilistic verification of hybrid systems. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) HSB 2015. LNCS (LNBI), vol. 9271, pp. 96\u2013116. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26916-0_6"},{"issue":"2","key":"28_CR18","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"28_CR20","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000)"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460\u2013463. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63166-6_48"},{"issue":"1","key":"28_CR22","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-46419-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A., Majumdar, R.: Symbolic model checking for rectangular hybrid systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 142\u2013156. Springer, Heidelberg (2000). doi: 10.1007\/3-540-46419-0_11"},{"key":"28_CR24","doi-asserted-by":"publisher","DOI":"10.1145\/1460833.1460872","volume-title":"A Programming Language","author":"KE Iverson","year":"1962","unstructured":"Iverson, K.E.: A Programming Language. Wiley, New York (1962)"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576\u2013591. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_38"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-02658-4_53","volume-title":"Computer Aided Verification","author":"S Jha","year":"2009","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 668\u2013674. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_53"},{"issue":"4","key":"28_CR27","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/j.apal.2011.12.002","volume":"163","author":"N Kamide","year":"2012","unstructured":"Kamide, N.: Bounded linear-time temporal logic: a proof-theoretic investigation. Ann. Pure Appl. Logic 163(4), 439\u2013466 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"Kong, P., Li, Y., Chen, X., Sun, J., Sun, M., Wang, J.: Towards concolic testing for hybrid systems. In: Fitzgerald, J., et al. (eds.) FM 2016, LNCS 9995, pp. X\u2013XY. Springer, Heidelberg (2016)","DOI":"10.1007\/978-3-319-48989-6_28"},{"issue":"1","key":"28_CR29","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/BF02420592","volume":"7","author":"H Lebesgue","year":"1902","unstructured":"Lebesgue, H.: Int\u00e9grale, longueur, aire. Annali di Matematica Pura ed Applicata 7(1), 231\u2013359 (1902)","journal-title":"Annali di Matematica Pura ed Applicata"},{"key":"28_CR30","volume-title":"Probability and Random Processes For EE\u2019s","author":"A Leon-Garcia","year":"2007","unstructured":"Leon-Garcia, A.: Probability and Random Processes For EE\u2019s, 3rd edn. Prentice-Hall Inc., Upper Saddle River (2007)","edition":"3"},{"key":"28_CR31","unstructured":"Lu, F., Iyer, M.K., Parthasarathy, G., Wang, L.-C., Cheng, K.-T., Chen, K.C.: An efficient sequential sat solver with improved search strategies. In: The Conference on Design, Automation and Test in Europe (DATE), 2005, pp. 1102\u20131107 (2005)"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Luckow, K.S., Pasareanu, C.S., Dwyer, M.B., Filieri, A., Visser, W.: Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: ACM\/IEEE International Conference on Automated Software Engineering (ASE), pp. 575\u2013586 (2014)","DOI":"10.1145\/2642937.2643011"},{"key":"28_CR33","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 416\u2013426. IEEE (2007)","DOI":"10.1109\/ICSE.2007.41"},{"key":"28_CR34","doi-asserted-by":"publisher","first-page":"046205","DOI":"10.1103\/PhysRevE.80.046205","volume":"80","author":"G Orosz","year":"2009","unstructured":"Orosz, G., Wilson, R.E., Szalai, R., St\u00e9p\u00e1n, G.: Exciting traffic jams: nonlinear phenomena behind traffic jam formation on highways. Phys. Rev. E. 80, 046205 (2009)","journal-title":"Phys. Rev. E."},{"key":"28_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). Incorporated"},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"Sen, K.: Concolic testing. In: 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 571\u2013572. ACM (2007)","DOI":"10.1145\/1321631.1321746"},{"key":"28_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer Aided Verification","author":"K Sen","year":"2006","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419\u2013423. Springer, Heidelberg (2006). doi: 10.1007\/11817963_38"},{"key":"28_CR38","unstructured":"Swat, S.: A test bed for secure water treatment (2015). http:\/\/academics.sutd.edu.sg\/news-events\/event\/news\/media-release-swat-a-test-bed-for-secure-water-treatment-swat\/"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"Veach, E., Guibas, L.J.: Optimally combining sampling techniques for monte carlo rendering. In: 22nd Annual Conference on Computer Graphics and Interactive Techniques (SIGGRAPH), pp. 419\u2013428 (1995)","DOI":"10.1145\/218380.218498"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:29:58Z","timestamp":1749691798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fm2016.cs.ucy.ac.cy\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}