scholarly journals Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications

2011 ◽  
Vol 2011 ◽  
pp. 1-13 ◽  
Author(s):  
Salamah Salamah ◽  
Ann Q. Gates ◽  
Steve Roach ◽  
Matthew Engskow
Keyword(s):  
Model Checking ◽  
Spin Model ◽  
Software Systems ◽  
Formal Specifications ◽  
Model Checker ◽  
Software Model Checking ◽  
Software Model ◽  
Property Specification ◽  
Büchi Automaton ◽  
Spin Model Checker

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.

scholarly journals Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)

2021 ◽  
pp. 433-437
Author(s):  
Zsófia Ádám ◽  
Gyula Sallai ◽  
Ákos Hajdu
Keyword(s):  
Model Checking ◽  
Predicate Abstraction ◽  
Model Checker ◽  
Software Model Checking ◽  
Abstraction Refinement ◽  
Value Analysis ◽  
C Programs ◽  
Software Model

AbstractGazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.

Verification of MPI Java programs using software model checking

2016 ◽  
Vol 51 (8) ◽  
pp. 1-2
Author(s):  
Waqas Ur Rehman ◽  
Muhammad Sohaib Ayub ◽  
Junaid Haroon Siddiqui
Keyword(s):  
Model Checking ◽  
Software Model Checking ◽  
Software Model ◽  
Java Programs

scholarly journals Efficient software model checking of soundness of type systems

2008 ◽  
Vol 43 (10) ◽  
pp. 493-504 ◽  
Author(s):  
Michael Roberson ◽  
Melanie Harries ◽  
Paul T. Darga ◽  
Chandrasekhar Boyapati
Keyword(s):  
Model Checking ◽  
Type Systems ◽  
Software Model Checking ◽  
Software Model ◽  
Efficient Software

scholarly journals Software Model Checking of UDP-based Distributed Applications

2015 ◽  
Vol 5 (2) ◽  
pp. 373-402 ◽  
Author(s):  
Nazim Sebih ◽  
Masami Hagiya ◽  
Franz Weitl ◽  
Mitsuharu Yamamoto ◽  
Cyrille Artho ◽  
...  
Keyword(s):  
Model Checking ◽  
Distributed Applications ◽  
Software Model Checking ◽  
Software Model

scholarly journals Parallel Assignments in Software Model Checking

2006 ◽  
Vol 157 (1) ◽  
pp. 77-94
Author(s):  
Murray Stokely ◽  
Sagar Chaki ◽  
Joël Ouaknine
Keyword(s):  
Model Checking ◽  
Software Model Checking ◽  
Software Model
Sign in / Sign up

Export Citation Format

Share Document