Naslov
Predicate Abstraction based Verification Framework: First Results

Autori
Pek, Edgar ; Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the Joint Conferences Computers in Technical systems and Intelligent systems / Budin, Leo ; Ribarić, Slobodan - Rijeka : Hrvatska udruga za informacijsku i komunikacijsku tehnologiju, elektroniku i mikroelektroniku - MIPRO, 2006, 37-41

Skup
29th International Convention MIPRO 2006 - Computers in Technical Systems

Mjesto i datum
Opatija, Hrvatska, 22.05.2006. - 26.05.2006

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
software engineering; formal verification; predicate abstraction; model checking; theorem proving

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA