Runtime assertion checking and its combinations with static and dynamic analyses tutorial synopsis - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Runtime assertion checking and its combinations with static and dynamic analyses tutorial synopsis

Résumé

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.
Fichier non déposé

Dates et versions

cea-01834982 , version 1 (11-07-2018)

Identifiants

Citer

N. Kosmatov, J. Signoles. Runtime assertion checking and its combinations with static and dynamic analyses tutorial synopsis. Tests and Proofs. TAP 2014. Lecture Notes in Computer Science, Jul 2014, York, United Kingdom. pp.165-168, ⟨10.1007/978-3-319-09099-3_13⟩. ⟨cea-01834982⟩
23 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More