Behind the Scenes in SANTE: A Combination of Static and Dynamic Analyses

Omar Chebaro 1, 2 Pascal Cuoq 3 Nikolai Kosmatov 3 Bruno Marre 3, 4 Anne Pacalet 5 Nicky Williams 3 Boris Yakobowski 3
2 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes Atlantique
3 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : While the development of one software verification tool is often seen as a difficult task, the realization of a tool combining various verification techniques is even more complex. This paper presents an innovative tool for verification of C programs called Sante (Static ANalysis and TEsting). We show how several tools based on heterogeneous techniques such as abstract interpretation, dependency analysis, program slicing, constraint solving and test generation can be combined within one tool. We describe the integration of these tools and discuss particular aspects of each underlying tool that are beneficial for the whole combination.
Document type :
Journal articles
Complete list of metadatas

https://hal.archives-ouvertes.fr/hal-00818147
Contributor : Omar Chebaro <>
Submitted on : Friday, April 26, 2013 - 10:26:11 AM
Last modification on : Thursday, February 7, 2019 - 4:10:13 PM

Identifiers

Citation

Omar Chebaro, Pascal Cuoq, Nikolai Kosmatov, Bruno Marre, Anne Pacalet, et al.. Behind the Scenes in SANTE: A Combination of Static and Dynamic Analyses. Automated Software Engineering, Springer Verlag, 2013, 21 (1), pp.107-143. ⟨10.1007/s10515-013-0127-x⟩. ⟨hal-00818147⟩

Share

Metrics

Record views

466