{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:16:14Z","timestamp":1725495374478},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_15","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T16:56:57Z","timestamp":1194973017000},"page":"208-222","source":"Crossref","is-referenced-by-count":23,"title":["Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol"],"prefix":"10.1007","author":[{"given":"Parosh","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Aurore","family":"Annichini","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"A. P","year":"1998","unstructured":"P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In CAV\u201998. LNCS 1427, 1998."},{"key":"15_CR2","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201992","author":"B. S","year":"1992","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property-preserving simulations. In CAV\u201992. LNCS 663, 1992."},{"key":"15_CR3","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"B. S","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In CAV\u201998. LNCS 1427, 1998."},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"B. B","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. In CAV\u201996. LNCS 1102, 1996."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","volume-title":"SAS\u201997","author":"B. B","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In SAS\u201997. LNCS 1302, 1997."},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201994","author":"B. B","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets. In CAV\u201994. LNCS 818, 1994."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201997","author":"B. A","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. In ICALP\u201997. LNCS 1256, 1997."},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"C. G\u00e9rard","year":"1996","unstructured":"G\u00e9rard C\u00e9c\u00e9, Alain Finkel, and S. Purushothaman Iyer. Unreliable Channels Are Easier to Verify Than Perfect Channels. Inf. and Comp., 124(1):20\u201331, 1996.","journal-title":"Inf. and Comp."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. In IFIP Conf. on Formal Desc. of Prog. Concepts. NH Pub., 1977.","DOI":"10.1145\/800022.808314"},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201997","author":"P. D\u2019Argenio","year":"1997","unstructured":"P. D\u2019Argenio, J-P. Katoen, T. Ruys, and G. J. Tretmans. The Bounded Retrans-mission Protocol must be on Time. In TACAS\u201997. LNCS 1217, 1997."},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In CAV\u201996. LNCS 1102, 1996."},{"key":"15_CR12","unstructured":"A. Finkel and O. Marc\u00e9. Verification of Infinite Regular Communicating Automata. Technical report, LIFAC, ENS de Cachan, 1996."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201997","author":"G. S","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In CAV\u201997, volume 1254 of LNCS, 1997."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","volume-title":"AMAST\u201996","author":"J.-F. Groote","year":"1996","unstructured":"J-F. Groote and J. Van de Pol. A Bounded Retransmission Protocol for Large Data Packets. In AMAST\u201996. LNCS 1101, 1996."},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. Long. Model Checking and Modular Verification. ACM TOPLAS, 16:843\u2013871, 1994.","journal-title":"ACM TOPLAS"},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","volume-title":"FME\u201996","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in Theorem Proving and Model Checking for Protocol Verification. In FME\u201996. LNCS 1051, 1996."},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M. P. A. Sellink, and F. Vaandrager. Proof checking a Data Link Protocol. In Types for Proofs and Programs. LNCS 806, 1994."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"R. M. Karp and R. E. Miller. Parallel Program Schemata: A Mathematical Model for Parallel Computation. In 8th ann. Switch. and Aut. Theo. Symp. IEEE, 1967.","DOI":"10.1109\/FOCS.1967.27"},{"key":"15_CR19","unstructured":"R. Mateescu. Formal Description and Analysis of a Bounded Retransmission Protocol. Technical report no. 2965, INRIA, 1996."},{"key":"15_CR20","unstructured":"J. K. Pachl. Protocol Description and Analysis Based on a State Transition Model with Channel Expressions. In Protocol Specification, Testing, and Verification VII, 1987."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T07:00:29Z","timestamp":1556953229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}