tailieunhanh - CONCUR 2004 – Concurrency Theory- P3

CONCUR 2004 – Concurrency Theory- P3: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 46 . Abdulla et al. Context Free Languages. Fismanand Pnueli FP01 use representations of context-free languages to verify parameterized algorithms whose symbolic verification require computation of invariants that are non-regular sets of finite words. The motivating example is the Peterson algorithm for mutual exclusion among n processes PS81 . References ABJ98 AJMd02 AJN 04 AJNd02 AJNd03 BCMD92 BEM97 BG96 BGWW97 BH97 BHV04 Parosh Aziz Abdulla Ahmed Bouajjani and Bengt Jonsson. On-the-fly analysis of systems with unbounded lossy fifo channels. In Proc. 10t l Int. Conf on Computer Aided Verification volume 1427 of Lecture Notes in Computer Science pages 305-318 1998. Parosh Aziz Abdulla Bengt Jonsson Pritha Mahata and Julien d Orso. Regular tree model checking. In Proc. 14ifc Int. Conf. on Computer Aided Verification volume 2404 of Lecture Notes in Computer Science 2002. . Abdulla B. Jonsson Marcus Nilsson Julien d Orso and M. Saksena. Regular model checking for MSO LTL. In Proc. 16th Int. Conf. on Computer Aided Verification 2004. to appear. Parosh Aziz Abdulla Bengt Jonsson Marcus Nilsson and Julien d Orso. Regular model checking made simple and efficient. In Proc. CONCUR 2002 13th Int. Conf. on Concurrency Theory volume 2421 of Lecture Notes in Computer Science pages 116-130 2002. Parosh Aziz Abdulla Bengt Jonsson Marcus Nilsson and Julien d Orso. Algorithmic improvements in regular model checking. In Proc. 15th Int. Conf. on Computer Aided Verification volume 2725 of Lecture Notes in Computer Science pages 236-248 2003. . Burch . Clarke . McMillan and . Dill. Symbolic model checking IO20 states and beyond. Information and Computation 98 142170 1992. A. Bouajjani J. Esparza and O. Maler. Reachability Analysis of Pushdown Automata Application to Model Checking. In Proc. Intern. Conf. on Concurrency Theory CONCUR 97 . LNCS 1243 1997. B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using .