local model checking
Recently Published Documents


TOTAL DOCUMENTS

31
(FIVE YEARS 0)

H-INDEX

11
(FIVE YEARS 0)

10.29007/df56 ◽  
2018 ◽  
Author(s):  
Nikolay V. Shilov

Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. This extended abstract sketches a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.


Author(s):  
Jonas Finnemann Jensen ◽  
Kim Guldstrand Larsen ◽  
Jiří Srba ◽  
Lars Kaerlund Oestergaard

2010 ◽  
Vol 21 (02) ◽  
pp. 115-134
Author(s):  
GENG-DIAN HUANG ◽  
BOW-YAW WANG

A complete SAT-based model checking algorithm for context-free processes is presented. We reduce proof search in local model checking to Boolean satisfiability. Bounded proof search can therefore be performed by SAT solvers. Moreover, the completeness of proof search is reduced to Boolean unsatisfiability and hence can be checked by SAT solvers. By encoding the local model checking algorithm in [13], SAT solvers are able to verify properties in the universal fragment of alternation-free µ-calculus formulae on context-free processes. Since software programs can be modeled by context-free processes, our result demonstrates that a purely SAT-based algorithm for software verification is indeed possible.


Sign in / Sign up

Export Citation Format

Share Document