engleski

Predicate Abstraction based Verification Framework: First Results

The analysis of software artifacts is steadily advancing due to the increase in computational power and new verification methodologies. As a result there is a trend to approach the verification of the implementation level code and systems with unbounded state space rather than verification of abstract hand-built models of code. We consider a methodology which enables the verification of systems with unbounded state space. This methodology is called predicate abstraction. The predicate abstraction enable automatic construction of the finite abstraction from the infinite system. The finite abstraction has more behaviours than original system and preserves safety properties. In this work we present first results in our implementation of the framework for the predicate abstraction.

software engineering; formal verification; predicate abstraction; model checking; theorem proving

nije evidentirano