{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:21:00Z","timestamp":1743009660996,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259444"},{"type":"electronic","value":"9783319259451"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-25945-1_3","type":"book-chapter","created":{"date-parts":[[2015,11,6]],"date-time":"2015-11-06T22:20:37Z","timestamp":1446848437000},"page":"35-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model-Based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts"],"prefix":"10.1007","author":[{"given":"Imen","family":"Boudhiba","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Gaston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"3_CR1","unstructured":"B. Bannour. Symbolic analysis of scenario based timed models for component-based systems: Compositionality results for testing. PhD thesis, Ecole Centrale Paris, CEA, 2012"},{"key":"3_CR2","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., Hubert, T., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, v1.9, March 2015"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Boudhiba, I., Gaston, C., Le Gall, P., Prevosto, V.: Input ouput symbolic transitions systems enriched by program calls and contracts : a detailed example of a vending machine. Technical report hal-01191890, MAS Laboratory, CentraleSupelec (2015)","DOI":"10.1007\/978-3-319-25945-1_3"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-18275-4_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150\u2013168. Springer, Heidelberg (2011)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: Dysy: Dynamic symbolic execution for invariant inference. In Proceedings of ICSE (2008)","DOI":"10.1145\/1368088.1368127"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-319-11743-0_14","volume-title":"System Analysis and Modeling: Models and Reusability","author":"J Deltour","year":"2014","unstructured":"Deltour, J., Faivre, A., Gaudin, E., Lapitre, A.: Model-based testing: an approach with SDL\/RTDS and DIVERSITY. In: Amyot, D., Fonseca i Casas, P., Mussbacher, G. (eds.) SAM 2014. LNCS, vol. 8769, pp. 198\u2013206. Springer, Heidelberg (2014)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"MD Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. Trans. Soft. Eng. 27, 99\u2013123 (2001)","journal-title":"Trans. Soft. Eng."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings AMS Symposium on Applied Mathematics, vol. 19 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11754008_1","volume-title":"Testing of Communicating Systems","author":"C Gaston","year":"2006","unstructured":"Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Uyar, M.\u00dc., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1\u201318. Springer, Heidelberg (2006)"},{"issue":"10","key":"3_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Jehan, S. Pill, I., Wotawa, F.: Functional SOA testing based on constraints. In: Automation of Software Test (2013)","DOI":"10.1109\/IWAST.2013.6595788"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"17","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Comm. ACM 17, 385\u2013395 (1976)","journal-title":"Comm. ACM"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27, 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Kumar, S., Khoo, S.-C., Roychoudhury, A., Lo, D.: Inferring class level specifications for distributed systems. In: Proceedings ICSE (2012)","DOI":"10.1109\/ICSE.2012.6227128"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10515-012-0103-x","volume":"19","author":"D Lo","year":"2012","unstructured":"Lo, D., Maoz, S.: Scenario-based and value-based specification mining: better together. Autom. Softw. Eng. 19, 423\u2013458 (2012)","journal-title":"Autom. Softw. Eng."},{"issue":"10","key":"3_CR18","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\". IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"3_CR19","unstructured":"Object Management Group. OMG Unified Modeling LanguageTM (OMG UML), version 2.5 edition (2013)"},{"key":"3_CR20","unstructured":"Schmitt, P.H., Wei\u00df, B.: Inferring invariants by symbolic execution. In: VERIFY Workshop. CEUR Workshop Proceedings, vol. 259 (2007)"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0169-7552(96)00017-7","volume":"29","author":"J Tretmans","year":"1996","unstructured":"Tretmans, J.: Conformance testing with labelled transition systems: implementation relations and test generation. Comput. Netw. ISDN Syst. 29, 49\u201379 (1996)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.14257\/ijfgcn.2014.7.3.19","volume":"7","author":"Y Wang","year":"2014","unstructured":"Wang, Y., Xing, Y., Zhang, X.: A method of path feasibility judgment based on symbolic execution and range analysis. Int. J. Future Gener. Commun. Networking 7, 205\u2013212 (2014)","journal-title":"Int. J. Future Gener. Commun. Networking"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: Proc ICSE (2011)","DOI":"10.1145\/1985793.1985820"},{"key":"3_CR24","unstructured":"Zhang, L., Yang, G., Rungta, N., Person, S., Khurshid, S.: Invariant discovery guided by symbolic execution. In: The Java PathFinder Workshop (2013)"}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25945-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,18]],"date-time":"2019-12-18T03:24:17Z","timestamp":1576639457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25945-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259444","9783319259451"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25945-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}