{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:43Z","timestamp":1748071603920},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_14","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"234-251","source":"Crossref","is-referenced-by-count":3,"title":["VAlloy \u2014 Virtual Functions Meet a Relational Language"],"prefix":"10.1007","author":[{"given":"Darko","family":"Marinov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"14_CR1","unstructured":"J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In Proc. Fifth International Conference on Principles of Knowledge Representation and Reasoning, 1996."},{"key":"14_CR2","unstructured":"Mukesh Dalal and Dipayan Gangopahyay. OOLP: A translation approach to object-oriented logic programming. In Proc. First International Conference on Deductive and Object-Oriented Databases (DOOD-89), pages 555\u2013568, Kyoto, Japan, December 1989."},{"key":"14_CR3","series-title":"PhD thesis","volume-title":"Dynamically Discovering Likely Program Invariants","author":"M. D. Ernst","year":"2000","unstructured":"Michael D. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington Department of Computer Science and Engineering, Seattle, Washington, August 2000."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Marieke Huisman, Bart Jacobs, and Joachim van den Berg. A case study in class library verification: Java\u2019s Vector class. Software Tools for Technology Transfer, 2001.","DOI":"10.1007\/s100090100047"},{"key":"14_CR5","unstructured":"Daniel Jackson. Micromodels of software: Modelling and analysis with Alloy, 2001. Available online: http:\/\/sdg.lcs.mit.edu\/alloy\/book.pdf ."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Daniel Jackson. Alloy: A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology, 2002. (to appear).","DOI":"10.1145\/505145.505149"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Daniel Jackson and Alan Fekete. Lightweight analysis of object interactions. In Proc. Fourth International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan, October 2001.","DOI":"10.1007\/3-540-45500-0_25"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Daniel Jackson, Ian Schechter, and Ilya Shlyakhter. ALCOA: The Alloy constraint analyzer. In Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337616"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Daniel Jackson, Ilya Shlyakhter, and Manu Sridharan. A micromodularity mechanism. In Proc. 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Vienna, Austria, September 2001.","DOI":"10.1145\/503209.503219"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In Proc. International Symposium on Software Testing and Analysis (ISSTA), Portland, OR, August 2000.","DOI":"10.1145\/347324.383378"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Idit Keidar, Roger Khazan, Nancy Lynch, and Alex Shvartsman. An inheritance-based technique for building simulation proofs incrementally. In Proc. 22nd International Conference on Software Engineering (ICSE), pages 478\u2013487, Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337358"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Sarfraz Khurshid, Darko Marinov, and Daniel Jackson. An analyzable annotation language. In Proc. ACM SIGPLAN 2002 Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA), Seattle, WA, Nov 2002.","DOI":"10.1145\/582419.582441"},{"key":"14_CR13","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, June 1998. (last revision: Aug 2001)."},{"key":"14_CR14","unstructured":"Barbara Liskov. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000."},{"key":"14_CR15","unstructured":"Nancy Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Darko Marinov and Sarfraz Khurshid. TestEra: A novel framework for automated testing of Java programs. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA, November 2001.","DOI":"10.1109\/ASE.2001.989787"},{"key":"14_CR17","unstructured":"Chris Moss. Prolog++ The Power of Object-Oriented and Logic Programming. Addison-Wesley, 1994."},{"key":"14_CR18","unstructured":"Mark Roulo. How to avoid traps and correctly override methods from java.lang.Object. http:\/\/www.javaworld.com\/javaworld\/jw-01-1999\/jw-01-object.html ."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"14_CR21","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992."},{"key":"14_CR22","unstructured":"Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification. http:\/\/java.sun.com\/j2se\/1.3\/docs\/api\/ ."},{"key":"14_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Proc. Tools and Algorithms for the Construction and Analysis of Software (TACAS)","author":"J. Berg van den","year":"2001","unstructured":"Joachim van den Berg and Bart Jacobs. The LOOP compiler for Java and JML. In Proc. Tools and Algorithms for the Construction and Analysis of Software (TACAS), (Springer LNCS 2031, 2001), pages 299\u2013312, Genoa, Italy, April 2001."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T04:12:04Z","timestamp":1587528724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}