Skip to main content
SpringerLink
Log in

The Trace Modality

  • Conference paper
  • First Online:
Dynamic Logic. New Trends and Applications (DALI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12005))

Included in the following conference series:

Abstract

We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its usefulness, we formalize several program verification problems in it: Functional Verification, Information Flow Analysis, Temporal Model Checking, Program Synthesis, Correct Compilation, and Program Evolution. To reason about the trace modality, we translate programs and specifications to regular symbolic traces and construct simulation relations on first-order symbolic automata. The idea with this uniform representation is that it helps to identify synergy potential—theoretically and practically—between so far separate verification approaches.

This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Ahrendt, W., Beckert, B., et al. (eds.): Deductive Software Verification - The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6

    Book  Google Scholar 

  2. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17

    Chapter  Google Scholar 

  3. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_17

    Chapter  Google Scholar 

  4. Barthe, G., D’Argenio, P.R., et al.: Secure information flow by self-composition. In: Proceedings of CSFW-17, pp. 100–114. IEEE Computer Society (2004)

    Google Scholar 

  5. Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 315–329. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_22

    Chapter  Google Scholar 

  6. Bobot, F., Filliâtre, J.C., et al.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on IVL, pp. 53–64 (2011)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Symposium of POPL, pp. 238–252. ACM Press, January 1977

    Google Scholar 

  8. Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32004-3_20

    Chapter  Google Scholar 

  9. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of 23rd IJCAI, pp. 854–860 (2013)

    Google Scholar 

  10. Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55179-4_25

    Chapter  Google Scholar 

  11. Din, C.C., Hähnle, R., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Locally abstract, globally concrete semantics of concurrent programming languages. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 22–43. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66902-1_2

    Chapter  Google Scholar 

  12. Garrido, A., Meseguer, J.: Formal specification and verification of Java refactorings. In: Proceedings of 6th SCAM, pp. 165–174. IEEE Computer Society (2006)

    Google Scholar 

  13. Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241–258 (2013)

    Article  Google Scholar 

  14. Hähnle, R., Heisel, M., Reif, W., Stephan, W.: An interactive verification system based on dynamic logic. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 306–315. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16780-3_99

    Chapter  Google Scholar 

  15. Harel, D., Tiuryn, J., et al.: Dynamic Logic. MIT Press, Cambridge (2000)

    Book  Google Scholar 

  16. Heisel, M.: Formalizing and implementing Gries’ program development method in dynamic logic. Sci. Comput. Program. 18(1), 107–137 (1992)

    Article  MathSciNet  Google Scholar 

  17. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  18. Holzmann, G.J.: The model checker SPIN. IEEE Trans. SE 23(5), 279–295 (1997)

    Article  Google Scholar 

  19. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)

    Article  Google Scholar 

  20. Kamburjan, E.: Behavioral program logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 391–408. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29026-9_22

    Chapter  Google Scholar 

  21. Leroy, X.: Formal verification of a realistic compiler. Comm. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  22. Monperrus, M.: Automatic software repair: a bibliography. ACM Comput. Surv. 51(1), 17:1–17:24 (2018)

    Article  Google Scholar 

  23. Păsăreanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 164–181. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24732-6_13

    Chapter  Google Scholar 

  24. Rauch Henzinger, M., Henzinger, T.A., et al.: Computing simulations on finite and infinite graphs. In: Proceedings of 36th Symposium on FoCS, pp. 453–462. IEEE (1995)

    Google Scholar 

  25. Reps, T.W., Horwitz, S., et al.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of 22nd POPL, pp. 49–61 (1995)

    Google Scholar 

  26. Shankar, N.: Combining model checking and deduction. Handbook of Model Checking, pp. 651–684. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_20

    Chapter  MATH  Google Scholar 

  27. Srivastava, S., Gulwani, S., et al.: From program verification to program synthesis. In: Proceedings of 37th POPL, pp. 313–326 (2010)

    Google Scholar 

  28. Steinhöfel, D., Hähnle, R.: Modular, correct compilation with automatic soundness proofs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 424–447. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03418-4_25

    Chapter  Google Scholar 

  29. Visser, W., Havelund, K., et al.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

    Article  Google Scholar 

  30. Yang, H.: Relational separation logic. Theoret. CS 375(1–3), 308–334 (2007)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, TU Darmstadt, Darmstadt, Germany

    Dominic Steinhöfel & Reiner Hähnle

Authors
  1. Dominic Steinhöfel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dominic Steinhöfel .

Editor information

Editors and Affiliations

  1. University of Minho, Braga, Portugal

    Luís Soares Barbosa

  2. Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, Noord-Holland, The Netherlands

    Alexandru Baltag

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Steinhöfel, D., Hähnle, R. (2020). The Trace Modality. In: Soares Barbosa, L., Baltag, A. (eds) Dynamic Logic. New Trends and Applications. DALI 2019. Lecture Notes in Computer Science(), vol 12005. Springer, Cham. https://doi.org/10.1007/978-3-030-38808-9_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-38808-9_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-38807-2

  • Online ISBN: 978-3-030-38808-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation