TY - GEN
T1 - Runtime assertion checking and its combinations with static and dynamic analyses tutorial synopsis
AU - Kosmatov, Nikolai
AU - Signoles, Julien
PY - 2014/1/1
Y1 - 2014/1/1
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-09099-3_13
DO - 10.1007/978-3-319-09099-3_13
M3 - Conference contribution
AN - SCOPUS:84904968188
SN - 9783319090986
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 165
EP - 168
BT - Tests and Proofs - 8th International Conference, TAP 2014, Held as Part of STAF 2014, Proceedings
PB - Springer Verlag
T2 - 8th International Conference on Tests and Proofs, TAP 2014, Held as Part of the Software Technologies: Applications and Foundations, STAF 2014
Y2 - 24 July 2014 through 25 July 2014
ER -