References

[1] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of the Workshop on Logic of Programs, New York, 1981. 52--71. Google Scholar https://scholar.google.com/scholar?&q=Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of the Workshop on Logic of Programs, New York, 1981. 52--71&

[2] Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the Colloquium on International Symposium on Programming, Turin, 1982. 337--351. Google Scholar https://scholar.google.com/scholar?&q=Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the Colloquium on International Symposium on Programming, Turin, 1982. 337--351&

[3] Clarke E M, Emerson E A, Sifakis J. Model checking: algorithmic verification and debugging. Commun ACM, 2009, 52: 74-84 Google Scholar https://scholar.google.com/scholar?&q=Model checking: algorithmic verification and debugging&author=Clarke E M&author=Emerson E A&author=Sifakis J&publication_year=2009&journal=Commun ACM&volume=52&pages=74-84

[4] Valmari A. A stubborn attack on state explosion. Form Method Syst Des, 1992, 1: 297-322 CrossRef Google Scholar https://scholar.google.com/scholar?&q=A stubborn attack on state explosion&author=Valmari A&publication_year=1992&journal=Form Method Syst Des&volume=1&pages=297-322

[5] Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: $10^{20}$ states and beyond. Inform Comput, 1992, 98: 142-170 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Symbolic model checking: $10^{20}$ states and beyond&author=Burch J R&author=Clarke E M&author=McMillan K L&publication_year=1992&journal=Inform Comput&volume=98&pages=142-170

[6] Biere A, Cimati A, Clarke E M, et al. Bounded model checking. Adv Comput, 2003, 58: 117-148 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Bounded model checking&author=Biere A&author=Cimati A&author=Clarke E M&publication_year=2003&journal=Adv Comput&volume=58&pages=117-148

[7] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Trans Progr Lang Syst, 1992, 16: 1512-1542 Google Scholar https://scholar.google.com/scholar?&q=Model checking and abstraction&author=Clarke E M&author=Grumberg O&author=Long D E&publication_year=1992&journal=ACM Trans Progr Lang Syst&volume=16&pages=1512-1542

[8] Tian C, Duan Z H, Duan Z. Making CEGAR more efficient in software model checking. IEEE Trans Softw Eng, 2014, 40: 1206-1223 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Making CEGAR more efficient in software model checking&author=Tian C&author=Duan Z H&author=Duan Z&publication_year=2014&journal=IEEE Trans Softw Eng&volume=40&pages=1206-1223

[9] Duan Z H, Tian C. A unified model checking approach with projection temporal logic. In: Proceedings of the International Conference on Formal Engineering Methods, Kitakyushu-City, 2008. 167--186. Google Scholar https://scholar.google.com/scholar?&q=Duan Z H, Tian C. A unified model checking approach with projection temporal logic. In: Proceedings of the International Conference on Formal Engineering Methods, Kitakyushu-City, 2008. 167--186&

[10] Duan Z H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005. Google Scholar https://scholar.google.com/scholar?&q=Duan Z H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005&

[11] Godefroid P, Wolper P. A partial approach to model checking. Inform Comput, 1994, 110: 305-326 CrossRef Google Scholar https://scholar.google.com/scholar?&q=A partial approach to model checking&author=Godefroid P&author=Wolper P&publication_year=1994&journal=Inform Comput&volume=110&pages=305-326

[12] Clarke E M, Grumberg O, Jha S, et al. Counter-\linebreak example-guided abstraction refinement for symbolic model checking. J ACM, 2003, 50: 752-794 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Counter-\linebreak example-guided abstraction refinement for symbolic model checking&author=Clarke E M&author=Grumberg O&author=Jha S&publication_year=2003&journal=J ACM&volume=50&pages=752-794

[13] Duan Z H, Tian C, Zhang N. A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor Comput Sci, 2016, 609: 544-560 CrossRef Google Scholar https://scholar.google.com/scholar?&q=A canonical form based decision procedure and model checking approach for propositional projection temporal logic&author=Duan Z H&author=Tian C&author=Zhang N&publication_year=2016&journal=Theor Comput Sci&volume=609&pages=544-560

[14] Duan Z H, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci, 2014, 554: 169-190 CrossRef Google Scholar https://scholar.google.com/scholar?&q=A practical decision procedure for propositional projection temporal logic with infinite models&author=Duan Z H&author=Tian C&publication_year=2014&journal=Theor Comput Sci&volume=554&pages=169-190

[15] Kroening D, Tautschnig M. CBMC --- C bounded model checker. In: Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 389--391. Google Scholar https://scholar.google.com/scholar?&q=Kroening D, Tautschnig M. CBMC --- C bounded model checker. In: Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 389--391&

[16] Henzinger T A, Jhala R, Majumdar R, et al. Software verification with Blast. In: Proceedings of the International SPIN Workshop on Model Checking of Software, Portland, 2003. 235--239. Google Scholar https://scholar.google.com/scholar?&q=Henzinger T A, Jhala R, Majumdar R, et al. Software verification with Blast. In: Proceedings of the International SPIN Workshop on Model Checking of Software, Portland, 2003. 235--239&

[17] Ball T, Bounimova E, Kumar R, et al. SLAM2: static driver verification with under 4\. Google Scholar https://scholar.google.com/scholar?&q=Ball T, Bounimova E, Kumar R, et al. SLAM2: static driver verification with under 4\&

[18] Tian C, Duan Z H. Expressiveness of propositional projection temporal logic with star. Theor Comput Sci, 2011, 412: 1729-1744 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Expressiveness of propositional projection temporal logic with star&author=Tian C&author=Duan Z H&publication_year=2011&journal=Theor Comput Sci&volume=412&pages=1729-1744

[19] Büchi J R. Symposium on decision problems: on a decision method in restricted second order arithmetic. Stud Logic Found Math, 1966, 44: 1-11 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Symposium on decision problems: on a decision method in restricted second order arithmetic&author=Büchi J R&publication_year=1966&journal=Stud Logic Found Math&volume=44&pages=1-11

[20] Gomes C P, Kautz H, Sabharwal A, et al. Satisfiability solvers. Found Artif Intell, 2008, 3: 89-134 Google Scholar https://scholar.google.com/scholar?&q=Satisfiability solvers&author=Gomes C P&author=Kautz H&author=Sabharwal A&publication_year=2008&journal=Found Artif Intell&volume=3&pages=89-134

[21] Duan Z H, Yang X X, Koutny M. Framed temporal logic programming. Sci Comput Program, 2008, 70: 31-61 CrossRef Google Scholar https://scholar.google.com/scholar?&q=Framed temporal logic programming&author=Duan Z H&author=Yang X X&author=Koutny M&publication_year=2008&journal=Sci Comput Program&volume=70&pages=31-61

[22] Wang X B, Duan Z H, Zhao L. Formalizing and implementing types in MSVL. In: Proceedings of the International Workshop of Structured Object-Oriented Formal Language and Method, Queenstown, 2013. 62--75. Google Scholar https://scholar.google.com/scholar?&q=Wang X B, Duan Z H, Zhao L. Formalizing and implementing types in MSVL. In: Proceedings of the International Workshop of Structured Object-Oriented Formal Language and Method, Queenstown, 2013. 62--75&

[23] Zhang N, Duan Z H, Tian C. A mechanism of function calls in MSVL. Theor Comput Sci, in press. doi: 10.1016/j.tcs.2016.02.037. Google Scholar https://scholar.google.com/scholar?&q=Zhang N, Duan Z H, Tian C. A mechanism of function calls in MSVL. Theor Comput Sci, in press. doi: 10.1016/j.tcs.2016.02.037&

[24] Rosner R, Pnueli A. A choppy logic. In: Proceedings of the Symposium on Logic in Computer Science, Cambridge, 1986. 306--313. Google Scholar https://scholar.google.com/scholar?&q=Rosner R, Pnueli A. A choppy logic. In: Proceedings of the Symposium on Logic in Computer Science, Cambridge, 1986. 306--313&

[25] Bowman H, Thompson S J. A decision procedure and complete axiomatization of finite interval temporal logic with projection. J Logic Comput, 2003, 13: 195-239 CrossRef Google Scholar https://scholar.google.com/scholar?&q=A decision procedure and complete axiomatization of finite interval temporal logic with projection&author=Bowman H&author=Thompson S J&publication_year=2003&journal=J Logic Comput&volume=13&pages=195-239

[26] Tang C S. Toward a Unified Logical Basis for Programming Languages. Technology Report, No. STAN-CS-81-865. 1981. Google Scholar https://scholar.google.com/scholar?&q=Tang C S. Toward a Unified Logical Basis for Programming Languages. Technology Report, No. STAN-CS-81-865. 1981&

[27] Moszkowski B C. Executing Temporal Logic Programs. Cambridge: Cambridge University Press, 1986. Google Scholar https://scholar.google.com/scholar?&q=Moszkowski B C. Executing Temporal Logic Programs. Cambridge: Cambridge University Press, 1986&