Regular model checking

被引:19
作者
Abdulla, Parosh Aziz [1 ]
机构
[1] Department of Information Technology, Uppsala University, Uppsala, Sweden
关键词
Program verification; Model checking; Regular languages;
D O I
10.1007/s10009-011-0216-8
中图分类号
学科分类号
摘要
Regular model checking has been studied extensively during recent years as a framework for algorithmic verification of systems with infinite state spaces. We describe the main concepts of the framework, and some of its applications. © 2011 Springer-Verlag.
引用
收藏
页码:109 / 118
页数:9
相关论文
共 23 条
[1]  
Abdulla P.A.(2010)Well (and better) quasi-ordered transition systems Bull. Symb. Log. 16 457-515
[2]  
Burch J.R.(1992)Symbolic model checking: 10 Inf. Comput. 98 142-170
[3]  
Clarke E.M.(1992)0 states and beyond Theor. Comput. Sci. 106 61-86
[4]  
McMillan K.L.(2001)On the regular structure of prefix rewriting Form. Methods Syst. Des. 19 7-34
[5]  
Dill D.L.(1999)Bounded model checking using satisfiability solving STTT 2 208-218
[6]  
Hwang L.J.(2009)Pragmatics of model checking: an sttt special section Log. Methods Comput. Sci. 5 1-20
[7]  
Caucal D.(2001)Antichains for the automata-based approach to model-checking Theor. Comput. Sci. 256 93-112
[8]  
Clarke E.M.(2002)Symbolic model checking with rich assertional languages Int. J. Found. Comput. Sci. 13 571-586
[9]  
Biere A.(2001)Mona implementation secrets Electr. Notes Theor. Comput. Sci. 50 342-356
[10]  
Raimi R.(undefined)Regular model checking using widening techniques undefined undefined undefined-undefined