{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:29Z","timestamp":1725516509077},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_16","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"144-152","source":"Crossref","is-referenced-by-count":26,"title":["The Spec# Programming System: Challenges and Directions"],"prefix":"10.1007","author":[{"given":"Mike","family":"Barnett","sequence":"first","affiliation":[]},{"given":"Robert","family":"DeLine","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"F\u00e4hndrich","sequence":"additional","affiliation":[]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[]},{"given":"Herman","family":"Venter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6) (2004), \n \n www.jot.fm","DOI":"10.5381\/jot.2004.3.6.a2"},{"volume-title":"Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE 2005","year":"2005","author":"M. Barnett","key":"16_CR3","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE 2005, September 2005, ACM, New York (2005)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"K. Mike Barnett","year":"2005","unstructured":"Mike Barnett, K., Rustan, M.: Leino, and Wolfram Schulte. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends Need a Bit More: Maintaining Invariants Over Shared State. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"16_CR6","unstructured":"Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: Useful abstractions in specifications. In: Proceedings, 6th workshop on Formal Techniques for Java-like Programs (June 2004)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-30579-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Abstract Interpretation with Alien Expressions and Heap Structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 147\u2013163. Springer, Heidelberg (2005)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Inferring object invariants. In: Proceedings of First International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL 2005) (2005)","DOI":"10.1016\/j.entcs.2005.01.023"},{"issue":"6","key":"16_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Software\u2014Practice and Experience\u00a035(6), 583\u2013599 (2005)","journal-title":"Software\u2014Practice and Experience"},{"key":"16_CR10","first-page":"238","volume-title":"Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, January 1977, pp. 238\u2013252. ACM, New York (1977)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, January 1978, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"16_CR12","unstructured":"DeLine, R., Rustan, K., Leino, M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical report, Microsoft Research (2005)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Evans, D., Guttag, J.V., Horning, J.J., Tan, Y.M.: LCLint: A tool for using specifications to check code. In: Wile, D.S. (ed.) SIGSOFT 1994, Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, December 1994. ACM SIGSOFT Software Engineering Notes, vol.\u00a019(5), pp. 87\u201396 (1994)","DOI":"10.1145\/193173.195297"},{"key":"16_CR14","series-title":"SIGPLAN Notices","first-page":"302","volume-title":"Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2003","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Crocker, R., Steele Jr., G.L. (eds.) Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2003, October 2003. SIGPLAN Notices, vol.\u00a038(11), pp. 302\u2013312. ACM, New York (2003)"},{"key":"16_CR15","first-page":"137","volume-title":"3rd International Conference on Software Engineering and Formal Methods","author":"B. Jacobs","year":"2005","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Aichernig, B.K., Beckert, B. (eds.) 3rd International Conference on Software Engineering and Formal Methods, September 2005, pp. 137\u2013146. IEEE, Los Alamitos (2005)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11901433_23","volume-title":"Formal Methods and Software Engineering","author":"B. Jacobs","year":"2006","unstructured":"Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 420\u2013439. Springer, Heidelberg (2006)"},{"key":"16_CR17","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev28, Iowa State University, Department of Computer Science, See (2003), \n \n http:\/\/www.jmlspecs.org"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K. Rustan","year":"2004","unstructured":"Rustan, K., Leino, M., M\u00fcller, P.: Object invariants in dynamic contexts. In Martin Odersky. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013516. Springer, Heidelberg (2004)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/978-3-540-32008-1","volume-title":"FM 2005: Formal Methods","author":"K. Rustan","year":"2005","unstructured":"Rustan, K., Leino, M., M\u00fcller, P.: Modular verification of static class invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 26\u201342. Springer, Heidelberg (2005)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K. Rustan","year":"2006","unstructured":"Rustan, K., Leino, M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"issue":"5","key":"16_CR21","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K. Rustan","year":"2002","unstructured":"Rustan, K., Leino, M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR22","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1109\/SEFM.2004.1347523","volume-title":"SEFM 2004\u2014Second International Conference on Software Engineering and Formal Methods","author":"K. Rustan","year":"2004","unstructured":"Rustan, K., Leino, M., Schulte, W.: Exception safety for C#. In: Cuellar, J.R., Liu, Z. (eds.) SEFM 2004\u2014Second International Conference on Software Engineering and Formal Methods, September 2004, pp. 218\u2013227. IEEE, Los Alamitos (2004)"},{"key":"16_CR23","series-title":"Series in Computer Science","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International, New York (1988)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11531142_1","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"B. Meyer","year":"2005","unstructured":"Meyer, B.: Attached Types and Their Application to Three Open Problems of Object-Oriented Programming. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 1\u201332. Springer, Heidelberg (2005)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45651-1","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"P. M\u00fcller","year":"2002","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-31984-9_15","volume-title":"Fundamental Approaches to Software Engineering","author":"D.A. Naumann","year":"2005","unstructured":"Naumann, D.A.: Observational purity and encapsulation. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 190\u2013204. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T12:46:38Z","timestamp":1551530798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}