{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T10:41:34Z","timestamp":1648982494234},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540606093","type":"print"},{"value":"9783540484639","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60609-2_10","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:46:24Z","timestamp":1330289184000},"page":"184-205","source":"Crossref","is-referenced-by-count":1,"title":["Formal methods in practice: A comparison of two support systems for proof"],"prefix":"10.1007","author":[{"given":"Juan C.","family":"Bicarregui","sequence":"first","affiliation":[]},{"given":"Brian M.","family":"Matthews","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,6]]},"reference":[{"key":"10_CR1","unstructured":"J-R Abrial. Deriving Programs from Meaning. Prentice Hall International, 1995. To appear."},{"key":"10_CR2","unstructured":"B-Core (UK) Ltd. B-Toolkit User's Manual, release version 2.0 edition, 1994. A full release of the B Toolkit is now available. For details, contact Ib Sorensen, B Core (UK) Ltd, Magdalen Centre, Robert Robinson Avenue, The Oxford Science Park, Oxford OX4 4GA. Tel: +44 865 784520. E-mail: Ib.Sorensen@comlab.ox.ac.uk."},{"key":"10_CR3","unstructured":"J.C. Bicarregui, et al. Formal Methods into Practice: case studies in the application of the B-Method, B User Trials Deliverable, D 18, Rutherford Appleton Laboratory. Submitted to the Software Engineering Journal."},{"key":"10_CR4","volume-title":"Supporting the length of formal development: from diagrams to VDM to B to C","author":"J.C. Bicarregui","year":"1995","unstructured":"J.C. Bicarregui, J. Dick and E. Woods, Supporting the length of formal development: from diagrams to VDM to B to C Proceedings, 7th International Conference on: Putting into practice method and tools for information system design\u201d, Nantes (France), October '95, IUT de Nantes, H. Habrias (Editor) 1995."},{"key":"10_CR5","unstructured":"J.C. Bicarregui, J. Dick and E. Woods, Qualitative analysis of an application of formal methods. Submitted to FME'96, Springer-Verlag."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"J C Bicarregui, J S Fitzgerald, P A Lindsay, R Moore, and B Ritchie. Proof in VDM: A Practitioner's Guide. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"J C Bicarregui and B Ritchie. Reasoning about VDM developments using the VDM support tool in Mural. In Proc. of VDM'91: Formal Software Development Methods, volume 552 of Lecture Notes in Computer Science. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54834-3_23"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"J C Bicarregui and B Ritchie. Invariants, frames and postconditions: a comparison of the VDM and B notations. In J C P Woodcock and P G Larsen, editors, Proc. of Formal Methods Europe'93: Industrial Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 162\u2013182. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0024645"},{"key":"10_CR9","unstructured":"D. Clutterbuck, J.C. Bicarregui and B. Matthews. Experiences with Proof in Formal Development. Submitted to FME'96, Springer-Verlag."},{"key":"10_CR10","unstructured":"Jeremy Dick and Jerome Loubersac. A Visual Approach to VDM: Entity-Structure Diagrams. Technical Report DE\/DRPA\/91001, Bull, 68, Route de Versailles, 78430 Louveciennes (France), January 1991."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Stephen J Garland and John V Guttag. An overview of LP, the Larch Prover. In N Dershowitz, editor, Proc. 3rd Conference on Rewriting Techniques and Applications., volume 355 of Lecture Notes in Computer Science, pages 137\u2013151. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_105"},{"key":"10_CR12","unstructured":"Chris George and S\u00f8ren Prehn. The RAISE Justification Handbook. Draft Manual, 1993."},{"key":"10_CR13","unstructured":"M J C Gordon and T F Melham. Introduction to HOL. Cambridge University Press, 1993."},{"key":"10_CR14","unstructured":"C B Jones. Systematic Softare Development using VDM. Prentice Hall International, 2nd edition, 1990."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"C B Jones, K.D. Jones, P.A.Lindsay, R.Moore. Mural; A formal Development Support Environment. IBSN 3-540-19651-X, Springer Verlag, 1991.","DOI":"10.1007\/978-1-4471-3180-9"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"R B Jones. Methods and tools for the verification of critical properties. In R Shaw, editor, Proc. of 5th BSC-FACS Refinement Workshop. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3550-0_6"},{"key":"10_CR17","unstructured":"Andrew Martin. Encoding W: A Logic for Z in 2OBJ. In J C P Woodcock and P G Larsen, editors, Proc. of Formal Methods Europe'93: Industrial Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462\u2013481. Springer-Verlag, 1993."},{"key":"10_CR18","unstructured":"C. Morgan. Programming From Specifications. Prentice Hall, 1990."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"B. Ritchie, J. Bicarregui, and H. Haughton. Experiences in Using the Abstract machine Notation in a GKS Case Study. In Proc. of FME'94, volume 873 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58555-9_90"},{"key":"10_CR20","unstructured":"J.M. Spivey. The Z Notaion (Second Edition). Prentice Hall, 1993."},{"key":"10_CR21","volume-title":"PhD thesis","author":"S. Vadera","year":"1992","unstructured":"Sunil Vadera. Heuristics for Proofs. PhD thesis, University of Manchester, Manchester M13 9PL, UK, 1992."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"J C P Woodcock and S Brien. W: a Logic for Z. In Procs of the 6th Z User Group Meeting. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3203-5_4"},{"key":"10_CR23","unstructured":"E. Woods. M.Sc. Thesis. University of Manchester, 1995."},{"key":"10_CR24","unstructured":"E. Woods and J. Dick. Lessons Learned Applying Formal Methods to Systems Software Development. IEE Software, to appear."}],"container-title":["SOFSEM '95: Theory and Practice of Informatics","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60609-2_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:00:35Z","timestamp":1605646835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60609-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540606093","9783540484639"],"references-count":24,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-60609-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1995]]}}}