Skip to main content
Springer Nature Link
Log in

Efficient Runtime Assertion Checking for Properties over Mathematical Numbers

  • Conference paper
  • First Online:
Runtime Verification (RV 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12399))

Included in the following conference series:

Abstract

Runtime assertion checking is the discipline of detecting at runtime violations of program properties written as formal code annotations. These properties often include numerical properties, which may rely on either (bounded) machine representations or (unbounded) mathematical numbers. The verification of the former is easier to implement and more efficient at runtime, while the latter are more expressive and often more adequate for writing specifications. This short paper explains how the runtime assertion checker E-ACSL reconciles both approaches by presenting a type system that allows the tool to generate efficient machine-number based code when it is safe to do so, while generating arbitrary-precision code when it is necessary. This type system and the code generator not only handle integers but also rational arithmetics. As far as we know, it is the first runtime verification tool that supports the verification of properties over rational numbers.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
Price includes VAT (France)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    https://blog.regehr.org/archives/1091.

  2. 2.

    See e.g. http://www-users.math.umn.edu/~arnold/disasters/patriot.html.

  3. 3.

    See e.g. https://en.wikipedia.org/wiki/Vancouver_Stock_Exchange.

  4. 4.

    https://gmplib.org/.

  5. 5.

    E-ACSL also supports floating-point constants such as 0.1f but they are excluded here for the sake of simplicity.

References

  1. Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006)

    Article  Google Scholar 

  2. Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with frama-C. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 386–399. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_29

    Chapter  Google Scholar 

  3. Chalin, P.: JML support for primitive arbitrary precision numeric types: definition and semantics. J. Object Technol. 3(6), 57–79 (2004)

    Article  Google Scholar 

  4. Chalin, P.: Improving JML: for a safer and more effective language. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 440–461. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_25

    Chapter  Google Scholar 

  5. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Symposium on Applied Computing (SAC), March 2013

    Google Scholar 

  6. Meyer, B.: Eiffel: The Language. Prentice-Hall, Upper Saddle River (1992)

    MATH  Google Scholar 

  7. Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3

    Chapter  Google Scholar 

  8. Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 175–188. Springer, Boston (1999). https://doi.org/10.1007/978-1-4615-5229-1_12

    Chapter  Google Scholar 

  9. Dross, C., Filliâtre, J.-C., Moy, Y.: Correct code containing containers. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 102–118. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21768-5_9

    Chapter  Google Scholar 

  10. Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C specification language. http://frama-c.com/acsl.html

  11. Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  12. Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32

    Chapter  Google Scholar 

  13. Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a runtime verification tool for safety and security of C programs. Tool paper. In: International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES), September 2017

    Google Scholar 

  14. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27, 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  15. Signoles, J.: E-ACSL: executable ANSI/ISO C specification language. http://frama-c.com/download/e-acsl/e-acsl.pdf

  16. Signoles, J.: From static analysis to runtime verification with Frama-C and E-ACSL, Habilitation thesis, July 2018

    Google Scholar 

  17. Jakobsson, A., Kosmatov, N., Signoles, J.: Rester statique pour devenir plus rapide, plus précis et plus mince. In: Journées Francophones des Langages Applicatifs (JFLA), January 2015. (In French)

    Google Scholar 

  18. ISO: ISO C Standard 1999. Technical report (1999)

    Google Scholar 

  19. Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  20. Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: International Symposium on Memory Management (ISMM), June 2017

    Google Scholar 

  21. Pariente, D., Signoles, J.: Static analysis and runtime assertion checking: contribution to security counter-measures. In: Symposium sur la Sécurité des Technologies de l’Information et des Communications (SSTIC), June 2017

    Google Scholar 

  22. Muller, J., et al.: Handbook of Floating-Point Arithmetic. Birkhäuser, Boston (2010)

    Book  Google Scholar 

  23. Richardson, D., Fitch, J.P.: The identity problem for elementary functions and constants. In: International Symposium on Symbolic and Algebraic Computation (ISSAC), July 1994

    Google Scholar 

Download references

Acknowledgment

The authors thank Thales Research & Technology for support of this work, the Frama-C team for providing the tool, as well as the anonymous reviewers for their helpful comments.

Author information

Authors and Affiliations

  1. CEA, LIST, Software Safety and Security Laboratory, Palaiseau, France

    Nikolai Kosmatov, Fonenantsoa Maurica & Julien Signoles

  2. Thales Research & Technology, Palaiseau, France

    Nikolai Kosmatov

  3. Billee, Neuilly-sur-Seine, France

    Fonenantsoa Maurica

Authors
  1. Nikolai Kosmatov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fonenantsoa Maurica
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julien Signoles
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikolai Kosmatov .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Jyotirmoy Deshmukh

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

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

Kosmatov, N., Maurica, F., Signoles, J. (2020). Efficient Runtime Assertion Checking for Properties over Mathematical Numbers. In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-60508-7_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-60507-0

  • Online ISBN: 978-3-030-60508-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation