Title: Toward a backward model checking

Authors: Aleb Nassima; Tamen Zahia; Kamel Nadjet

Addresses: Computer Sciences Department, USTHB, BP 32 Al Allia 16111, Bab Ezzouar, Algiers, Algeria. ' Computer Sciences Department, USTHB, BP 32 Al Allia 16111, Bab Ezzouar, Algiers, Algeria. ' Computer Sciences Department, USTHB, BP 32 Al Allia 16111, Bab Ezzouar, Algiers, Algeria

Abstract: This paper presents a new method of program verification, backward incremental model checking (BIMC). BIMC is a backward compositional technique to check, statically safety properties of C programs. A program is a hierarchy of blocks. Blocks are analysed in reverse order until we prove or disprove property. To our knowledge, it is the first work dealing with program model checking in a backward way. We define a new method: ASMA for program modelling. ASMA allows separating a program into two components: the data model and the control model. This approach allows an easy program manipulation. BIMC starts the verification with a minimal set P0 which is then incrementally extended each time needed. The weakest precondition concept is applied on the two models in an adequate and incremental way. BIMC allows handling programs containing function calls and pointers. All the techniques described in this paper are illustrated by clarifying examples.

Keywords: computer aided verification; software verification; software analysis; software model checking; program modelling; languages; static analysis; program verification; backward incremental model checking.

DOI: 10.1504/IJCAET.2013.050552

International Journal of Computer Aided Engineering and Technology, 2013 Vol.5 No.1, pp.20 - 43

Published online: 30 Jan 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article