{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:22Z","timestamp":1725558982879},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250791"},{"type":"electronic","value":"9783540318453"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31845-3_4","type":"book-chapter","created":{"date-parts":[[2010,7,5]],"date-time":"2010-07-05T15:43:57Z","timestamp":1278344637000},"page":"41-52","source":"Crossref","is-referenced-by-count":0,"title":["A Program Verification System Based on Oz"],"prefix":"10.1007","author":[{"given":"Isabelle","family":"Dony","sequence":"first","affiliation":[]},{"given":"Baudouin","family":"Le Charlier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"The Mozart Programming System, http:\/\/www.mozart-oz.org"},{"key":"4_CR2","unstructured":"The PVS specification and verification system, http:\/\/pvs.csl.sri.com"},{"key":"4_CR3","unstructured":"Bal, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (2000)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.: A language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 93\u2013112. Springer, Heidelberg (2000)"},{"issue":"2","key":"4_CR5","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/276393.276396","volume":"20","author":"S.J.D. Jackson","year":"1998","unstructured":"Jackson, S.J.D., Damon, C.A.: Isomorph-free model enumeration: a new method for checking relational specifications. ACM Trans. on Programming Languages and Systems\u00a020(2), 302\u2013343 (1998)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/3-540-61042-1_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C.A. Damon","year":"1996","unstructured":"Damon, C.A., Jackson, D.: Efficient search as a means of executing specifications. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 70\u201386. Springer, Heidelberg (1996)"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Clarke, E.M., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Langages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Langages and Systems"},{"key":"4_CR8","first-page":"84","volume-title":"Proc. of the conference record of the Fifth annual ACM Symptium on Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of the conference record of the Fifth annual ACM Symptium on Principles of Programming Languages, Tukson, Arizona, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. of Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332. Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Hoare., C.A.R.: An axiomatic definition of semantics. Communications of the ACM\u00a012(10) (1969)","DOI":"10.1145\/363235.363259"},{"issue":"2","key":"4_CR11","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/210134.210135","volume":"4","author":"D. Jackson","year":"1995","unstructured":"Jackson, D.: Aspect: Detecting bugs with abstract dependences. ACM Trans. on Software Engineering and Methodology\u00a04(2), 109\u2013145 (1995)","journal-title":"ACM Trans. on Software Engineering and Methodology"},{"key":"4_CR12","unstructured":"Charlier, B.L., Derroite, M.: Un syst\u00e8me d\u2019aide \u00e0 l\u2019enseignement d\u2019une m\u00e9thode de programmation. In: Actes du premier colloque francophone sur la didactique de l\u2019informatique (1989)"},{"key":"4_CR13","unstructured":"Moussa, L., Dieul, E.: VICS, verification of an implementation conforming to its specification, http:\/\/vics.sourceforge.net"},{"key":"4_CR14","unstructured":"Schulte, C.: Programming constraint services. Master\u2019s thesis, Saarbrucken (2000)"},{"key":"4_CR15","volume-title":"Concepts, Techniques, and Models of Computer Programming","author":"P. Roy Van","year":"2004","unstructured":"Van Roy, P., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. The MIT Press, Cambridge (2004)"}],"container-title":["Lecture Notes in Computer Science","Multiparadigm Programming in Mozart\/Oz"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31845-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T15:18:47Z","timestamp":1559229527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31845-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250791","9783540318453"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31845-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}