{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:13:29Z","timestamp":1742386409040,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_24","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T20:25:09Z","timestamp":1184963109000},"page":"338-345","source":"Crossref","is-referenced-by-count":12,"title":["PVS: An Experience Report"],"prefix":"10.1007","author":[{"given":"S.","family":"Owre","sequence":"first","affiliation":[]},{"given":"J. M.","family":"Rushby","sequence":"additional","affiliation":[]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[]},{"given":"D. W. J.","family":"Stringer-Calvert","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 99","author":"P. A. Abdulla","year":"1999","unstructured":"Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, and Yassine Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In CAV\u201999 [8]."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-63531-9_16","volume-title":"Software Engineering-ESEG\/FSE\u2019 97: Sixth European Software Engineering Conference and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"A. Alborghetti","year":"1997","unstructured":"Andren Alborghetti, Angelo Gargantini, and Angelo Morzenti. Providing auto mated support to deductive analysis of time critical systems. In Mehdi Jazayeri and Helmut Schauer, editors, Software Engineering-ESEG\/FSE\u2019 97: Sixth European Software Engineering Conference and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1301 of Lecture Notes in Computer Science, pages 211\u2013226, Zurich, Switzerland, September 1997. Springer-Verlag."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 96","year":"1996","unstructured":"Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"Myla Archer and Constance Heitmeyer. Mechanical verification of timed au tomata: A case study. In IEEE Real-Time Technology and Applications Symposium (RTAS\u201996), pages 192\u2013203, Brookline, MA, June 1996. IEEE Computer Society.","key":"24_CR4","DOI":"10.1109\/RTTAS.1996.509536"},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-61474-5_80","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"S. Bensalem","year":"1996","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Hassen Sa\u00efdi. Powerful techniques for the automatic generation of invariants. In Thomas A. Henzinger, editors. Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July\/August 1996 Alur and Henzinger [3], pages 323\u2013335."},{"key":"24_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/BFb0000497","volume-title":"Algebraic Methodology and Software Technology, AMAST\u201997","author":"B. Buth","year":"1997","unstructured":"Bettina Buth. PAMELA + PVS. In Michael Johnson, editor, Algebraic Methodology and Software Technology, AMAST\u201997, volume 1349 of Lecture Notes in Computer Science, pages 560\u2013562, Sydney, Australia, December 1997. Springer-Verlag."},{"key":"24_CR7","series-title":"NASA Technical Memorandum","volume-title":"A PVS graph theory library","author":"R. W. Butler","year":"1998","unstructured":"Ricky W. Butler and Jon A. Sjogren. A PVS graph theory library. NASA Technical Memorandum 1998-206923, NASA Langley Research Center, Hampton, VA, February 1998."},{"unstructured":"Computer-Aided Verification, CAV\u2019 99, Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag. To appear.","key":"24_CR8"},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0028757","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"R. Couturier","year":"1998","unstructured":"Raphael Couturier and Dominique M\u00e9ry. An experiment in parallelizing an appli cation using formal methods. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 345\u2013356."},{"issue":"3","key":"24_CR10","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1145\/287000.287023","volume":"7","author":"J. Crow","year":"1998","unstructured":"Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle software requirements: Four case studies. ACM Transactions on Software Engineering and Methodology, 7(3):296\u2013332, July 1998.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"doi-asserted-by":"crossref","unstructured":"Drew Dean. Static typing with dynamic linking. In Fourth ACM Conference on Computer and Communications Security, pages 18\u201327, Zurich, Switzerland, April 1997. Association for Computing Machinery.","key":"24_CR11","DOI":"10.1145\/266420.266428"},{"unstructured":"Darryl Dieckman, Perry Alexander, and Philip A. Wilsey. ActiveSPEC: A frame work for the specification and verification of active network services and secu rity policies. In Nevin Heintze and Jeannette Wing, editors, Workshop on Formal Methods and Security Protocols, Indianapolis, IN, June 1998. Informal proceedings available at http:\/\/www.cs.bell-labs.com\/who\/nch\/fmsp\/program.html .","key":"24_CR12"},{"issue":"5","key":"24_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1109\/32.588520","volume":"23","author":"B. Dutertre","year":"1997","unstructured":"Bruno Dutertre and Victoria Stavridou. Formal requirements analysis of an avion ics control system. IEEE Transactions on Software Engineering, 23(5):267\u2013278, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"24_CR14","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/32.663994","volume":"24","author":"S. Easterbrook","year":"1998","unstructured":"Steve Easterbrook, Robyn Lutz, Richard Covington, John Kelly, Yoko Ampo, and David Hamilton. Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering, 24(1):4\u201314, January 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"Formal Methods Europe FME\u2019 97, volume 1313 of Lecture Notes in Computer Science, Graz, Austria, September 1997. Springer-Verlag.","key":"24_CR15"},{"doi-asserted-by":"crossref","unstructured":"Simon Fowler and Andy Wellings. Formal development of a real-time kernel. In Real Time Systems Symposium, pages 220\u2013229, San Francisco, CA, December 1997. IEEE Computer Society.","key":"24_CR16","DOI":"10.1109\/REAL.1997.641284"},{"doi-asserted-by":"crossref","unstructured":"Ganesh Gopalakrishnan and Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD\u2019 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998. Springer-Verlag.","key":"24_CR17","DOI":"10.1007\/3-540-49519-3"},{"doi-asserted-by":"crossref","unstructured":"David Greve. Symbolic simulation of the JEM1 microprocessor. In Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD\u2019 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 321\u2013333.","key":"24_CR18","DOI":"10.1007\/3-540-49519-3_21"},{"key":"24_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BFb0028729","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"D. Hardin","year":"1998","unstructured":"David Hardin, Matthew Wilding, and David Greve. Transforming the theorem-prover into a digital design tool: From concept car to off-road vehicle. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 39\u201344."},{"key":"24_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"Formal Methods Europe FME\u2019 96","author":"K. Havelund","year":"1996","unstructured":"Klaus Havelund and N. Shankar. Experiments in theorem proving and model check ing for protocol verification. In Formal Methods Europe FME\u2019 96, volume 1051 of Lecture Notes in Computer Science, pages 662\u2013681, Oxford, UK, March 1996. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"Mats P. E. Heimdahl and Barbara J. Czerny. Using PVS to analyze hierarchi cal state-based requirements for completeness and consistency. In IEEE High-Assurance Systems Engineering Workshop (HASE\u2019 96), pages 252\u2013262, Niagara on the Lake, Canada, October 1996.","key":"24_CR21","DOI":"10.1109\/HASE.1996.618606"},{"key":"24_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0028731","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"J. Hoffman","year":"1998","unstructured":"John Hoffman and Charlie Payne. A formal experience at Secure Computing Cor poration. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 49\u201356."},{"key":"24_CR23","series-title":"Lect Notes Comput Sci","first-page":"276","volume-title":"Compositionality: The Sig nificant Difference (Revised lectures from International Symposium COMPOS\u201997)","author":"J. Hooman","year":"1997","unstructured":"Jozef Hooman. Compositional verification of real-time applications. In Willem Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Compositionality: The Sig nificant Difference (Revised lectures from International Symposium COMPOS\u201997), volume 1536 of Lecture Notes in Computer Science, pages 276\u2013300, Bad Malente, Germany, September 1997. Springer-Verlag."},{"key":"24_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 99","author":"R. Hosabettu","year":"1999","unstructured":"Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Proof of correct ness of a processor with reorder buffer using the completion functions approach. In CAV\u201999 [8]."},{"key":"24_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 98","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag."},{"issue":"10","key":"24_CR26","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1145\/286936.286973","volume":"33","author":"B. Jacobs","year":"1998","unstructured":"Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum, Ulrich Hensel, and Hendrick Tews. Reasoning about Java classes. In Proceedings, ObjectO-riented Programming Systems, Languages and Applications (OOPSLA\u2019 98), pages 329\u2013340, Vancouver, Canada, October 1998. Association for Computing Machinery. Proceedings issued as ACM SIGPLAN Notices Vol. 33, No. 10, October 1998.","journal-title":"Proceedings, ObjectO-riented Programming Systems, Languages and Applications (OOPSLA\u2019 98)"},{"key":"24_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/3-540-63533-5_31","volume-title":"Formal Methods Europe FME\u2019 97","author":"P. Kellom\u00e4ki","year":"1997","unstructured":"Pertti Kellom\u00e4ki. Verification of reactive systems using DisCo and PVS. In FME [15], pages 589\u2013604."},{"doi-asserted-by":"crossref","unstructured":"Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE compliant sub-tractive division algorithms. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 96), volume 1166 of Lec ture Notes in Computer Science, pages 64\u201378, Palo Alto, CA, November 1996. Springer-Verlag.","key":"24_CR28","DOI":"10.1007\/BFb0031800"},{"doi-asserted-by":"crossref","unstructured":"Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan. Formalization and proof of a solution to the PCI 2.1 bus transaction ordering problem. In Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD\u2019 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 237\u2013254.","key":"24_CR29","DOI":"10.1007\/3-540-49519-3_17"},{"key":"24_CR30","series-title":"Technical Report SRI-CSL","volume-title":"PBS: Support for the B-method in PVS","author":"C. Mu\u00f1oz","year":"1999","unstructured":"C\u00e9sar Mu\u00f1oz. PBS: Support for the B-method in PVS. Technical Report SRI-CSL 99-1, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1999."},{"key":"24_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Thomas A. Henzinger, editors. Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July\/August 1996 Alur and Henzinger [3], pages 411\u2013414."},{"key":"24_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/BFb0035400","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 97)","author":"S. Owre","year":"1997","unstructured":"Sam Owre, John Rushby, and N. Shankar. Integration in PVS: Tables, types, and model checking. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 97), volume 1217 of Lecture Notes in Computer Science, pages 366\u2013383, Enschede, The Netherlands, April 1997. Springer-Verlag."},{"issue":"2","key":"24_CR33","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"24_CR34","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/s002240000093","volume":"31","author":"S. Park","year":"1998","unstructured":"Seungjoon Park and David L. Dill. Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems, 31(4):355\u2013376, 1998.","journal-title":"Theory of Computing Systems"},{"key":"24_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-540-49382-2_18","volume-title":"18th Conference on the Foundations of Software Technology and Theoretical Computer Science","author":"N.S. Pendharkar","year":"1998","unstructured":"N.S. Pendharkar and K. Gopinath. Formal verification of an O.S. submodule. In V. Arvind and R. Ramanujin, editors, 18th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1530 of Lecture Notes in Computer Science, pages 197\u2013208, Madras, India, December 1998. Springer-Verlag."},{"key":"24_CR36","first-page":"193","volume-title":"Dependable Computing for Critical Applications-7","author":"H. Pfeifer","year":"1999","unstructured":"Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke. Formal verification for time-triggered clock synchronization. In Rushby [41], pages 193\u2013212."},{"doi-asserted-by":"crossref","unstructured":"Amir Pnueli and Tamara Arons. Verification of data-insensitive circuits: An in order-retirement case study. In Phillip Windley, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 351\u2013368.","key":"24_CR37","DOI":"10.1007\/3-540-49519-3_23"},{"doi-asserted-by":"crossref","unstructured":"S. P. Rajan, M. Fujita, K. Yuan, and M. T-C. Lee. ATM switch design by high level modeling, formal verification, and high level synthesis. ACM Transactions on Design Automation of Electronic Systems (TODAES), 3(4), October 1998.","key":"24_CR38","DOI":"10.1145\/296333.296342"},{"unstructured":"John Rushby. PVS bibliography. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA. Constantly updated; available at http:\/\/www.csl.sri.com\/pvs-bib.html .","key":"24_CR39"},{"doi-asserted-by":"crossref","unstructured":"John Rushby. Formal methods and their role in the certification of critical systems. In Roger Shaw, editor, Safety and Reliability of Software Based Systems (Twelfth Annual CSR Workshop), pages 1\u201342, Bruges, Belgium, September 1995. Springer.","key":"24_CR40","DOI":"10.1007\/978-1-4471-0921-1_1"},{"volume-title":"Dependable Computing for Critical Applications-7","year":"1999","unstructured":"John Rushby, editor. Dependable Computing for Critical Applications-7, Dependable Computing and Fault Tolerant Systems, San Jose, CA, January 1999. IEEE Computer Society. To appear (page numbers refer to preliminary proceedings).","key":"24_CR41"},{"issue":"9","key":"24_CR42","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709\u2013720, September 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR43","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 99","author":"H. Sa\u00efdi","year":"1999","unstructured":"Hassen Sa\u00efdi and N. Shankar. Abstract and model check while you prove. In CAV\u201999 [8]."},{"key":"24_CR44","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/3-540-58468-4_189","volume-title":"Formal Tech niques in Real-Time and Fault-Tolerant Systems","author":"J. U. Skakkebjk","year":"1994","unstructured":"Jens U. Skakkebjk and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Tech niques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 660\u2013679, L\u00fcbeck, Germany, September 1994. Springer Verlag."},{"key":"24_CR45","volume-title":"Mechanical Verification of Compiler Correctness","author":"D. W. J. Stringer-Calvert","year":"1998","unstructured":"David W. J. Stringer-Calvert. Mechanical Verification of Compiler Correctness. PhD thesis, University of York, Department of Computer Science, York, England, March 1998. Available at http:\/\/www.csl.sri.com\/dave.sc\/papers\/thesis.html ."},{"key":"24_CR46","first-page":"473","volume":"44","author":"K. Umamageswaran","year":"1998","unstructured":"Kothanda Umamageswaran, Krishnan Subramani, Philip A. Wilsey, and Perry Alexander. Formal verification and empirical analysis of rollback relaxation. Jour nal of Systems Architecture (formerly published as Microprocessing and Micropro gramming: the Euromicro Journal), 44:473\u2013495, 1998.","journal-title":"Jour nal of Systems Architecture (formerly published as Microprocessing and Micropro gramming: the Euromicro Journal)"},{"key":"24_CR47","first-page":"251","volume-title":"Dependable Computing for Critical Applications-7","author":"B. L. Vito Di","year":"1999","unstructured":"Ben L. Di Vito. A model of cooperative noninterference for integrated modular avionics. In Rushby [41], pages 251\u2013268."},{"key":"24_CR48","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/BFb0055152","volume-title":"The orem Proving in Higher Order Logics: 11th International Conference, TPHOLs\u2019 98","author":"F. Henke von","year":"1998","unstructured":"Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rue\u00df. Case studies in meta-level theorem proving. In Jim Grundy and Malcolm Newey, editors, The orem Proving in Higher Order Logics: 11th International Conference, TPHOLs\u2019 98, volume 1479 of Lecture Notes in Computer Science, pages 461\u2013478, Canberra, Australia, September 1998. Springer-Verlag."},{"key":"24_CR49","series-title":"Research Report","volume-title":"Verification and abstraction of flow-graph programs with pointers and computed jumps","author":"M. Wahab","year":"1998","unstructured":"M. Wahab. Verification and abstraction of flow-graph programs with pointers and computed jumps. Research Report CS-RR-354, Department of Computer Science, University of Warwick, Coventry, UK, November 1998. Available at http:\/\/www.dcs.warwick.ac.uk\/pub\/reports\/rr\/354.html ."},{"key":"24_CR50","first-page":"269","volume-title":"Dependable Computing for Critical Applications-7","author":"M. M. Wilding","year":"1999","unstructured":"Matthew M. Wilding, David S. Hardin, and David A. Greve. Invariant perfor mance: A statement of task isolation useful for embedded application integration. In Rushby [41], pages 269\u2013282."}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T20:56:08Z","timestamp":1737320168000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}