A candid industrial evaluation of formal software verification using model checking

2014 ◽  
Author(s):  
Matthew Bennion ◽  
Ibrahim Habli
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Formal Software Verification

scholarly journals A Latent Implementation Error Detection Method for Software Validation

2013 ◽  
Vol 2013 ◽  
pp. 1-10
Author(s):  
Jiantao Zhou ◽  
Jing Liu ◽  
Jinzhao Wu ◽  
Guodong Zhong
Keyword(s):  
Model Checking ◽  
Error Detection ◽  
Software Verification ◽  
Conformance Testing ◽  
Software Validation ◽  
Software Model Checking ◽  
Software Model ◽  
Novel Approach ◽  
Tightly Coupled ◽  
Security Properties

Model checking and conformance testing play an important role in software system design and implementation. From the view of integrating model checking and conformance testing into a tightly coupled validation approach, this paper presents a novel approach to detect latent errors in software implementation. The latent errors can be classified into two kinds, one is called as Unnecessary Implementation Trace, and the other is called as Neglected Implementation Trace. The method complements the incompleteness of security properties for software model checking. More accurate models are characterized to leverage the effectiveness of the model-based software verification and testing combined method.

Comparison of Model Checking Tools

2013 ◽  
Vol 659 ◽  
pp. 181-185
Author(s):  
Wei Gong ◽  
Jun Wei Jia
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Bounded Model Checking ◽  
Hardware Verification ◽  
Model Checker ◽  
Software And Hardware ◽  
Inherent Part

Model Checking is a method for verification. The model will be checked until the specification of it is proved or disproved. With the rising complexity of big models, there are non-checkable cases, in which cases the problem can be analyzed by some models, for example, bounded Model Checking means to analyze the model until a defined time or depth. The verification happens automatically. The programs for doing this are called Model Checking Tools or Model Checker. Model Checking are used in both software and hardware verification. It is an inherent part of hardware verification, whereas it is less used in the software verification.

scholarly journals Efficient SAT-based bounded model checking for software verification

2008 ◽  
Vol 404 (3) ◽  
pp. 256-274 ◽  
Author(s):  
Franjo Ivančić ◽  
Zijiang Yang ◽  
Malay K. Ganai ◽  
Aarti Gupta ◽  
Pranav Ashar
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Bounded Model Checking
Sign in / Sign up

Export Citation Format

Share Document