nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Verifying Temporal Properties of C Programs via Lazy Abstraction

verfasst von : Zhao Duan, Cong Tian, Zhenhua Duan

Erschienen in: Formal Methods and Software Engineering

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

To verify both safety and liveness temporal properties of programs in practice, this paper investigates scalable Linear Temporal Logic (LTL) property verification approach of C programs. We show that the verification target can be accomplished as a scalable lazy abstraction supplemented Counter-Example Guided Abstraction Refinement (CEGAR) based program analysis task. As a result, the scalable lazy abstraction based safety property analysis approaches as well as their mature supporting tools can be reused to verify temporal properties of C programs. We have implemented the proposed approach in TPChecker to verify temporal properties of C programs. Experimental results on benchmark programs show that the proposed approach performs well when verifying non-safety temporal properties of C programs.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Improving the Scalability of Automatic Linearizability Checking in SPIN

Nächstes Kapitel Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774 CrossRef

Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.1007/3-540-11494-7_22 CrossRef

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_16 CrossRef

Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4% false alarms. In: FMCAD 2010, pp. 35–42 (2010)

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003). doi:10.1007/3-540-44829-2_17 CrossRef

Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)

Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, pp. 995–1072 (1990)

Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)MathSciNetCrossRefMATH

http://divine.fi.muni.cz/

10.

Koskinen, E.: Temporal verification of programs, Ph.D. thesis, University of Cambridge (2012)

11.

Craig, W.: Linear reasoning. A new form of the Herbrand - Gentzen theorem. Symb. Log. 22(3), 250–268 (1957)MathSciNetCrossRefMATH

12.

Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: POPL 2007, pp. 265–276 (2007)

13.

Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: POPL 2011, pp. 399–410 (2011)

14.

Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef

15.

http://spinroot.com/spin/whatispin.html

16.

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of Symposium on Principles of Programming Languages, pp. 58–70 (2002)

17.

Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). doi:10.1007/3-540-44585-4_6 CrossRef

18.

Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105–128 (2010)CrossRefMATH

19.

Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). doi:10.1007/3-540-63166-6_10 CrossRef

20.

Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Principles of Programming Languages (POPL), pp 232–244. ACM Press, New York (2004)

21.

Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006). doi:10.1007/11691372_33 CrossRef

22.

Terauchi, T., Unno, H.: Relaxed stratification: a new approach to practical complete predicate refinement. In: Proceedings of the 24th European Symposium on Programming (ESOP 2015) (2015)

23.

Cordeiro, L., Fischer, B., Verifying multi-threaded software using SMT-based context-bounded model checking. In Proceedings of the International Conference on Software Engineering (ICSE 2011), pp. 331–340. ACM (2011)

24.

Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733–749 (1985)MathSciNetCrossRefMATH

25.

De Giacomo, G., Vardi, M.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2013, pp. 2000–2007 (2013)

26.

Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49–66. Springer, Cham (2015). doi:10.1007/978-3-319-21690-4_4 CrossRef

27.

Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S.: Bandera: extracting finite-state models from Java source code. In: ICSE 2000, pp. 439–448 (2000)

28.

Cadence SMV. http://www.kenmcmil.com/smv.html

29.

Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 608–614. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_45 CrossRef

30.

Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_22 CrossRef

Titel: Verifying Temporal Properties of C Programs via Lazy Abstraction
verfasst von: Zhao Duan
Cong Tian
Zhenhua Duan
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-68690-5_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner