Titre du document / Document title

Focuscheck : A tool for model checking and debugging sequential C programs

Auteur(s) / Author(s)

KELLER Curtis W. ⁽¹⁾ ; SAHA Diptikalyan ⁽²⁾ ; BASU Samik ⁽¹⁾ ; SMOLKA Scott A. ⁽²⁾ ;

Affiliation(s) du ou des auteurs / Author(s) Affiliation(s)

⁽¹⁾ Department of Computer Science, Iowa State University, Ames, ETATS-UNIS
⁽²⁾ Department of Computer Science, State University of New York, Stony Brook, ETATS-UNIS

Résumé / Abstract

We present the FocusCheck model-checking tool for the verification and easy debugging of assertion violations in sequential C programs. The main functionalities of the tool are the ability to: (a) identify all minimum-recursion, loop-free counter-examples in a C program using on-the-fly abstraction techniques; (b) extract focus-statement sequences (FSSs) from counter-examples, where a focus statement is one whose execution directly or indirectly causes the violation underlying a counter-example; (c) detect and discard infeasible counter-examples via feasibility analysis of the corresponding FSSs; and (d) isolate program segments that are most likely to harbor the erroneous statements causing the counter-examples. FocusCheck is equipped with a smart graphical user interface that provides various views of counter-examples in terms of their FSSs, thereby enhancing usability and readability of model-checking results.

Revue / Journal Title

Lecture notes in computer science   ISSN 0302-9743 

Source / Source

Congrès
TACAS 2005 : tools and algorithms for the construction and analysis of systems :   ( Edinburgh, 4-8 April 2005 )
International conference on tools and algorithms for the construction and analysis of systems N^o11, Edinburgh , ROYAUME-UNI (04/04/2005)
2005  , vol. 3440, pp. 563-569[Note(s) : XVII, 585 p., ] [Document : 7 p.] (8 ref.) ISBN 3-540-25333-5 ;  Illustration : Illustration ;

Langue / Language

Anglais

Editeur / Publisher

Springer, Berlin, ALLEMAGNE  (1973) (Revue)
Springer, Berlin, ALLEMAGNE  (2005) (Monographie)

Mots-clés anglais / English Keywords

Legibility ; Usability ; Abstraction ; Debugging program ; User interface ; Graphical interface ; Feasibility ; Debugging ; Program verification ; Model checking ; Software development ;

Mots-clés français / French Keywords

Lisibilité ; Utilisabilité ; Abstraction ; Programme débogage ; Interface utilisateur ; Interface graphique ; Faisabilité ; Débogage ; Vérification programme ; Vérification modèle ; Développement logiciel ;

Mots-clés espagnols / Spanish Keywords

Legibilidad ; Usabilidad ; Abstracción ; Programa puesta a punto ; Interfase usuario ; Interfaz grafica ; Practicabilidad ; Puesta a punto programa ; Verificación programa ; Verificación modelo ; Desarrollo logicial ;

Localisation / Location

INIST-CNRS, Cote INIST : 16343, 35400012447893.0390