{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:11:41Z","timestamp":1773655901432,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614630","type":"print"},{"value":"9783540685951","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0014320","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T04:04:25Z","timestamp":1132718665000},"page":"241-255","source":"Crossref","is-referenced-by-count":7,"title":["Tracing the origins of verification conditions"],"prefix":"10.1007","author":[{"given":"Ranan","family":"Fraer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"J-R. Abrial. The B-Book. Assigning Programs to Meanings. Cambridge University Press, 1995. (to appear).","DOI":"10.1017\/CBO9780511624162"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Y. Bertot. Occurrences in Debugger Specifications. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 1991.","DOI":"10.1145\/113445.113473"},{"key":"19_CR3","unstructured":"Y. Bertot. Une Automatisation du Calcul des R\u00e9sidus en S\u00e9mantique Naturelle. PhD thesis, Universit\u00e9 de Nice-Sophia Antipolis, 1991."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Y. Bertot. Origin Functions in \u03bb-calculus and Term Rewriting Systems. In CAAP'92, 1992. Springer Verlag LNCS 581.","DOI":"10.1007\/3-540-55251-0_3"},{"key":"19_CR5","unstructured":"Y. Bertot. A Canonical Calculus of Residuals. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 147\u2013163. Cambridge University Press, 1993. (also appears as INRIA Report no. 1542, Oct. 1991)."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"T. Despeyroux. Executable Specifications of Static Semantics. In International Symposium on Semantics of Data Types, 1984. Springer-Verlag LNCS 173.","DOI":"10.1007\/3-540-13346-1_11"},{"key":"19_CR7","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"19_CR8","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1016\/S0747-7171(06)80004-0","volume":"15","author":"A.V. Deursen","year":"1993","unstructured":"A.V. Deursen, P. Klint, and F. Tip. Origin Tracking. In Journal of Symbolic Computation, volume 15, pages 523\u2013545, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"R.W. Floyd. Assigning Meanings to Programs. In J.T. Schwartz, editor, Mathematical Aspects of Computer Science: Proceedings of the 19th Symposium in Applied Mathematics, pages 19\u201332, Providence, United States, 1966.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"1058","DOI":"10.1109\/32.58790","volume":"16","author":"D. Guaspari","year":"1990","unstructured":"D. Guaspari, C. Marceau, and W. Polak. Formal Verification of Acta Programs. In IEEE Transactions on Software Engineering, volume 16, pages 1058\u20131075, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"D.I. Good. Mechanical Proofs about Computer Programs. In C.A.R. Hoare and J.C. Sheperdson, editors, Mathematical Logic and Programming Languages. Prentice Hall, 1985.","DOI":"10.21236\/ADA494739"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. An Axiomatic Basis for Computer Programming. In Communications of the ACM, October 1969.","DOI":"10.1145\/363235.363259"},{"key":"19_CR13","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"S. Igarashi, R.L. London, and D.C. Luckham. Automatic Program Verification: A Logical Basis and its Implementation. In Acta Informatica, volume 4, pages 145\u2013182, 1975.","journal-title":"Acta Informatica"},{"key":"19_CR14","volume-title":"Technical report","author":"I. Jacobs","year":"1994","unstructured":"I. Jacobs. The Centaur Reference Manual. Technical report, INRIA, Sophia-Antipolis, 1994."},{"key":"19_CR15","volume-title":"Technical Report 150","author":"I. Jacobs","year":"1993","unstructured":"I. Jacobs, F. Montagnac, J. Bertot, and D. Clement. The Sophtalk Reference Manual. Technical Report 150, INRIA, Sophia-Antipolis, 1993."},{"key":"19_CR16","unstructured":"C. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986."},{"key":"19_CR17","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1145\/151257.151260","volume":"2","author":"P. Klint","year":"1993","unstructured":"P. Klint. A Meta-environment for Generating Programming Environments. In ACM Transaction on Software Engineering and Methodology, volume 2, pages 176\u2013201, 1993.","journal-title":"ACM Transaction on Software Engineering and Methodology"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"S. Kromodimoeljo, B. Pase, M. Saaltink, D. Craigen, and I. Meisels. The EVES System. In Proceedings of the International Lecture Series on Functional Programming, Concurrency, Simulation and Automated Reasoning, 1992.","DOI":"10.1007\/3-540-56883-2_16"},{"key":"19_CR19","unstructured":"T. Reps and T. Teitelbaum. The Synthesizer Generator: a System for Constructing Language Based Editors. Springer Verlag, 1988. (third edition)."},{"key":"19_CR20","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"M. Weiser. Program Slicing. In IEEE Transactions on Software Engineering, volume 10, page 352, 1984.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:46:32Z","timestamp":1586565992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614630","9783540685951"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0014320","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}