publication . Part of book or chapter of book . Conference object . Other literature type . Book . 2004

Abstract Regular Model Checking

Bouajjani, A.; Habermehl, P.; Tomas Vojnar;
Open Access
  • Published: 01 Jan 2004
  • Publisher: Springer Berlin Heidelberg
  • Country: France
International audience; We propose abstract regular model checking as a new generic technique for verification of parametric and infinite-state systems. The technique combines the two approaches of regular model checking and verification by abstraction. We propose a general framework of the method as well as several concrete ways of abstracting automata or transducers, which we use for modelling systems and encoding sets of their states as usual in regular model checking. The abstraction is based on collapsing states of automata (or transducers) and its precision is being incrementally adjusted by analysing spurious counterexamples. We illustrate the technique o...
free text keywords: Computer science, Encoding (memory), Model checking, Abstract interpretation, Automaton, Data structure, Predicate abstraction, Algorithm, Abstraction model checking, Theoretical computer science, Parametric statistics, Infinite-state model checking, regular model checking, verification by abstraction, counterexample-guided abstraction refinement, [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF]
30 references, page 1 of 2

1. P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In Proc. of TACAS, volume 1579 of LNCS. Springer, 1999.

2. P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc. of CAV'98, volume 1427 of LNCS. Springer, 1998.

3. P.A. Abdulla, J. d'Orso, B. Jonsson, and M. Nilsson. Algorithmic improvements in regular model checking. In Proc. of CAV'03, volume 2725 of LNCS. Springer, 2003.

4. B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Proc. of CAV'96, volume 1102 of LNCS. Springer, 1996. [OpenAIRE]

5. B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. of CAV'94, volume 818 of LNCS, pages 55-67. Springer, 1994. [OpenAIRE]

6. T. Ball and S. K. Rajamani. The SLAM toolkit. In Proc. CAV'01, LNCS. Springer, 2001.

7. K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S systems to verify parameterized networks. In Proc. of TACAS, volume 1785 of LNCS. Springer, 2000. [OpenAIRE]

8. S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. of CAV'98, LNCS. Springer, 1998.

9. B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large. In Proc. CAV'03, volume 2725 of LNCS. Springer, 2003. [OpenAIRE]

10. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. of CONCUR'97, LNCS. Springer, 1997.

11. A. Bouajjani and P. Habermehl. Symbolic Reachability Analysis of Fifo-Channel Systems with Nonregular Sets of Configurations. Theoretical Computer Science, 221(1-2), 1999. [OpenAIRE]

12. A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Proc. of CAV'00, volume 1855 of LNCS. Springer, 2000.

13. S. Chaki, E. Clarke, A. Groce, J. Ouaknine, O. Strichman, and K. Yorav. Efficient verification of sequential and concurrent c programs. Formal Methods in System Design, 2004. To appear.

14. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. CAV'00, volume 1855 of LNCS. Springer, 2000.

15. D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. In Proc. CAV'01, volume 2102 of LNCS. Springer, 2001.

30 references, page 1 of 2
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue