DC Field | Value | Language |
---|---|---|
dc.contributor.author | Bae, K. | - |
dc.contributor.author | Rocha, C. | - |
dc.date.accessioned | 2019-12-03T12:11:12Z | - |
dc.date.available | 2019-12-03T12:11:12Z | - |
dc.date.created | 2019-04-30 | - |
dc.date.issued | 2019-06 | - |
dc.identifier.issn | 0167-6423 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/100202 | - |
dc.description.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. | - |
dc.language | English | - |
dc.publisher | ELSEVIER SCIENCE BV | - |
dc.relation.isPartOf | SCIENCE OF COMPUTER PROGRAMMING | - |
dc.title | Symbolic state space reduction with guarded terms for rewriting modulo SMT | - |
dc.type | Article | - |
dc.identifier.doi | 10.1016/j.scico.2019.03.006 | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | SCIENCE OF COMPUTER PROGRAMMING, v.178, pp.20 - 42 | - |
dc.identifier.wosid | 000468012000002 | - |
dc.citation.endPage | 42 | - |
dc.citation.startPage | 20 | - |
dc.citation.title | SCIENCE OF COMPUTER PROGRAMMING | - |
dc.citation.volume | 178 | - |
dc.contributor.affiliatedAuthor | Bae, K. | - |
dc.identifier.scopusid | 2-s2.0-85063960210 | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.isOpenAccess | N | - |
dc.type.docType | Article | - |
dc.subject.keywordPlus | Symbolic state space | - |
dc.subject.keywordPlus | Symbolic techniques | - |
dc.subject.keywordPlus | Model checking | - |
dc.subject.keywordPlus | Scheduling algorithms | - |
dc.subject.keywordPlus | Concurrent computation | - |
dc.subject.keywordPlus | Infinite state systems | - |
dc.subject.keywordPlus | Rewriting logic | - |
dc.subject.keywordPlus | Rewriting modulo | - |
dc.subject.keywordPlus | State-space reduction | - |
dc.subject.keywordPlus | Symbolic reachability analysis | - |
dc.subject.keywordAuthor | CASH scheduling algorithm | - |
dc.subject.keywordAuthor | Rewriting logic | - |
dc.subject.keywordAuthor | Rewriting modulo SMT | - |
dc.subject.keywordAuthor | State space reduction | - |
dc.subject.keywordAuthor | Symbolic reachability analysis | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.