{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:33:35Z","timestamp":1725536015399},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642034657"},{"type":"electronic","value":"9783642034664"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03466-4_21","type":"book-chapter","created":{"date-parts":[[2009,8,3]],"date-time":"2009-08-03T07:20:54Z","timestamp":1249284054000},"page":"322-335","source":"Crossref","is-referenced-by-count":7,"title":["Input-Output Model Programs"],"prefix":"10.1007","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. In: Proc. 30th Symp. on Foundations of Computer Science, pp. 164\u2013169 (1989)","DOI":"10.1109\/SFCS.1989.63473"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"21_CR3","unstructured":"AsmL, http:\/\/research.microsoft.com\/fse\/AsmL\/"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"volume-title":"Logics of Specification Languages","year":"2008","key":"21_CR5","unstructured":"Bj\u00f8rner, D., Henson, M. (eds.): Logics of Specification Languages. Springer, Heidelberg (2008)"},{"key":"21_CR6","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating Lemma Learning using Joins - DPPL(Join). In: Proceedings of short papers at LPAR 2008 (2008)"},{"key":"21_CR7","unstructured":"Bj\u00f8rner, N., Gurevich, Y., Schulte, W., Veanes, M.: Symbolic bounded model checking of abstract state machines. Technical Report MSR-TR-2009-14, Microsoft Research (February 2009) (submitted to IJSI)"},{"key":"21_CR8","doi-asserted-by":"crossref","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: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol.\u00a03997, pp. 32\u201346. Springer, Heidelberg (2006)","DOI":"10.1007\/11759744_3"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S.M., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-39910-0_12","volume-title":"Verification: Theory and Practice","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 269\u2013289. Springer, Heidelberg (2004)"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/503209.503226","volume-title":"ESEC\/FSE","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/FSE, pp. 109\u2013120. ACM Press, New York (2001)"},{"key":"21_CR13","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"21_CR15","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-7091-9459-1_5","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"M.J. Fisher","year":"1998","unstructured":"Fisher, M.J., Rabin, M.O.: Super-exponential complexity of presburger arithmetic. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 122\u2013135. Springer, Heidelberg (1998); Reprint from SIAM-AMS Proceedings, vol. VII, pp. 27\u201341 (1974)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Grieskamp, W., MacDonald, D., Kicillof, N., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of Windows protocol documentation. In: First International Conference on Software Testing, Verification and Validation, ICST, Lillehammer, Norway (April 2008)","DOI":"10.1109\/ICST.2008.50"},{"key":"21_CR17","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"issue":"3","key":"21_CR18","doi-asserted-by":"publisher","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.\u00a0343(3), 370\u2013412 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR19","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $\\Pi^1_1$ complete. Journal of Symbolic Logic\u00a056, 637\u2013642 (1991)","journal-title":"Journal of Symbolic Logic"},{"key":"21_CR20","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)"},{"key":"21_CR21","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":"21_CR22","unstructured":"SMB2 (2008), http:\/\/msdn2.microsoft.com\/en-us\/library\/cc246482.aspx"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing","author":"J. Tretmans","year":"2008","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol.\u00a04949, pp. 1\u201338. Springer, Heidelberg (2008)"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II, 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic bounded conformance checking of model programs. Technical Report MSR-TR-2009-28, Microsoft Research (March 2009)","DOI":"10.1007\/978-3-642-11486-1_33"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-68855-6_4","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Bj\u00f8rner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol.\u00a05048, pp. 53\u201368. Springer, Heidelberg (2008)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-78917-8_2","volume-title":"Formal Methods and Testing","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with Spec Explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol.\u00a04949, pp. 39\u201376. Springer, Heidelberg (2008)"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1081706.1081751","volume-title":"ESEC\/FSE-13","author":"M. Veanes","year":"2005","unstructured":"Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC\/FSE-13, pp. 273\u2013282. ACM Press, New York (2005)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-89439-1_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol.\u00a05330, pp. 305\u2013317. Springer, Heidelberg (2008)"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Veanes, M., Saabas, A., Bj\u00f8rner, N.: Bounded reachability of model programs. Technical Report MSR-TR-2008-81, Microsoft Research (May 2008)","DOI":"10.1007\/978-3-540-89439-1_22"},{"key":"21_CR31","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1109\/LICS.2004.1319602","volume-title":"Proceedings of the Nineteenth Annual IEEE Symposium on Logic In Computer Science, LICS 2004","author":"M. Yannakakis","year":"2004","unstructured":"Yannakakis, M.: Testing, optimization, and games. In: Proceedings of the Nineteenth Annual IEEE Symposium on Logic In Computer Science, LICS 2004, pp. 78\u201388. IEEE, Los Alamitos (2004)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03466-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T06:20:07Z","timestamp":1685082007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03466-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642034657","9783642034664"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03466-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}