Efficient Verification of Distributed Protocols Using Stateful Model Checking

2013 ◽  
Author(s):  
Habib Saissi ◽  
Peter Bokor ◽  
Can Arda Muftuoglu ◽  
Neeraj Suri ◽  
Marco Serafini
Keyword(s):  
Model Checking ◽  
Distributed Protocols ◽  
Efficient Verification

scholarly journals Efficient Strategies for CEGAR-Based Model Checking

2019 ◽  
Vol 64 (6) ◽  
pp. 1051-1091
Author(s):  
Ákos Hajdu ◽  
Zoltán Micskei
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
State Of The Art ◽  
Abstraction Refinement ◽  
Remarkable Improvement ◽  
Research Questions ◽  
Effectiveness And Efficiency ◽  
Efficient Verification ◽  
New Strategies

Abstract Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.

Model Checking Control Software for Nonlinear Dynamic Systems

2008 ◽  
Author(s):  
James Kapinski ◽  
Alexandre Donze ◽  
Flavio Lerda ◽  
Hitashyam Maka ◽  
Edmund Clarke ◽  
...  
Keyword(s):  
Model Checking ◽  
Dynamic Systems ◽  
Nonlinear Dynamic ◽  
Nonlinear Dynamic Systems ◽  
Control Software
Sign in / Sign up

Export Citation Format

Share Document