On Computing Reachability Sets of Process Rewrite Systems

1. Ammirati, P., Delzanno, G., Ganty, P., Geeraerts, G., Raskin, J.-F., Van Begin, L.: Babylon: An integrated toolkit for the specification and verification of parameterized systems. In: SAVE 2002 (2002)

   Google Scholar 

2. Annichini, A., Asarin, E., Bouajjani, A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)

   Chapter  Google Scholar 

3. Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A Tool for Reachability Analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 368. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

4. Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 158. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

5. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

6. Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

7. Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

8. Boigelot, B., Wolper, P.: Symbolic Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)

   Google Scholar 

9. Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)

   Google Scholar 

10. Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proc. of the 30th ACM Symp. on Principles of Programming Languages, POPL 2003 (2003)

    Google Scholar 

11. Bouajjani, A., Esparza, J., Touili, T.: Reachability Analysis of Synchronized PA Systems. In: Proc. Infinity Workshop (2004)

    Google Scholar 

12. Bouajjani, A., Touili, T.: Reachability Analysis of Process Rewrite Systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 74–87. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

13. Bruggemann-Klein, A., Murata, M., Wood, D.: Regular tree and regular hedge languages over unranked alphabets. Research report (2001)

    Google Scholar 

14. Bultan, T., Gerber, R., League, C.: Verifying Systems With Integer Constraints and Boolean Predicates: A Composite Approach. In: Proc. of the Intern. Symp. on Software Testing and Analysis, ACM press, New York (1998)

    Google Scholar 

15. Caucal, D.: On the regular structure of prefix rewriting. Theoret. Comput. Sci. 106, 61–86 (1992)

    Article  MathSciNet  Google Scholar 

16. Colcombet, T.: Rewriting in the partial algebra of typed terms modulo ac. In: Proc. Infinity Workshop. Electronic Notes in Theoretical Computer Science, vol. 68, Elsevier Science Pub., Amsterdam (2002)

    Google Scholar 

17. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, ACM, New York (1978)

    Google Scholar 

18. Delzanno, G., Van Begin, L., Raskin, J.-F.: Attacking symbolic state explosion in parametrized verification. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 298. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

19. Delzanno, G., Van Begin, L., Raskin, J.-F.: Toward the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 173. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

20. Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, Springer, Heidelberg (1995)

    Google Scholar 

21. Esparza, J.: Grammars as processes. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, p. 277. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

22. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithm for model checking pushdown systems. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)

    Google Scholar 

23. Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 14–30. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

24. Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design 16 (2000)

    Google Scholar 

25. Esparza, J., Nielsenl, M.: Decidability issues for Petri nets - a survey. Bulletin of the EATCS 52, 85–107 (1994)

    Google Scholar 

26. Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

27. Esparza, J., Podelski, A.: Efficient algorithms for pre * and post * on interprocedural parallel flow graphs. In: Symposium on Principles of Programming Languages, pp. 1–11 (2000)

    Google Scholar 

28. Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

29. Finkel, A., Willems, B., Wolper, P.: A Direct Symbolic Approach to Model Checking Pushdown Systems. In: Infinity 1997 (1997)

    Google Scholar 

30. Hopcroft, J., Pansiot, J.-J.: On The Reachability Problem for 5-Dimensional Vector Addition Systems. Theoret. Comput. Sci. 8 (1979)

    Google Scholar 

31. The Liège Automata-based Symbolic Handler, LASH (2001), Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/

32. Lugiez, D.: Counting and equality constraints for multitree automata. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 328–342. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

33. Lugiez, D., Schnoebelen, P.: The regular viewpoint on PA-processes. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 50–66. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

34. Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, Techn. Univ. of Munich (1998)

    Google Scholar 

35. Qadeer, S., Rajamani, S.K., Rehof, J.: Procedure Summaries for Model Checking Multithreaded Software. In: POPL 2004, ACM, New York (2004)

    Google Scholar 

36. Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit ät München (2002)

    Google Scholar 

37. Seidl, H., Schwentick, T., Muscholl, A.: Numerical Document Queries. In: PODS 2003, ACM Press, New York (2003)

    Google Scholar 

38. Touili, T.: Analyse symbolique de systèmes infinis basée sur les automates: Application à la vérification de systèmes paramétrés et dynamiques. Phd. thesis, University of Paris 7 (2003)

    Google Scholar 

39. Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references