{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T05:30:06Z","timestamp":1672983006698},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2000,8,24]]},"DOI":"10.1145\/349360.351127","type":"proceedings-article","created":{"date-parts":[[2004,2,4]],"date-time":"2004-02-04T23:19:04Z","timestamp":1075936744000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Using TAME to prove invariants of automata models"],"prefix":"10.1145","author":[{"given":"Myla","family":"Archer","sequence":"first","affiliation":[{"name":"Naval Research Lab., Washington, DC"}]},{"given":"Constance","family":"Heitmeyer","sequence":"additional","affiliation":[{"name":"Naval Research Lab., Washington, DC"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[{"name":"Universita di Catania, Catania, Italy"}]}],"member":"320","published-online":{"date-parts":[[2000,8,24]]},"reference":[{"key":"e_1_3_2_1_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/267895.267912"},{"key":"e_1_3_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/524958.828344"},{"key":"e_1_3_2_1_4_2","series-title":"Lect","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0028384","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs'97)","author":"Archer Myla","year":"1997","unstructured":"Myla Archer and Constance Heitmeyer . Human-style theorem proving using PVS . In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics (TPHOLs'97) , volume 1275 of Lect . Notes in Comp. Sci., pages 33 - 48 . Springer-Verlag , 1997 . Myla Archer and Constance Heitmeyer. Human-style theorem proving using PVS. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics (TPHOLs'97), volume 1275 of Lect. Notes in Comp. Sci., pages 33-48. Springer-Verlag, 1997."},{"key":"e_1_3_2_1_5_2","doi-asserted-by":"crossref","unstructured":"Myla\n Archer\n and \n Constance\n Heitmeyer\n .\n Verifying hybrid systems modeled as timed automata: A case study. InHybrid and Real-Time Systems (HART'97) volume \n 1201\n of \n Lect\n . Notes in Comp. Sci. pages \n 171\n -\n 185\n . \n Springer-Verlag 1997\n . Myla Archer and Constance Heitmeyer. Verifying hybrid systems modeled as timed automata: A case study. InHybrid and Real-Time Systems (HART'97) volume 1201 of Lect. Notes in Comp. Sci. pages 171-185. Springer-Verlag 1997.","DOI":"10.1007\/BFb0014724"},{"key":"e_1_3_2_1_6_2","volume-title":"Proc. User Interfaces for Theorem Provers 1998 (UITP '98)","author":"Archer Myla","year":"1998","unstructured":"Myla Archer , Constance Heitmeyer , and Steve Sims . TAME : A PVS interface to simplify proofs for automata models . In Proc. User Interfaces for Theorem Provers 1998 (UITP '98) , Eindhoven, Netherlands , July 1998 . Myla Archer, Constance Heitmeyer, and Steve Sims. TAME: A PVS interface to simplify proofs for automata models. In Proc. User Interfaces for Theorem Provers 1998 (UITP '98), Eindhoven, Netherlands, July 1998."},{"key":"e_1_3_2_1_7_2","volume-title":"NASA Technical Memorandum 110255","author":"Butler Ricky W.","year":"1996","unstructured":"Ricky W. Butler . An introduction to requirements capture using PVS: Specification of a simple autopilot , NASA Technical Memorandum 110255 . NASA Langley Research Center , May 1996 . Ricky W. Butler. An introduction to requirements capture using PVS: Specification of a simple autopilot, NASA Technical Memorandum 110255. NASA Langley Research Center, May 1996."},{"key":"e_1_3_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1995.521893"},{"key":"e_1_3_2_1_9_2","first-page":"40","volume-title":"Proc. First ACM Workshop on Formal Methods in Software Practice (FMSP'96)","author":"Crow Judith","year":"1996","unstructured":"Judith Crow and Ben L . Di Vito. Formalizing space shuttle software requirements . In Proc. First ACM Workshop on Formal Methods in Software Practice (FMSP'96) , pages 40 - 48 , San Diego, CA , January 1996 . Judith Crow and Ben L. Di Vito. Formalizing space shuttle software requirements. In Proc. First ACM Workshop on Formal Methods in Software Practice (FMSP'96), pages 40-48, San Diego, CA, January 1996."},{"key":"e_1_3_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/287000.287023"},{"key":"e_1_3_2_1_11_2","volume-title":"Verification of a tree-identity protocol. URL http:\/\/www.cs.kun.nl\/~marcod\/1394.html","author":"Devillers M.","year":"1997","unstructured":"M. Devillers . Verification of a tree-identity protocol. URL http:\/\/www.cs.kun.nl\/~marcod\/1394.html , 1997 . M. Devillers. Verification of a tree-identity protocol. URL http:\/\/www.cs.kun.nl\/~marcod\/1394.html, 1997."},{"key":"e_1_3_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008764923992"},{"key":"e_1_3_2_1_13_2","volume-title":"Private communication","author":"Devillers Marco","year":"1999","unstructured":"Marco Devillers . Private communication . January , 1999 . Marco Devillers. Private communication. January, 1999."},{"key":"e_1_3_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/259380.259422"},{"key":"e_1_3_2_1_15_2","volume-title":"Draft. MIT Laboratory for Computer Science","author":"Garland S. J.","year":"1998","unstructured":"S. J. Garland and N. A. Lynch . The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems . Draft. MIT Laboratory for Computer Science , August , 1998 . S. J. Garland and N. A. Lynch. The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Draft. MIT Laboratory for Computer Science, August, 1998."},{"key":"e_1_3_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.730543"},{"key":"e_1_3_2_1_18_2","volume-title":"How to write a proof.Technical report","author":"Lamport L.","year":"1993","unstructured":"L. Lamport . How to write a proof.Technical report , Digital Equipment Corp., System Research Center , February 1993 . Research Report 94. L. Lamport. How to write a proof.Technical report, Digital Equipment Corp., System Research Center, February 1993. Research Report 94."},{"key":"e_1_3_2_1_19_2","volume-title":"Private communication","author":"Lincoln Patrick","year":"1998","unstructured":"Patrick Lincoln . Private communication . July , 1998 . Patrick Lincoln. Private communication. July, 1998."},{"key":"e_1_3_2_1_20_2","volume-title":"Using simulation techniques to prove timing properties. Master's thesis","author":"Luchangco Victor","year":"1995","unstructured":"Victor Luchangco . Using simulation techniques to prove timing properties. Master's thesis , Massachusetts Institute of Technology , June 1995 . Victor Luchangco. Using simulation techniques to prove timing properties. Master's thesis, Massachusetts Institute of Technology, June 1995."},{"issue":"3","key":"e_1_3_2_1_21_2","first-page":"219","article-title":"An introduction to Input\/Output automata","volume":"2","author":"Lynch N.","year":"1989","unstructured":"N. Lynch and M. Tuttle . An introduction to Input\/Output automata . CWI-Quarterly , 2 ( 3 ): 219 - 246 , September 1989 . Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands. N. Lynch and M. Tuttle. An introduction to Input\/Output automata. CWI-Quarterly, 2(3):219-246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.","journal-title":"CWI-Quarterly"},{"key":"e_1_3_2_1_22_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_2_1_23_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_3_2_1_24_2","first-page":"74","volume-title":"Proc. 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques","author":"Miller Steve","year":"1998","unstructured":"Steve Miller . The industrial use of formal methods: Was Darwin right ? In Proc. 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques , pages 74 - 82 , Boca Raton, FL , October , 1998 . Steve Miller. The industrial use of formal methods: Was Darwin right? In Proc. 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques, pages 74-82, Boca Raton, FL, October, 1998."},{"key":"e_1_3_2_1_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/527212.837427"},{"key":"e_1_3_2_1_27_2","unstructured":"J. Romijn. Tackling the RPC-Memory Specification Problem with I\/O automata. Addendum. URL http:\/\/www.cwi.nl\/~judi\/papers\/ dagstuhl proofs.ps.gz. J. Romijn. Tackling the RPC-Memory Specification Problem with I\/O automata. Addendum. URL http:\/\/www.cwi.nl\/~judi\/papers\/ dagstuhl proofs.ps.gz."},{"key":"e_1_3_2_1_28_2","series-title":"Lect","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/BFb0024438","volume-title":"Formal Systems Specification - The RPC-Memory Specification Case","author":"Romijn J.","year":"1996","unstructured":"J. Romijn . Tackling the RPC-Memory Specification Problem with I\/O automata . In M. Broy, S. Merz, and K. Spies, editors, Formal Systems Specification - The RPC-Memory Specification Case , volume 1169 of Lect . Notes in Comp. Sci., pages 437 - 476 . Springer-Verlag , 1996 . J. Romijn. Tackling the RPC-Memory Specification Problem with I\/O automata. In M. Broy, S. Merz, and K. Spies, editors, Formal Systems Specification - The RPC-Memory Specification Case, volume 1169 of Lect. Notes in Comp. Sci., pages 437-476. Springer-Verlag, 1996."},{"key":"e_1_3_2_1_29_2","volume-title":"Proc. 1992 Workshop on Types and Proofs for Programs","author":"Rudnicki P.","year":"1996","unstructured":"P. Rudnicki and A. Trybulec . A note on \\How to Write a Proof \". In Proc. 1992 Workshop on Types and Proofs for Programs , June 1996 . Available through P. Rudnicki's web page at http:\/\/www.cs.ualberta.ca\/~piotr\/Mizar\/. P. Rudnicki and A. Trybulec. A note on \\How to Write a Proof \". In Proc. 1992 Workshop on Types and Proofs for Programs, June 1996. Available through P. Rudnicki's web page at http:\/\/www.cs.ualberta.ca\/~piotr\/Mizar\/."},{"key":"e_1_3_2_1_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/646843.706642"}],"event":{"name":"FMSP00: ACM SIGSOFT Workshop on Formal Methods in Software Practice","location":"Portland Oregon USA","acronym":"FMSP00","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the third workshop on Formal methods in software practice"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/349360.351127","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,5]],"date-time":"2023-01-05T20:56:12Z","timestamp":1672952172000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/349360.351127"}},"subtitle":["Two case studies"],"short-title":[],"issued":{"date-parts":[[2000,8,24]]},"references-count":27,"alternative-id":["10.1145\/349360.351127","10.1145\/349360"],"URL":"http:\/\/dx.doi.org\/10.1145\/349360.351127","relation":{},"published":{"date-parts":[[2000,8,24]]},"assertion":[{"value":"2000-08-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}