Open Access System for Information Sharing

Login Library

 

Article
Cited 3 time in webofscience Cited 4 time in scopus
Metadata Downloads

Symbolic state space reduction with guarded terms for rewriting modulo SMT SCIE SCOPUS

Title
Symbolic state space reduction with guarded terms for rewriting modulo SMT
Authors
Bae, K.Rocha, C.
Date Issued
2019-06
Publisher
ELSEVIER SCIENCE BV
Abstract
Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a non-deterministic environment, by seamlessly combining rewriting modulo equational theories, SMT solving, and model checking. This paper presents guarded terms, an approach to deal with the symbolic state-space explosion problem for rewriting modulo SMT, one of the main challenges of this technique. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach. (C) 2019 Elsevier B.V. All rights reserved.
URI
https://oasis.postech.ac.kr/handle/2014.oak/100202
DOI
10.1016/j.scico.2019.03.006
ISSN
0167-6423
Article Type
Article
Citation
SCIENCE OF COMPUTER PROGRAMMING, vol. 178, page. 20 - 42, 2019-06
Files in This Item:
There are no files associated with this item.

qr_code

  • mendeley

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Related Researcher

Researcher

배경민BAE, KYUNGMIN
Dept of Computer Science & Enginrg
Read more

Views & Downloads

Browse