{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:01Z","timestamp":1761597001038},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540410300"},{"type":"electronic","value":"9783540452973"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722468_13","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T11:43:32Z","timestamp":1167479012000},"page":"205-223","source":"Crossref","is-referenced-by-count":31,"title":["A Language Framework for Expressing Checkable Properties of Dynamic Software"],"prefix":"10.1007","author":[{"given":"James C.","family":"Corbett","sequence":"first","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"family":"Robby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Bal, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (2000)","key":"13_CR1"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Generalized temporal verification diagrams","author":"I.A. Browne","year":"1995","unstructured":"Browne, I.A., Manna, Z., Sipma, H.B.: FSTTCS 1995. LNCS, vol.\u00a01026. Springer, Heidelberg (1995)"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (2000) (to appear)","key":"13_CR3","DOI":"10.1007\/s100090050046"},{"doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)","key":"13_CR4","DOI":"10.1145\/337180.337234"},{"doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Bandera: A source-level interface for model checking Java programs. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)","key":"13_CR5","DOI":"10.1145\/337180.337625"},{"doi-asserted-by":"crossref","unstructured":"Darimont, R., van Lamsweerde, A.: Formal refinement patterns for goal-driven requirements elaboration. In: Proceedings of the Fourth ACM SIGSOFT Symposium on Foundations of Software Engineering, October 1996, pp. 179\u2013190 (1996)","key":"13_CR6","DOI":"10.1145\/239098.239131"},{"issue":"7","key":"13_CR7","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent Java programs. Software - Practice and Experience\u00a029(7), 577\u2013603 (1999)","journal-title":"Software - Practice and Experience"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-48234-2_20","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sisto, R.: dspin: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 261. Springer, Heidelberg (1999)"},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"L.K. Dillon","year":"1994","unstructured":"Dillon, L.K., Kutty, G., Moser, L.E., Melliar-Smith, P.M., Ra- makrishna, Y.S.: A graphical interval logic for specifying concurrent systems. ACM Transactions on Software Engineering and Methodology\u00a03(2), 131\u2013165 (1994)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) Proceedings of the Second Workshop on Formal Methods in Software Practice, March 1998, pp. 7\u201315 (1998)","key":"13_CR10","DOI":"10.1145\/298595.298598"},{"unstructured":"Dwyer, M.B., Pasareanu, C.S., Corbett, J.C.: Translating Ada programs for model checking: A tutorial. Technical Report 98-12, Kansas State University, Department of Computing and Information Sciences (1998)","key":"13_CR11"},{"unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: A System of Specification Patterns (1998), http:\/\/www.cis.ksu.edu\/santos\/spec-patterns","key":"13_CR12"},{"doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering (May 1999)","key":"13_CR13","DOI":"10.1145\/302405.302672"},{"unstructured":"Grove, D.P.: Effective Interprocedural Optimization of Object-oriented Lan- guages. PhD thesis, University of Washington (1998)","key":"13_CR14"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48294-6_1","volume-title":"Static Analysis","author":"J. Hatcliff","year":"1999","unstructured":"Hatcliff, J., Corbett, J.C., Dwyer, M.B., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, p. 1. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (1999)","key":"13_CR16","DOI":"10.1007\/s100090050043"},{"issue":"5","key":"13_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: Extracting verification models from source code. In: Proceedings of FORTE\/PSTV 1999 (November 1999)","key":"13_CR18","DOI":"10.1007\/978-0-387-35578-8_28"},{"unstructured":"Iosif, R., Sisto, R.: On the specification and semantics of source level properties in java. In: Proceedings of the First International Workshop on Automated Program Analysis Testing and Verification (June 2000), Held in conjunction with the 2000 Internation Conference on Software Engineering","key":"13_CR19"},{"unstructured":"Jackson, D.: Alloy: A lightweight object modelling notation","key":"13_CR20"},{"key":"13_CR21","volume-title":"Proceedings of Technology of Object-Oriented Languages and Systems, TOOLS-USA","author":"R. Kramer","year":"1998","unstructured":"Kramer, R.: iContract|the Java Design by Contract tool. In: Proceedings of Technology of Object-Oriented Languages and Systems, TOOLS-USA. IEEE Press, Los Alamitos (1998)"},{"unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling lan- guage. In: Reflection and Software Engineering (1998)","key":"13_CR22"},{"key":"13_CR23","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)"},{"key":"13_CR24","volume-title":"The Object Constraint Language: Precise Mode- ling with UML","author":"J. Warmer","year":"1998","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Mode- ling with UML. Addison-Wesley, Reading (1998)"}],"container-title":["Lecture Notes in Computer Science","SPIN Model Checking and Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722468_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T15:23:56Z","timestamp":1587309836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722468_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410300","9783540452973"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/10722468_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}