{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:07:31Z","timestamp":1742386051172},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203032"},{"type":"electronic","value":"9783540396567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_10","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:35:52Z","timestamp":1277836552000},"page":"242-261","source":"Crossref","is-referenced-by-count":17,"title":["High-Level Specifications: Lessons from Industry"],"prefix":"10.1007","author":[{"given":"Brannon","family":"Batson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leslie","family":"Lamport","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science\u00a082(2), 253\u2013284 (1991)","journal-title":"Theoretical Computer Science"},{"key":"10_CR2","volume-title":"Machine Intelligence","author":"E.A. Ashcroft","year":"1970","unstructured":"Ashcroft, E.A., Manna, Z.: Formalization of properties of parallel programs. In: Machine Intelligence, vol.\u00a06. Edinburgh University Press, Edinburgh (1970)"},{"key":"10_CR3","volume-title":"Parallel Program Design","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design. Addison-Wesley, Reading (1988)"},{"key":"10_CR4","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panagaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"10_CR5","first-page":"19","volume-title":"Proceedings of the Symposium on Applied Math.","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the Symposium on Applied Math., vol.\u00a019, pp. 19\u201332. American Mathematical Society, Providence (1967)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Gafni, E., Lamport, L.: Disk paxos. To appear in Distributed Computing (2002)","DOI":"10.1007\/s00446-002-0070-8"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Gharachorloo, K., Sharma, M., Steely, S., Van Doren, S.: Architecture and design of AlphaServer GS320. In: Gupta, A. (ed.) Proceedings of the Ninth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS IX), November 2000, pp. 13\u201324 (2000)","DOI":"10.1145\/356989.356991"},{"key":"10_CR8","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"10","key":"10_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"issue":"5","key":"10_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"10_CR11","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"SE-10","author":"S.S. Lam","year":"1984","unstructured":"Lam, S.S., Shankar, A.U.: Protocol verification via projections. IEEE Transactions on Software Engineering\u00a0SE-10(4), 325\u2013342 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering\u00a0SE-3(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"10_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0167-6423(83)90014-X","volume":"2","author":"L. Lamport","year":"1982","unstructured":"Lamport, L.: An assertional correctness proof of a distributed algorithm. Science of Computer Programming\u00a02(3), 175\u2013206 (1982)","journal-title":"Science of Computer Programming"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1007\/BF01211870","volume":"6","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: How to write a long formula. Formal Aspects of Computing\u00a06, 580\u2013584 (1994); First appeared as Research Report 119, Digital Equipment Corporation, Systems Research Center","journal-title":"Formal Aspects of Computing"},{"issue":"3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-49213-5_15","volume-title":"Compositionality: The Significant Difference","author":"L. Lamport","year":"1998","unstructured":"Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 402\u2013423. Springer, Heidelberg (1998)"},{"key":"10_CR17","volume-title":"Specifying Systems","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002); A link to an electronic copy can be found at http:\/\/lamport.org"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Lamport, L., Matthews, J., Tuttle, M., Yu, Y.: Specifying and verifying systems with TLA+. In: Proceedings of the Tenth ACM SIGOPS European Workshop, Saint-Emilion, France, September 2002, pp. 45\u201348. INRIA (Institut National de Recherche en Informatique et en Automatique) (2002)","DOI":"10.1145\/1133373.1133382"},{"issue":"3","key":"10_CR19","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/319301.319317","volume":"21","author":"L. Lamport","year":"1999","unstructured":"Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Transactions on Programming Languages and Systems\u00a021(3), 502\u2013526 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR20","unstructured":"Lamport, L., Sharma, M., Tuttle, M., Yu, Y.: The wildfire verification challenge problem, At URL http:\/\/research.microsoft.com\/users\/lamport\/tla\/wildfire-challenge.html on the World Wide Web; It can also be found by searching the Web for the 24-letter string wildfirechallengeproblem"},{"issue":"5","key":"10_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM\u00a019(5), 279\u2013284 (1976)","journal-title":"Communications of the ACM"},{"issue":"3","key":"10_CR22","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems\u00a04(3), 455\u2013495 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"10_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering\u00a021(2), 107\u2013125 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR24","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on the Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, November 1977, pp. 46\u201357. IEEE, Los Alamitos (1977)"},{"key":"10_CR25","volume-title":"Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions","author":"S. Tasiran","year":"2002","unstructured":"Tasiran, S., Yu, Y., Batson, B., Kreider, S.: Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In: Proceedings of the 3rd IEEE Workshop on Microprocessor Test and Verification, Common Challenges and Solutions. IEEE Computer Society, Los Alamitos (2002)"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 54\u201366. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39656-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T14:56:52Z","timestamp":1559228212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}