SAT and SMT Based Model Checking of Concurrent Systems

Autor: Tsuchiya, Tatsuhiro, Kikuno, Tohru
Jazyk: angličtina
Rok vydání: 2009
Předmět:
Zdroj: 電子情報通信学会技術研究報告. CST, コンカレント工学. 109(73):19-23
ISSN: 0913-5685
Popis: We discuss model checking that uses a SAT (satisfiability) or SMT (satisfiability modulo theory) solver. The basic idea behind this model checking approach is to reduce the model checking problem to the satisfiability problem of a formula of some logic. Recent advances in SAT and SMT solvers make this particular approach significantly attractive. However, it does not work effectively in verification of concurrent systems, because the size of the formula blows up if the system has high concurrency. To overcome this challenge, we propose a new semantics for concurrent systems. The new semantics allows a compact formula representation of the behavior of concurrent systems. In this paper, we first introduce this new semantics and bounded model checking based on it, in the context of a general model of concurrent systems. Then we apply it to two specific concurrent system models, namely Petri nets and concurrent programs using unbounded integer variables.
Databáze: OpenAIRE