{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:14:55Z","timestamp":1737090895767,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441656"},{"type":"electronic","value":"9783540457398"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45739-9_19","type":"book-chapter","created":{"date-parts":[[2007,5,16]],"date-time":"2007-05-16T02:42:01Z","timestamp":1179283321000},"page":"311-330","source":"Crossref","is-referenced-by-count":8,"title":["Parametric Verification of a Group Membership Algorithm"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agathe","family":"Merceron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,4]]},"reference":[{"key":"19_CR1","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201999","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla P.A, Annichini A., Bensalem S., Bouajjani A., Habermehl P., Lakhnech Y: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. CAV\u201999, Lecture Notes in Computer Science, Vol 1633. Springer-Verlag, (1999)"},{"key":"19_CR2","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"CON-CUR\u201901","author":"P.A. Abdulla","year":"2001","unstructured":"Abdulla P.A, Jonsson B.: Channel Representations in Protocol Verification. CON-CUR\u201901, Lecture Notes in Computer Science, Vol 2154. Springer-Verlag, (2001) 1\u201315"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/S0304-3975(00)00105-5","volume":"256","author":"P.A. Abdulla","year":"2001","unstructured":"Abdulla P.A, Jonsson B.: Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems. Theoretical Computer Science, Vol 256. (2001) 145\u2013167","journal-title":"Theoretical Computer Science"},{"key":"19_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Annichini","year":"2000","unstructured":"Annichini A., Asarin E., Bouajjani A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. CAV\u201900, Lecture Notes in Computer Science, Vol 1855. (2000)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bauer G., Paulitsch M.: An investigation of membership and clique avoidance in TTP\/C. Proceedings 19th IEEE Symposium on Reliable Distributed Systems (SRDS\u201900), IEEE Computer Society, (2000), 118\u2013124","DOI":"10.1109\/RELDI.2000.885399"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Baukus K., Lakhnech Y., Stahl K.: Verifying Universal Properties of Parameterized Networks. Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 2000, Pune, India","DOI":"10.1007\/3-540-45352-0_24"},{"key":"19_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201994","author":"B. Boigelot","year":"1994","unstructured":"Boigelot B., Wolper P.: Symbolic Verification with Periodic Sets. CAV\u201994, Lecture Notes in Computer Science, Vol 818. Springer-Verlag, (1994)"},{"key":"19_CR8","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani A., Esparza J., Maler O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. CONCUR\u201997, Lecture Notes in Computer Science, Vol 1243. Springer-Verlag, (1997)"},{"key":"19_CR9","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201997","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani A., Habermehl P.: Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. ICALP\u201997, Lecture Notes in Computer Science, Vol 1256. Springer-Verlag, (1997) Full version in TCS, Vol 221 (1\/2) (1999) 221\u2013250"},{"key":"19_CR10","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani A., Jonsson B., Nilsson M., Touili T.: Regular Model Checking. CAV\u201900, Lecture Notes in Computer Science, Vol 1855. Springer-Verlag, (2000)"},{"key":"19_CR11","unstructured":"Bouajjani A., Merceron A.: Parametric Verification of a Group Membership Algorithm. Technical Report, Liafa, University of Paris 7, (2002)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Bultan T., Gerber R., League C.: Verifying Systems With Integer Constraints and Boolean Predicates: A Composite Approach. Proc. of the Intern. Symp. on Software Testing and Analysis, ACM Press (1998)","DOI":"10.1145\/271771.271799"},{"key":"19_CR13","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001)","author":"T. Bultan","year":"2001","unstructured":"Bultan T., Yavuz-Kahveci T.: Action Language Verifier. Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), IEEE Computer Society, Coronado Island, California, (2001)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Cousot P., Halbwachs H.: Automatic Discovery of Linear Restraints Among Variables of a Program. POPL\u201978, ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"19_CR15","unstructured":"Creese S., Roscoe A.W.: TTP: a case study in combining induction and data independence. Oxford University Programming Research Group, Technical Report TR-1-99, (1999)"},{"key":"19_CR16","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201997","author":"S. Graf","year":"1997","unstructured":"Graf S., Saidi H.: Construction of abstract state graphs with pvs. CAV\u201997, Lecture Notes in Computer Science, Vol 1254. Springer-Verlag, (1997)"},{"key":"19_CR17","series-title":"Lect Notes Comput Sci","volume-title":"WDAG\u201997","author":"S. Katz","year":"1997","unstructured":"Katz S., Lincoln P., Rushby J.: Low-overhead Time-Triggered Group Membership. WDAG\u201997, Lecture Notes in Computer Science, Vol 1320. Springer-Verlag, (1997)"},{"key":"19_CR18","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201997","author":"Y. Kesten","year":"1997","unstructured":"Kesten Y., Maler O., Marcus M., Pnueli A., Shahar E.: Symbolic Model Checking with Rich Assertional Languages. CAV\u201997, Lecture Notes in Computer Science, Vol 1254. Springer-Verlag, (1997)"},{"key":"19_CR19","unstructured":"Kopetz H.: TTP\/C Protocol-Specification of the TTP\/C Protocol. http:\/\/www.tttech.com (1999)"},{"key":"19_CR20","unstructured":"Kopetz H., Gr\u00fcnsteidl G.: A time triggered protocol for fault-tolerant Real-Time Systems. IEEE Computer, (1999) 14\u201323"},{"key":"19_CR21","unstructured":"LASH: The Li\u00e9ge Automata-based Symbolic Handler (LASH). http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Pfeifer H.: Formal verification of the TTP Group Membership Algorithm. IFIP TC6\/WG6.1 International Conference on Formal Description Techniques for Distributed Systems and Communication protocols and Protocol Specification, Testing and Verification, FORTE\/PSTV 2000, Pisa, Italy (2000)","DOI":"10.1007\/978-0-387-35533-7_1"},{"key":"19_CR23","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201999","author":"H. Saidi","year":"1999","unstructured":"Saidi H., Shankar N.: Abstract and Model Check while you Prove. CAV\u201999, Lecture Notes in Computer Science, Vol 1633. Springer-Verlag, (1999)"},{"key":"19_CR24","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"W. Wolper","year":"1998","unstructured":"Wolper W., Boigelot B.: Verifying systems with infinite but regular state spaces. CAV\u201998, Lecture Notes in Computer Science, Vol 1427. Springer-Verlag, (1998)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45739-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T09:17:22Z","timestamp":1737019042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45739-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441656","9783540457398"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45739-9_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}