Abstract
Among various static and dynamic software verification techniques, runtime assertion checking traditionally holds a particular place. Commonly used by most software developers, it can provide a fast feedback on the correctness of a property for one or several concrete executions of the program. Quite easy to realize for simple program properties, it becomes however much more complex for complete program contracts written in an expressive specification language. This paper presents a one-hour tutorial on runtime assertion checking in which we give an overview of this popular dynamic verification technique, present its various combinations with other verification techniques (such as static analysis, deductive verification, test generation, etc.) and emphasize the benefits and difficulties of these combinations. They are illustrated on concrete examples of C programs within the Frama-C software analysis framework using the executable specification language E-ACSL.
This work was partially funded by EU FP7 (project STANCE, grant 317753).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes 31(3), 25–37 (2006)
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C, a program analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)
Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language (2013), http://frama-c.com/download/e-acsl/e-acsl.pdf
Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: The 28th Annual ACM Symposium on Applied Computing (SAC 2013), pp. 1230–1235. ACM (2013)
Williams, N., Marre, B., Mouy, P.: On-the-fly generation of k-paths tests for C functions: towards the automation of grey-box testing. In: The International Conference on Automated Software Engineering (ASE 2004), pp. 290–293. IEEE Computer Society (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Kosmatov, N., Signoles, J. (2014). Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses. In: Seidl, M., Tillmann, N. (eds) Tests and Proofs. TAP 2014. Lecture Notes in Computer Science, vol 8570. Springer, Cham. https://doi.org/10.1007/978-3-319-09099-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-09099-3_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09098-6
Online ISBN: 978-3-319-09099-3
eBook Packages: Computer ScienceComputer Science (R0)