{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:04:56Z","timestamp":1748577896616,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319212142"},{"type":"electronic","value":"9783319212159"}],"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-21215-9_5","type":"book-chapter","created":{"date-parts":[[2015,7,16]],"date-time":"2015-07-16T13:36:34Z","timestamp":1437053794000},"page":"76-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Code Generation Tools for the B-Method Using Tests: A Case Study"],"prefix":"10.1007","author":[{"given":"Anamaria M.","family":"Moreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cleverton","family":"Hentz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernesto C. B.","family":"de Matos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00e3o B. Souza","family":"Neto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Val\u00e9rio","family":"de Medeiros","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,17]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2008","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, New York (2008)"},{"key":"5_CR3","unstructured":"ClearSy. Atelier B User Manual Version 4.0. Clearsy System Engineering (2009)"},{"key":"5_CR4","unstructured":"D\u00e9harbe, D., Medeiros, Jr., V.: Proposal: Translation of B Implementations to LLVM-IR. In: SBMF, Bras\u00edlia - DF, SBMF (2013)"},{"key":"5_CR5","unstructured":"Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., Von Henke, F.W., Hoffmann, U., Langmaack, H., Pfeifer, H., Ruess, H., et al.: Compiler correctness and implementation verification: The verifix approach (1996)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-21470-7_16","volume-title":"Modelling Foundations and Applications","author":"M Gogolla","year":"2011","unstructured":"Gogolla, M., Vallecillo, A.: Tractable model transformation testing. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 221\u2013235. Springer, Heidelberg (2011)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/978-3-319-11245-9_19","volume-title":"Software Language Engineering","author":"J H\u00e4rtel","year":"2014","unstructured":"H\u00e4rtel, J., H\u00e4rtel, L., L\u00e4mmel, R.: Test-Data generation for Xtext. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) SLE 2014. LNCS, vol. 8706, pp. 342\u2013351. Springer, Heidelberg (2014)"},{"key":"5_CR8","unstructured":"Hentz, C.: Automatic Generation of Tests from Language Descriptions (Text in Portuguese). Master\u2019s thesis, UFRN, Natal, Brazil (2010)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Hoffman, D.M., Ly-Gagnon, D., Strooper, P., Wang, H.-Y.: Grammar-based test generation with yougen. Software: Practice and Experience 41(4), 427\u2013447 (2011)","DOI":"10.1002\/spe.1017"},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/s11086-005-0002-z","volume":"31","author":"AS Kossatchev","year":"2005","unstructured":"Kossatchev, A.S., Posypkin, M.A.: Survey of compiler testing methods. Program. Comput. Softw. 31(1), 10\u201319 (2005)","journal-title":"Program. Comput. Softw."},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-45314-8_15","volume-title":"Fundamental Approaches to Software Engineering","author":"R L\u00e4mmel","year":"2001","unstructured":"L\u00e4mmel, R.: Grammar testing. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 201\u2013216. Springer, Heidelberg (2001)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11754008_2","volume-title":"Testing of Communicating Systems","author":"R L\u00e4mmel","year":"2006","unstructured":"L\u00e4mmel, R., Schulte, W.: Controllable combinatorial coverage in grammar-based testing. In: Uyar, M.U., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 19\u201338. Springer, Heidelberg (2006)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM International Symposium on Code Generation and Optimization, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"7","key":"5_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Li, N., Offutt, J.: An empirical analysis of test oracle strategies for model-based testing. In: IEEE 7th International Conference on Software Testing, Verification and Validation (April 2014)","DOI":"10.1109\/ICST.2014.49"},{"key":"5_CR16","unstructured":"Moreira, A.M., Hentz, C., Ramalho, V.: Application of a Syntax-based Testing Method and Tool to Software Product Lines. In: 7th Brazilian Workshop on Systematic and Automated Software Testing, Bras\u00edlia - DF (2013)"},{"issue":"5","key":"5_CR17","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"GC Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. ACM Sigplan Notices 35(5), 83\u201394 (2000)","journal-title":"ACM Sigplan Notices"},{"issue":"4","key":"5_CR18","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BF01932308","volume":"12","author":"P Purdom","year":"1972","unstructured":"Purdom, P.: A sentence generator for testing parsers. BIT Numerical Mathematics 12(4), 366\u2013375 (1972)","journal-title":"BIT Numerical Mathematics"},{"issue":"9","key":"5_CR19","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1109\/TSE.2007.70708","volume":"33","author":"I Stuermer","year":"2007","unstructured":"Stuermer, I., Conrad, M., Doerr, H., Pepper, P.: Systematic testing of model-based code generators. IEEE Transactions on Software Engineering 33(9), 622\u2013634 (2007)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-41533-3_13","volume-title":"Model-Driven Engineering Languages and Systems","author":"M Wimmer","year":"2013","unstructured":"Wimmer, M., Burgue\u00f1o, L.: Testing M2T\/T2M transformations. In: Moreira, A., Sch\u00e4tz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 203\u2013219. Springer, Heidelberg (2013)"},{"issue":"3","key":"5_CR21","first-page":"223","volume":"9","author":"L Zuck","year":"2003","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A Methodology for the Translation Validation of Optimizing Compilers. Journal of Universal Computer Science 9(3), 223\u2013247 (2003)","journal-title":"Journal of Universal Computer Science"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21215-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T08:42:02Z","timestamp":1748508122000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21215-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319212142","9783319212159"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21215-9_5","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":"17 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}