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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=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
http://scholar.google.com/scholar_lookup?title=Moszkowski B C. Executing Temporal Logic Programs. Cambridge: Cambridge University Press, 1986&