DocumentCode :
2832921
Title :
Static Checking by Means of Abstract Interpretation
Author :
Musumbu, Kaninda
Author_Institution :
LaBRI (UMR 5800 du CNRS), Univ. Bordeaux 1, Bordeaux
fYear :
2008
fDate :
Aug. 29 2008-Sept. 2 2008
Firstpage :
107
Lastpage :
112
Abstract :
Dynamic checking are usually easier to use, because the concept are established and wide well know. But they are usually limited to systems whose state space is finite. In an other part, certain faults cannot be detected dynamically, even by keeping track of the history of the state space. Indeed, the classical problem of finding the right test cases is far from trivial and limit the abilities of dynamic checkers further. Static checking have the advantage that they work on a more abstract level than dynamic checker and can verify system properties for all inputs. Problem, it is hard to assure that a violation of a modeled property corresponds to a fault in the concrete system. We propose an approach, in which we generate counter-examples dynamically using the abstract interpretation techniques.
Keywords :
formal verification; abstract interpretation; dynamic checking; state space; static checking; system properties verification; Binary decision diagrams; Computer science; Concrete; Data structures; Explosions; Fault detection; History; Information technology; State-space methods; Testing; Model checking; abstract interpretation; fixpoint computation; refinement; static analysis;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Science and Information Technology, 2008. ICCSIT '08. International Conference on
Conference_Location :
Singapore
Print_ISBN :
978-0-7695-3308-7
Type :
conf
DOI :
10.1109/ICCSIT.2008.10
Filename :
4624842
Link To Document :
بازگشت