SAT and SMT Based Model Checking of Concurrent Systems

Tsuchiya, Tatsuhiro; Kikuno, Tohru

電子情報通信学会技術研究報告. CST, コンカレント工学, 2009, 109(73), 19-23

Number of Access:380（2025-08-15 20:53 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27252

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr109_73_19 pdf None 469 KB 92 2014.04.03  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
SAT and SMT Based Model Checking of Concurrent Systems
Creator
NRID
1000030283740 1000030283740
ORCID
0000-0002-3329-9235 0000-0002-3329-9235
researchmap permalink
tatsuhirotsuchiya72 tatsuhirotsuchiya72
Scopus Author ID
7403030658 7403030658
CreatorName
Tsuchiya, Tatsuhiro
NRID
1000050093745 1000050093745
CreatorName
Kikuno, Tohru
Subject
Model checking
concurrent systems
SAT
SMT
Abstract
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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. CST, コンカレント工学
Volume (Issue)
109(73)
Page
19-23
Date of Issued
2009-05-27
Language
English
Handle URL
https://hdl.handle.net/11094/27252
PISSN
09135685
NCID
AN10438446
Access Rights
open access
CopyRight
Copyright © 2009 by IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article