{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:53:11Z","timestamp":1777488791736,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540737698","type":"print"},{"value":"9783540737704","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73770-4_7","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T16:00:13Z","timestamp":1187971213000},"page":"114-130","source":"Crossref","is-referenced-by-count":9,"title":["Using Contracts and Boolean Queries to Improve the Quality of Automatic Test Generation"],"prefix":"10.1007","author":[{"given":"Lisa (Ling)","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Schoeller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnettl","year":"2005","unstructured":"Barnettl, M., Rustan, K., Leinol, M., Schultel, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T.: A theory of predicate-complete test coverage and generation. In: 3rd International Symposium on Formal Methods for Components and Objects, pp. 1\u201322 (2004)","DOI":"10.1007\/11561163_1"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566172.566191","volume-title":"ISSTA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: ISSTA 2002. Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 123\u2013133. ACM Press, New York (2002)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","first-page":"422","volume-title":"Software Engineering Education in the Modern Age","author":"C. Csallner","year":"2006","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 crash: combining static checking and testing. In: Inverardi, P., Jazayeri, M. (eds.) ICSE 2005. LNCS, vol.\u00a04309, pp. 422\u2013431. Springer, Heidelberg (2006)"},{"key":"7_CR5","unstructured":"Ciupa, I., Leitner, A.: Automatic testing based on design by contract. In: Proceedings of Net.ObjectDays 2005 (6th Annual International Conference on Object-Oriented and Internet-based Technologies, Concepts and Applications for a Networked World), pp. 545\u2013557 (2005)"},{"key":"7_CR6","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003), http:\/\/research.compaq.com\/SRC\/esc\/Simplify.html"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1109\/TSE.1984.5010257","volume":"SE-10","author":"J. Duran","year":"1984","unstructured":"Duran, J., Ntafos, S.: An evaluation of random testing. IEEE Transactions on Software Engineering\u00a0SE-10, 438\u2013444 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR8","volume-title":"Proceedings of 6th IASTED International Conference on Software Engineering and Applications","author":"A. Hamie","year":"2002","unstructured":"Hamie, A.: Towards verifying Java realization of OCL-constrained design models using JML. In: Proceedings of 6th IASTED International Conference on Software Engineering and Applications, ACTA Press, MIT, Cambridge, MA, USA (2002)"},{"issue":"12","key":"7_CR9","doi-asserted-by":"publisher","first-page":"1402","DOI":"10.1109\/32.62448","volume":"16","author":"D. Hamlet","year":"1990","unstructured":"Hamlet, D., Taylor, R.: Partition testing does not inspire confidence. IEEE Transactions on Software Engineering\u00a016(12), 1402\u20131411 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR10","first-page":"970","volume-title":"Encyclopedia of Software Engineering","author":"R. Hamlet","year":"1994","unstructured":"Hamlet, R.: Random testing. In: Marciniak, J. (ed.) Encyclopedia of Software Engineering, pp. 970\u2013978. Wiley, Chichester (1994)"},{"issue":"2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: Alightweight object modeling notation. ACM Trans. Soft. Eng. Methodology\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Soft. Eng. Methodology"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Kramer, R.: iContract - the JavaTM design by contractTM tool. In: Proceedings of Object-Oriented Language and Systems, pp. 295\u2013307. IEEE Computer Society, Washington, DC, USA (1998)","DOI":"10.1109\/TOOLS.1998.711021"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: World Congress on Formal Methods, pp. 1087\u20131106 (1999)","DOI":"10.1007\/3-540-48118-4_8"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of jml accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003)"},{"key":"7_CR15","first-page":"1090","volume-title":"Proc. The IEEE","author":"D. Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. In: Proc. The IEEE, pp. 1090\u20131123. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"7_CR16","unstructured":"Liu, L., Leitner, A., Offutt, J.: Using contracts to automate forward class testing. Journal of System and Software (submitted)"},{"key":"7_CR17","volume-title":"Reusable Software: The Base Object-Oriented Libraries","author":"B. Meyer","year":"1994","unstructured":"Meyer, B.: Reusable Software: The Base Object-Oriented Libraries. Prentice Hall, Englewood Cliffs (1994)"},{"key":"7_CR18","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"7_CR19","unstructured":"Meyer, B.: Eiffel: The Language, Prentice Hall, 1991, revised edn. in progress at (2006), http:\/\/se.ethz.ch\/~meyer\/ongoing\/etl\/"},{"key":"7_CR20","first-page":"22","volume-title":"ASE","author":"D. Marinov","year":"2001","unstructured":"Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: ASE. Proc. 16th IEEE International Conference on Automated Software Engineering, pp. 22\u201334. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","first-page":"11","volume-title":"Fast Software Encryption","author":"J.W. Nimmer","year":"2002","unstructured":"Nimmer, J.W., Ernst, M.D.: Invariant inference for static checking: An empirical evaluation. In: Daemen, J., Rijmen, V. (eds.) FSE 2002. LNCS, vol.\u00a02365, pp. 11\u201320. Springer, Heidelberg (2002)"},{"issue":"6","key":"7_CR22","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1145\/62959.62964","volume":"31","author":"T.J. Ostrand","year":"1988","unstructured":"Ostrand, T.J., Balcer, M.J.: The Category-Partition method for specifying and generating functional test. Comm. ACM\u00a031(6), 676\u2013686 (1988)","journal-title":"Comm. ACM"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-49730-7","volume-title":"Conceptual Modeling \u2013 ER 1998","author":"M. Richtersl","year":"1998","unstructured":"Richtersl, M., Gogolla, M.: On formalizing the UML object constraint language OCL. In: Ling, T.-W., Ram, S., Lee, M.L. (eds.) Conceptual Modeling \u2013 ER 1998. LNCS, vol.\u00a01507, Springer, Heidelberg, Singapore (1998)"},{"key":"7_CR24","unstructured":"SICStus Prolog User\u2019s Manual, http:\/\/www.sics.se\/sicstus\/docs\/latest\/pdf\/sicstus.pdf"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interface. In: ISSTA 2002, pp. 218\u2013228 (2002)","DOI":"10.1145\/566172.566212"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-540-30482-1_27","volume-title":"Formal Methods and Software Engineering","author":"T. Xie","year":"2004","unstructured":"Xie, T., Notkin, D.: Automatic extraction of object-oriented observer abstractions from unit-test executions. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 290\u2013305. Springer, Heidelberg (2004)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together! In: ISSTA 2006, pp. 145-156 (2006)","DOI":"10.1145\/1146238.1146255"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73770-4_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T16:56:19Z","timestamp":1737392179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73770-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540737698","9783540737704"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73770-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}