SCIENCE CHINA Information Sciences, Volume 59, Issue 11: 118101(2016) https://doi.org/10.1007/s11432-015-0882-6

Model checking concurrent systems with MSVL

• ReceivedMar 3, 2016
• AcceptedApr 22, 2016
• PublishedOct 10, 2016
Share
Rating

Funded by

National Natural Science Foundation of China(61133001)

National Natural Science Foundation of China(61420106004)

National Natural Science Foundation of China(91418201)

Acknowledgment

Acknowledgments

This work was supported by National Natural Science Foundation of China (Grant Nos. 61133001, 61420106004, 91418201).

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

[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

[3] Clarke E M, Emerson E A, Sifakis J. Model checking: algorithmic verification and debugging. Commun ACM, 2009, 52: 74-84 Google Scholar

[4] Valmari A. A stubborn attack on state explosion. Form Method Syst Des, 1992, 1: 297-322 CrossRef Google Scholar

[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

[6] Biere A, Cimati A, Clarke E M, et al. Bounded model checking. Adv Comput, 2003, 58: 117-148 CrossRef Google Scholar

[7] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Trans Progr Lang Syst, 1992, 16: 1512-1542 Google Scholar

[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

[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

[10] Duan Z H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005. Google Scholar

[11] Godefroid P, Wolper P. A partial approach to model checking. Inform Comput, 1994, 110: 305-326 CrossRef Google Scholar

[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

[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

[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

[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

[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

[17] Ball T, Bounimova E, Kumar R, et al. SLAM2: static driver verification with under 4\. Google Scholar

[18] Tian C, Duan Z H. Expressiveness of propositional projection temporal logic with star. Theor Comput Sci, 2011, 412: 1729-1744 CrossRef Google Scholar

[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

[20] Gomes C P, Kautz H, Sabharwal A, et al. Satisfiability solvers. Found Artif Intell, 2008, 3: 89-134 Google Scholar

[21] Duan Z H, Yang X X, Koutny M. Framed temporal logic programming. Sci Comput Program, 2008, 70: 31-61 CrossRef Google Scholar

[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

[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

[24] Rosner R, Pnueli A. A choppy logic. In: Proceedings of the Symposium on Logic in Computer Science, Cambridge, 1986. 306--313. Google Scholar

[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

[26] Tang C S. Toward a Unified Logical Basis for Programming Languages. Technology Report, No. STAN-CS-81-865. 1981. Google Scholar

[27] Moszkowski B C. Executing Temporal Logic Programs. Cambridge: Cambridge University Press, 1986. Google Scholar

• 11

Citations

• Altmetric

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.6430259943008423, "perplexity": 28452.67641505222}, "config": {"markdown_headings": false, "markdown_code": false, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2020-10/segments/1581875143079.30/warc/CC-MAIN-20200217175826-20200217205826-00019.warc.gz"}