Complete SAT-Based Model Checking for Context-Free Processes

2007 ◽  
pp. 51-65 ◽  
Author(s):  
Geng-Dian Huang ◽  
Bow-Yaw Wang
Keyword(s):  
Model Checking ◽  
Context Free

Towards Nominal Context-Free Model-Checking

2013 ◽  
pp. 109-121 ◽  
Author(s):  
Pierpaolo Degano ◽  
Gian-Luigi Ferrari ◽  
Gianluca Mezzetti
Keyword(s):  
Model Checking ◽  
Free Model ◽  
Context Free

scholarly journals The Relationship between Markov Models and Wide-Area Networks with BOSS

2019 ◽  
Vol 8 (6S2) ◽  
pp. 668-671
Keyword(s):  
World Wide Web ◽  
Model Checking ◽  
World Wide ◽  
Markov Models ◽  
Wide Area Networks ◽  
Hash Tables ◽  
Context Free Grammar ◽  
The World ◽  
The Relationship ◽  
Context Free

Many security experts would agree that, had it not been forth econstruction of model checking, the deployment of access points might never have occurred .In this paper ,weverify the de- ploy men to fthe UNIVAC computer .In t his po sition paper wever if ythatthoughth eacclaimed trainable algorithm for the deployment of hash tables by Brown[21]is recursivel yenumerable, context-free grammar and the World Wide Web are generally incompatible. Weleaveoutthese results for anonymity

scholarly journals The Affiliation Between Markov Models and Wide-Area Networks with BOSS

2019 ◽  
Vol 8 (9S3) ◽  
pp. 945-949
Keyword(s):  
Model Checking ◽  
World Wide ◽  
Markov Models ◽  
Position Paper ◽  
Wide Area Networks ◽  
Hash Tables ◽  
Context Free Grammar ◽  
Recursively Enumerable ◽  
The World ◽  
Context Free

Many security experts would agree that ,had it not been for the Construction of model checking, the deployment of accesspoints might never have occurred.In this paper, weverifythede- ployment of the UNIV AC computer. In this position paper wever ifyth atthough the acclaimed train able algorithm for the deployment of hash tables by Brown[21]is recursively enumerable, context- free grammar and the World Wide Web are generally incompatible. We leave out these results for an onymity

scholarly journals Model-Checking Structured Context-Free Languages

2021 ◽  
pp. 387-410
Author(s):  
Michele Chiari ◽  
Dino Mandrioli ◽  
Matteo Pradella
Keyword(s):  
Model Checking ◽  
Use Cases ◽  
Temporal Logics ◽  
Local Properties ◽  
Nested Words ◽  
Checking Procedure ◽  
Definition Of ◽  
And Function ◽  
Context Free

AbstractThe problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, and provide a model checking procedure for it. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL by being FO-complete, and by expressing more easily stack inspection and function-local properties. We developed a model checking tool for POTL, which we experimentally evaluate on some interesting use-cases.

scholarly journals Temporal Logics Beyond Regularity

2007 ◽  
Vol 14 (13) ◽  
Author(s):  
Martin Lange
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Turing Machines ◽  
Temporal Logics ◽  
Propositional Dynamic Logic ◽  
Program Correctness ◽  
Recursive Procedures ◽  
Language Classes ◽  
Context Free

Non-regular program correctness properties play an important role in the specification of unbounded buffers, recursive procedures, etc. This thesis surveys results about the relative expressive power and complexity of temporal logics which are capable of defining non-regular properties. In particular, it features Propositional Dynamic Logic of Context-Free Programs, Fixpoint Logic with Chop, the Modal Iteration Calculus, and Higher-Order Fixpoint Logic.<br /> <br />Regarding expressive power we consider two classes of structures: arbitrary transition systems as well as finite words as a subclass of the former. The latter is meant to give an intuitive account of the logics' expressive powers by relating them to known language classes defined in terms of grammars or Turing Machines. <br /> <br /> Regarding the computational complexity of temporal logics beyond regularity we focus on their model checking problems since their satisfiability problems are all highly undecidable. Their model checking complexities range between polynomial time and non-elementary.

COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES

2010 ◽  
Vol 21 (02) ◽  
pp. 115-134
Author(s):  
GENG-DIAN HUANG ◽  
BOW-YAW WANG
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Boolean Satisfiability ◽  
Local Model ◽  
Sat Solvers ◽  
Proof Search ◽  
Software Programs ◽  
Context Free ◽  
Local Model Checking

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