{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:37:36Z","timestamp":1729629456153,"version":"3.28.0"},"reference-count":26,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1109\/memcod.2003.1210095","type":"proceedings-article","created":{"date-parts":[[2004,1,24]],"date-time":"2004-01-24T04:33:03Z","timestamp":1074918783000},"page":"103-112","source":"Crossref","is-referenced-by-count":0,"title":["How to compute the refinement relation for parameterized systems"],"prefix":"10.1109","author":[{"given":"F.","family":"Bellegarde","sequence":"first","affiliation":[]},{"given":"C.","family":"Charlet","sequence":"additional","affiliation":[]},{"given":"O.","family":"Kouchnarenko","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","article-title":"Using acceleration to compute parameterized system refinement","author":"bellegarde","year":"2003","journal-title":"Technical Report"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46428-X_19"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_43"},{"key":"ref13","first-page":"403","article-title":"Regular model checking","author":"bouajjani","year":"2000","journal-title":"Proc Int Conf on Computer Aided Verification CAV'00 volume 1855 of Lecture Notes in Computer Science"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/PL00003930"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","article-title":"Verifying parameterized networks using abstraction and regular languages","author":"clarke","year":"1995","journal-title":"Proc 6th International Conference on Concurrency Theory (CONCUR '95)"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028751"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024651"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/10721959_19","article-title":"Reducing model checking of the many to the few","volume":"14","author":"emerson","year":"2000","journal-title":"17th International Conference on Automated Deduction (CADE)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199468"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_14"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_9"},{"key":"ref6","first-page":"419","article-title":"Symbolic techniques for parametric reasoning","author":"annichini","year":"2000","journal-title":"Proc Int Conf on Computer Aided Verification CAV'00 volume 1855 of Lecture Notes in Computer Science"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"ref8","first-page":"221","article-title":"Parameterized verification with automatically computed inductive assertions","author":"arons","year":"2001","journal-title":"Proc Int Conf CAV'01 volume 2102 of Lecture Notes in Computer Science"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"journal-title":"Regular Model Checking (RMC)","year":"0","key":"ref2"},{"key":"ref9","first-page":"1121","article-title":"Raffiner pour vérifier des systèmes parametres","volume":"8","author":"bellegarde","year":"2002","journal-title":"Technique et Science Informatiques"},{"journal-title":"The Liège Automata-based Symbolic Handler (LASH)","year":"0","key":"ref1"},{"key":"ref20","article-title":"Automatic verification of parameterized synchronous systems","author":"emerson","year":"1996","journal-title":"Proc Int Conf CAV'98 volume 1102 of LNCS"},{"key":"ref22","first-page":"424","article-title":"Symbolic model checking with rich assertional languages","author":"kesten","year":"1997","journal-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV 1997)"},{"key":"ref21","first-page":"220","article-title":"Transitive closures of regular relations for verifying infinite-state systems","author":"jonsson","year":"2000","journal-title":"Proc 6th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2000)"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_29"},{"key":"ref23","first-page":"183","article-title":"Specifying concurrent systems with tla +","author":"lamport","year":"1999","journal-title":"Calculational System Design"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050040"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_26"}],"event":{"name":"2003 1st IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2003)","start":{"date-parts":[[2003,6,24]]},"location":"Mont Saint Michel, France","end":{"date-parts":[[2003,6,26]]}},"container-title":["First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8593\/27232\/01210095.pdf?arnumber=1210095","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T07:51:49Z","timestamp":1585468309000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210095\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/memcod.2003.1210095","relation":{},"subject":[],"published":{"date-parts":[[2003]]}}}