Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter

1. R. Alur and D. Dill, “The theory of timed automata,” TCS, 126(2):183–236, 1994

   Article  MATH  MathSciNet  Google Scholar 

2. P. Abdulla and B. Jonsson, “Verifying programs with unreliable channels,” Information and Computation, 127(2): 91–101, 1996

   Article  MATH  MathSciNet  Google Scholar 

3. A. Bouajjani, J. Esparza, and O. Maler. “Reachability analysis of pushdown automata: application to model-Checking,” CONCUR’97, LNCS 1243, pp. 135–150

   Google Scholar 

4. G. Cece and A. Finkel, “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315

   Google Scholar 

5. H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279

   Google Scholar 

6. H. Comon and Y. Jurski, “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257

   Google Scholar 

7. Z. Dang, “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517

   Google Scholar 

8. Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su, “Binary Reachability Analysis of Discrete Pushdown Timed Automata,” CAV’00, LNCS 1855, pp. 69–84

   Google Scholar 

9. Z. Dang, O. H. Ibarra and R. A. Kemmerer, “Decidable Approximations on Generalized and Parameterized Discrete Timed Automata,” COCOON’01, LNCS 2108, pp. 529–539

   Google Scholar 

10. Z. Dang and R. A. Kemmerer, “Using the ASTRAL model checker to analyze Mobile IP,” Proceedings of the Twenty-first International Conference on Software Engineering (ICSE’99), pp. 132–141, IEEE Press, 1999

    Google Scholar 

11. Z. Dang and R. A. Kemmerer, “Three approximation techniques forASTRALsymbolic model checking of infinite state real-time systems,” Proceedings of the Twenty-second International Conference on Software Engineering (ICSE’00), pp. 345–354, IEEE Press, 2000

    Google Scholar 

12. Z. Dang, P. San Pietro, and R. A. Kemmerer, “On Presburger Liveness of Discrete Timed Automata,” STACS’01, LNCS 2010, pp. 132–143

    Google Scholar 

13. A. Finkel and G. Sutre. “Decidability of Reachability Problems for Classes of Two Counter Automata,” STACS’00, LNCS 1770, pp. 346–357

    Google Scholar 

14. A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97

    Google Scholar 

15. O. H. Ibarra, “Reversal-bounded multicounter machines and their decision problems,” J.ACM, 25 (1978) 116–133

    Article  MATH  MathSciNet  Google Scholar 

16. O. H. Ibarra, “Reachability and safety in queue systems with counters and pushdown stack,” Proceedings of the International Conference on Implementation and Application of Automata, pp. 120–129, 2000

    Google Scholar 

17. O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001

    Google Scholar 

18. O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer, “Counter Machines: Decidable Properties and Applications to Verification Problems,”, MFCS’00, LNCS 1893, pp. 426–435

    Google Scholar 

19. G. Kreisel and J. L. Krevine, “Elements of Mathematical Logic,” North-Holland, 1967

    Google Scholar 

20. K. L. McMillan. “Symbolic model-checking-an approach to the state explosion problem,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992

    Google Scholar 

21. W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,” Acta Informatica, 29(6/7): 499–522, 1992

    Article  MATH  MathSciNet  Google Scholar 

22. W. Pugh, “TheOmega test: a fast and practical integer programming algorithm for dependence analysis,” Communications of the ACM, 35(8): 102–114, 1992

    Article  Google Scholar 

Download references