Advertisement

A Broader View on Verification: From Static to Runtime and Back (Track Summary)

  • Wolfgang Ahrendt
  • Marieke HuismanEmail author
  • Giles Reger
  • Kristin Yvonne Rozier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

When seeking to verify a computational system one can either view the system as a static description of possible behaviours or a dynamic collection of observed or actual behaviours. Historically, there have been clear differences between the two approaches in terms of their level of completeness, the associated costs, the kinds of specifications considered, how and when they are applied, and so on. Recently there has been a concentrated interest in the combination of static and runtime (dynamic) techniques and this track (taking place as part of ISoLA 2018) aims to explore this combination further.

References

  1. 1.
    Aceto, L., Francalanza, A., Ingolfsdottir, A.: Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques. ArXiv e-prints, May 2016Google Scholar
  2. 2.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification-The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6Google Scholar
  3. 3.
    Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Form. Methods Syst. Des. 51(1), 200–265 (2017).  https://doi.org/10.1007/s10703-017-0274-yCrossRefzbMATHGoogle Scholar
  4. 4.
    Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS — episode II - strengthen and distribute the force. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 402–415. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_28CrossRefGoogle Scholar
  5. 5.
    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-75632-5_1CrossRefGoogle Scholar
  6. 6.
    Beckert, B., Herda, M., Kobischke, S., Ulbrich, M.: Towards a notion of coverage for incomplete program-correctness proofs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 53–63. Springer, Cham (2018)Google Scholar
  7. 7.
    Bodden, E., Lam, P., Hendren, L.J.: Partially evaluating finite-state runtime monitors ahead of time. ACM Trans. Program. Lang. Syst. 34(2), 7:1–7:52 (2012).  https://doi.org/10.1145/2220365.2220366CrossRefGoogle Scholar
  8. 8.
    Bonakdarpour, B., Sánchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 8–27. Springer, Cham (2018)CrossRefGoogle Scholar
  9. 9.
    Boockmann, J.H., Lüttgen, G., Mühlberg, J.T.: Generating inductive shape predicates for runtime checking and formal verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 64–74. Springer, Cham (2018)CrossRefGoogle Scholar
  10. 10.
    Chen, X., Rosu, G.: A language-independent program verification framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 92–102. Springer, Cham (2018)CrossRefGoogle Scholar
  11. 11.
    Cheon, Y., Leavens, G.T.: A Runtime Assertion Checker for the Java Modeling Language (JML) (2002)Google Scholar
  12. 12.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.P.: Handbook of Model Checking. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-10575-8zbMATHGoogle Scholar
  13. 13.
    Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006)CrossRefGoogle Scholar
  14. 14.
    Desai, A., Seshia, S., Qadeer, S.: Programming safe robotics systems: challenges, advances, and opportunities. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 103–119. Springer, Cham (2018)Google Scholar
  15. 15.
    Filliâtre, J.C.: Deductive software verification. Int. J. Softw. Tools Technol. Transf. 13(5), 397 (2011).  https://doi.org/10.1007/s10009-011-0211-0CrossRefGoogle Scholar
  16. 16.
    Fisman, D., Kugler, H.: Temporal reasoning on incomplete paths. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 28–52. Springer, Cham (2018)CrossRefGoogle Scholar
  17. 17.
    Francalanza, A., Pace, G.J.: Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques. ArXiv e-prints, August 2017Google Scholar
  18. 18.
    Gurov, D., Havelund, K., Huisman, M., Monahan, R.: Static and runtime verification, competitors or friends? (Track Summary). In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 397–401. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_27CrossRefGoogle Scholar
  19. 19.
    Howar, F., Giannakopoulou, D., Mues, M., Navas, J.: Generating component interfaces by integrating static and symbolic analysis, learning, and runtime monitoring. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 120–136. Springer, Cham (2018)CrossRefGoogle Scholar
  20. 20.
    Maurica, F., Cok, D., Signoles, J.: Runtime assertion checking and static verification: collaborative partners. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 75–91. Springer, Cham (2018)CrossRefGoogle Scholar
  21. 21.
    Rupprecht, T., Chen, X., White, D.H., Boockmann, J.H., Lüttgen, G., Bos, H.: DSIbin: identifying dynamic data structures in C/C++ binaries. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, 30 October–3 November 2017, pp. 331–341. IEEE Computer Society (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Wolfgang Ahrendt
    • 1
  • Marieke Huisman
    • 2
    Email author
  • Giles Reger
    • 3
  • Kristin Yvonne Rozier
    • 4
  1. 1.Chalmers University of TechnologyGothenburgSweden
  2. 2.University of TwenteEnschedeThe Netherlands
  3. 3.University of ManchesterManchesterUK
  4. 4.Iowa State UniversityAmesUSA

Personalised recommendations