{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:18:29Z","timestamp":1712369909422},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,11,3]],"date-time":"2011-11-03T00:00:00Z","timestamp":1320278400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10009-011-0215-9","type":"journal-article","created":{"date-parts":[[2011,11,2]],"date-time":"2011-11-02T15:37:21Z","timestamp":1320248241000},"page":"387-405","source":"Crossref","is-referenced-by-count":7,"title":["Alternating simulation and IOCO"],"prefix":"10.1007","volume":"14","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,3]]},"reference":[{"key":"215_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"issue":"1\u20132","key":"215_CR2","first-page":"1","volume":"77","author":"J.-R. Abrial","year":"2007","unstructured":"Abrial J.-R., Hallerstede S.: Refinement, decomposition and instantiation of discrete models: application to Event-B. Fundam. Inform. 77(1\u20132), 1\u201328 (2007)","journal-title":"Fundam. Inform."},{"key":"215_CR3","doi-asserted-by":"crossref","unstructured":"Aichernig, B., Brandl, H., Krenn, W.: Qualitative action systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM\u201909. LNCS, vol. 5885, pp. 206\u2013225. Springer, Berlin-Heidelberg (2009)","DOI":"10.1007\/978-3-642-10373-5_11"},{"key":"215_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.: Alternating refinement relations. In: CONCUR\u201998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055622"},{"key":"215_CR5","unstructured":"AsmL. http:\/\/research.microsoft.com\/fse\/AsmL\/"},{"key":"215_CR6","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0167-6423(90)90069-P","volume":"13","author":"R.J.R. Back","year":"1990","unstructured":"Back R.J.R., Sere K.: Stepwise refinement of parallel algorithms. Sci. Comput. Program. 13, 133\u2013180 (1990)","journal-title":"Sci. Comput. Program."},{"key":"215_CR7","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli C.: Satisfiability modulo theories. Frontiers in Artificial Intelligence and Applications, chap. 26, vol. 185, pp 825\u2013885. IOS Press, February 2009"},{"key":"215_CR8","volume-title":"Logics of Specification Languages","year":"2008","unstructured":"Bj\u00f8rner, D., Henson, M. (eds): Logics of Specification Languages. Springer, Berlin (2008)"},{"key":"215_CR9","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating lemma learning using joins\u2014DPPL(Join). In: Proceedings of Short Papers at LPAR\u201908 (2008)"},{"key":"215_CR10","unstructured":"Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. Technical report MSR-TR-2005-04, Microsoft Research, January 2005. Short version appears in FATES (2005)"},{"key":"215_CR11","doi-asserted-by":"crossref","unstructured":"Boiten, E., Derrick, J.: IO-refinement in Z. In: 3rd Northern Formal Methods Workshop (1998)","DOI":"10.14236\/ewic\/NFM1998.3"},{"key":"215_CR12","doi-asserted-by":"crossref","unstructured":"Brandl, H., Weiglhofer, M., Aichernig, B.K.: Automated conformance verification of hybrid systems. In: QSIC 2010: The 10th International Conference on Quality Software, pp. 3\u201312. IEEE Computer Society (2010)","DOI":"10.1109\/QSIC.2010.53"},{"key":"215_CR13","doi-asserted-by":"crossref","unstructured":"Brinksma, E., Tretmans, J.: Testing transition systems: an annotated bibliography. In: MOVEP\u20192k. LNCS, vol. 2067, pp. 187\u2013193. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45510-8_9"},{"key":"215_CR14","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., German, S.M., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Conference on Computer Aided Verification (CAV\u201999). LNCS, vol. 1633, pp. 470\u2013482. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_40"},{"key":"215_CR15","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. Conference on Computer-Aided Verification (CAV\u201994). LNCS, vol. 818, pp. 68\u201380. Springer, (1994)"},{"key":"215_CR16","first-page":"20","volume-title":"IFM\u201909. LNCS, vol. 5423","author":"M. Butler","year":"2009","unstructured":"Butler M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds) IFM\u201909. LNCS, vol. 5423, pp. 20\u201338. Springer, Berlin (2009)"},{"key":"215_CR17","doi-asserted-by":"crossref","unstructured":"CACM Staff: Microsoft\u2019s protocol documentation program: interoperability testing at scale, a discussion with Nico Kicillof, Wolfgang Grieskamp, and Bob Binder. Commun. ACM 54(7), 51\u201357 (2011)","DOI":"10.1145\/1965724.1965741"},{"key":"215_CR18","doi-asserted-by":"crossref","unstructured":"de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 269\u2013289. Springer, Berlin","DOI":"10.1007\/978-3-540-39910-0_12"},{"key":"215_CR19","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/FSE, pp. 109\u2013120. ACM, New York (2001)","DOI":"10.1145\/503271.503226"},{"key":"215_CR20","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, (TACAS\u201908). LNCS. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"215_CR21","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L. Moura de","year":"2011","unstructured":"de Moura L., Bj\u00f8rner N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54, 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"215_CR22","doi-asserted-by":"crossref","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Proceedings of the 18th International Conference on Automated Deduction (CADE\u201902). LNCS, vol. 2392, pp. 438\u2013455. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45620-1_35"},{"key":"215_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra E.W., Scholten C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990)"},{"key":"215_CR24","first-page":"40","volume-title":"FATES\/RV 2006. LNCS, vol. 4262","author":"L. Frantzen","year":"2006","unstructured":"Frantzen L., Tretmans J., Willemse T.: A symbolic framework for model-based testing. In: Havelund, K., N\u00fa\u00f1ez, M., Rosu, G., Wolff, B. (eds) FATES\/RV 2006. LNCS, vol. 4262, pp. 40\u201354. Springer, Berlin (2006)"},{"key":"215_CR25","unstructured":"Franzen, L., Tretmans, J., Willemse, T.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) Proceedings of the Workshop on Formal Approaches to Software Testing (FATES 2004), pp. 3\u201317, Linz, Austria, September 2004. LNCS (to appear)"},{"key":"215_CR26","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium (2008)"},{"issue":"3","key":"215_CR27","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1016\/j.tcs.2005.06.017","volume":"343","author":"Y. Gurevich","year":"2005","unstructured":"Gurevich Y., Rossman B., Schulte W.: Semantic essence of AsmL. Theor. Comput. Sci. 343(3), 370\u2013412 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"215_CR28","first-page":"38","volume-title":"UTP\u20192006. LNCS, vol. 4010","author":"J. He","year":"2006","unstructured":"He J., Hoare T.: CSP is a retract of CCS. In: Dunne, S., Stoddart, W. (eds) UTP\u20192006. LNCS, vol. 4010, pp. 38\u201362. Springer, Berlin (2006)"},{"key":"215_CR29","doi-asserted-by":"crossref","first-page":"1311","DOI":"10.1016\/j.tcs.2009.12.012","volume":"411","author":"J. He","year":"2010","unstructured":"He J., Hoare T.: CSP is a retract of CCS. Theor. Comput. Sci. 411, 1311\u20131337 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"215_CR30","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson D.: Software Abstractions. MIT Press, New York (2006)"},{"key":"215_CR31","volume-title":"Model-Based Software Testing and Analysis with C#","author":"J. Jacky","year":"2008","unstructured":"Jacky J., Veanes M., Campbell C., Schulte W.: Model-Based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2008)"},{"key":"215_CR32","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R. Keller","year":"1976","unstructured":"Keller R.: Formal verification of parallel programs. Commun. ACM. 19, 371\u2013384 (1976)","journal-title":"Commun. ACM."},{"issue":"2","key":"215_CR33","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1109\/9.250512","volume":"38","author":"R. Kumar","year":"1993","unstructured":"Kumar R., Garg V.K., Marcus S.I.: A predicate transformer approach to control of discrete event systems. IEEE Trans. Autom. Control 38(2), 232\u2013247 (1993)","journal-title":"IEEE Trans. Autom. Control"},{"key":"215_CR34","doi-asserted-by":"crossref","unstructured":"Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 137\u2013151. ACM Press (1987)","DOI":"10.1145\/41840.41852"},{"key":"215_CR35","doi-asserted-by":"crossref","unstructured":"Poppleton, M.: The composition of Event-B models. In: B\u00f6rger, E., Butler, M.J., Bowen, J.P., Boca, P. International Conference on ASM, B and Z (ABZ\u201908). LNCS, vol. 5238, pp. 209\u2013222. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-87603-8_17"},{"issue":"1","key":"215_CR36","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1016\/S0304-3975(02)00547-9","volume":"290","author":"M. R\u00f6nkk\u00f6","year":"2003","unstructured":"R\u00f6nkk\u00f6 M., Ravn A.P., Sere K.: Hybrid action systems. Theor. Comput. Sci. 290(1), 937\u2013973 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"215_CR37","unstructured":"SMB2. http:\/\/msdn2.microsoft.com\/en-us\/library\/cc246482.aspx (2008)"},{"key":"215_CR38","doi-asserted-by":"crossref","unstructured":"Tillmann, N., Schulte, W.: Parameterized unit tests. In: ESEC\/FSE-13: Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 253\u2013262. ACM, New York (2005)","DOI":"10.1145\/1081706.1081745"},{"key":"215_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing. LNCS, vol. 4949","author":"J. Tretmans","year":"2008","unstructured":"Tretmans J.: Model based testing with labelled transition systems. In: Hierons, R., Bowen, J., Harman, M. (eds) Formal Methods and Testing. LNCS, vol. 4949, pp. 1\u201338. Springer, Berlin (2008)"},{"key":"215_CR40","unstructured":"Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR\u201999: 7th European Int. Conference on Software Testing, Analysis & Review, Barcelona, Spain, November 8\u201312, 1999. EuroStar Conferences, Galway, Ireland"},{"key":"215_CR41","doi-asserted-by":"crossref","unstructured":"van der Bij, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) Formal Approaches to Software Testing: Third International Workshop, FATES 2003. LNCS, vol. 2931, pp. 86\u2013100. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24617-6_7"},{"key":"215_CR42","doi-asserted-by":"crossref","unstructured":"Veanes, M., Bj\u00f8rner, N.: Input-output model programs. In: ICTAC\u201909. LNCS, vol. 5684, pp. 322\u2013335. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03466-4_21"},{"key":"215_CR43","first-page":"388","volume-title":"Perspectives of System Informatics (PSI\u201909). LNCS, vol. 5947","author":"M. Veanes","year":"2009","unstructured":"Veanes M., Bj\u00f8rner N.: Symbolic bounded conformance checking of model programs. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of System Informatics (PSI\u201909). LNCS, vol. 5947, pp. 388\u2013400. Springer, Berlin (2009)"},{"key":"215_CR44","doi-asserted-by":"crossref","unstructured":"Veanes, M., Bj\u00f8rner, N.: Alternating simulation and IOCO. In: Petrenko, A., Sim\u00e3o, A., Maldonado, J.(eds.) ICTSS\u20192010. LNCS, vol. 6435, pp. 47\u201362, Springer, Berlin","DOI":"10.1007\/978-3-642-16573-3_5"},{"issue":"2\u20133","key":"215_CR45","first-page":"149","volume":"3","author":"M. Veanes","year":"2009","unstructured":"Veanes M., Bj\u00f8rner N., Gurevich Y., Schulte W.: Symbolic Bounded Model Checking of Abstract State Machines. Int. J. Softw. Inform. 3(2\u20133), 149\u2013170 (2009)","journal-title":"Int. J. Softw. Inform."},{"key":"215_CR46","doi-asserted-by":"crossref","unstructured":"Veanes, M., Bj\u00f8rner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: FORTE\u201908. LNCS, vol. 5048, pp. 53\u201368. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68855-6_4"},{"issue":"7","key":"215_CR47","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1016\/j.jlap.2010.07.004","volume":"79","author":"M. Veanes","year":"2010","unstructured":"Veanes M., Jacky J.: Composing model programs for analysis. J. Logic Algebraic Program. 79(7), 467\u2013482 (2010)","journal-title":"J. Logic Algebraic Program."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0215-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0215-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0215-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,26]],"date-time":"2020-06-26T23:07:19Z","timestamp":1593212839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0215-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,3]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["215"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0215-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,3]]}}}