{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T13:25:59Z","timestamp":1773235559289,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642112652","type":"print"},{"value":"9783642112669","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11266-9_34","type":"book-chapter","created":{"date-parts":[[2009,12,7]],"date-time":"2009-12-07T14:04:58Z","timestamp":1260194698000},"page":"407-418","source":"Crossref","is-referenced-by-count":6,"title":["Practically Applicable Formal Methods"],"prefix":"10.1007","author":[{"given":"J\u0119drzej","family":"Fulara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krzysztof","family":"Jakubczyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"2006","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison Wesley, Reading (2006)","edition":"2"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Dealing with Numeric Fields in Termination Analysis of Java-Like Languages. In: FTfJP, pp. 77\u201387 (2008)","DOI":"10.1007\/978-3-540-68863-1_2"},{"key":"34_CR3","unstructured":"Andersen, M., Barnett, M., F\u00c4hndrich, M., Grunkemeyer, B., King, K., Logozzo, F.: Code Contracts User Manual"},{"key":"34_CR4","volume-title":"Test Driven Development: By Example","author":"K. Beck","year":"2002","unstructured":"Beck, K.: Test Driven Development: By Example. Addison-Wesley Professional, Reading (2002)"},{"key":"34_CR5","first-page":"332","volume-title":"Proceedings of 21st\u00a0International Computer Software and Application Conference (COMPSAC 1997)","author":"J.P. Bowen","year":"1997","unstructured":"Bowen, J.P., Hinchey, M.G.: The Use of Industrial-Strength Formal Methods. In: Proceedings of 21st\u00a0International Computer Software and Application Conference (COMPSAC 1997), pp. 332\u2013337. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"3","key":"34_CR6","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An Overview of JML Tools and Applications. Int. J. Softw. Tools Technol. Transf.\u00a07(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-68237-0_18","volume-title":"FM 2008: Formal Methods","author":"P. Chalin","year":"2008","unstructured":"Chalin, P., Rioux, F.: JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 246\u2013261. Springer, Heidelberg (2008)"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Cielecki, M., Fulara, J., Jakubczyk, K., Jancewicz, L.: Propagation of JML Non-Null Annotations in Java Programs. PPPJ, 135\u2013140 (2006)","DOI":"10.1145\/1168054.1168073"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML: Progress and Issues in Building and Using ESC\/Java2 and a Report on a\u00a0Case Study Involving the Use of ESC\/Java2 to Verify Portions of an Internet Voting Tally System. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"34_CR10","unstructured":"Cousot, P.: Avionic Software Verification by Abstract Interpretation. In: 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation. Special Workshop Theme: Formal Methods in Avionics, Space and Transport, Poitiers, France, December 12-14 (2007)"},{"key":"34_CR11","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT 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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Craigen, D., Craigen, D., Canada, O., Canada, O., Gerhart, S., Gerhart, S., Ralston, T., Brown, R.H.: An International Survey of Industrial Applications of Formal Methods, vol.\u00a02 Case studies (1993)","DOI":"10.1016\/B978-0-8155-1362-9.50005-6"},{"issue":"1","key":"34_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1327452.1327492","volume":"51","author":"J. Dean","year":"2008","unstructured":"Dean, J., Ghemawat, S.: Mapreduce: Simplified Data Processing on Large Clusters. Commun. ACM\u00a051(1), 107\u2013113 (2008)","journal-title":"Commun. ACM"},{"issue":"1-3","key":"34_CR14","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"M.D. Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon System for Dynamic Detection of Likely Invariants. Science of Computer Programming\u00a069(1-3), 35\u201345 (2007)","journal-title":"Science of Computer Programming"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Rustan, K., Leino, M.: Houdini, an Annotation Assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"issue":"2","key":"34_CR16","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/s10270-002-0015-5","volume":"2","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: the Play-in\/Play-out Approach. Software and System Modeling\u00a02(2), 82\u2013107 (2003)","journal-title":"Software and System Modeling"},{"issue":"12","key":"34_CR17","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1052883.1052895","volume":"39","author":"D. Hovemeyer","year":"2004","unstructured":"Hovemeyer, D., Pugh, W.: Finding Bugs is Easy. SIGPLAN Not.\u00a039(12), 92\u2013106 (2004)","journal-title":"SIGPLAN Not."},{"key":"34_CR18","unstructured":"Leavens, G., Cheon, Y.: Design by Contract with JML (2003)"},{"key":"34_CR19","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual"},{"key":"34_CR20","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall PTR, Englewood Cliffs (1997)"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Moor, O., Sereni, D., Verbaere, M., Hajiyev, E., Avgustinov, P., Ekman, T., Ongkingco, N., Tibble, J.: QL: Object-Oriented Queries Made Easy. In: Generative and Transformational Techniques in Software Engineering\u00a0II: International Summer School, GTTSE\u00a02007, Braga, Portugal, Revised Papers, July 2-7, pp. 78\u2013133 (2008)","DOI":"10.1007\/978-3-540-88643-3_3"},{"key":"34_CR22","unstructured":"Walton, L.: Eclipse Metrics Plugin, http:\/\/metrics.sourceforge.net\/"},{"key":"34_CR23","first-page":"385","volume-title":"APSEC 2008: Proceedings of the 2008 15th\u00a0Asia-Pacific Software Engineering Conference","author":"J. Yoo","year":"2008","unstructured":"Yoo, J., Cha, S., Jee, E.: A Verification Framework for fbd Based Software in Nuclear Power Plants. In: APSEC 2008: Proceedings of the 2008 15th\u00a0Asia-Pacific Software Engineering Conference, Washington, DC, USA, pp. 385\u2013392. IEEE Computer Society, Los Alamitos (2008)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2010: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11266-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T08:44:50Z","timestamp":1558687490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11266-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642112652","9783642112669"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11266-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}