Show simple item record

dc.contributor.authorYang, Jinji
dc.contributor.authorSu, Kaile
dc.contributor.authorChen, Qingliang
dc.contributor.editorJifeng He, Jian Lv, Jim Davies and Xuandong Li
dc.date.accessioned2017-05-03T14:39:43Z
dc.date.available2017-05-03T14:39:43Z
dc.date.issued2008
dc.date.modified2011-08-08T07:21:45Z
dc.identifier.doi10.1109/TASE.2008.23
dc.identifier.urihttp://hdl.handle.net/10072/39766
dc.description.abstractBounded Model Checking (BMC) has played an important role in verification of software, embedded systems and protocols. The idea of BMC is to encode Finite State Machine (FSM) and Linear Temporal Logic (LTL) verification specification into satisfiability (SAT) instances, and then to search for a counterexample via various SAT tools. Improving encoding technology of BMC can generate a SAT instance easy to solve, and therefore is essential to improve the efficiency of BMC. In this paper, we improve the encoding of BMC by combining the characteristic of FSM state transition and semantics of LTL, get a simple and efficient recursion formula which is useful to efficiently generate SAT instances. We present an efficient algorithm to encode the modal operator (safety formula) in BMC. The experiments for comparative analysis shows that this encoding algorithm is more powerful than the existing two mainstream encoding algorithms in both the scale of generated SAT instances and the solving efficiency. The methodology presented in this paper is also valuable for optimization of other modal operator encodings in BMC.
dc.description.peerreviewedYes
dc.description.publicationstatusYes
dc.format.extent276379 bytes
dc.format.mimetypeapplication/pdf
dc.languageEnglish
dc.language.isoeng
dc.publisherIEEE
dc.publisher.placeUnited States
dc.relation.ispartofstudentpublicationN
dc.relation.ispartofconferencename2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
dc.relation.ispartofconferencetitleTASE 2008 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering
dc.relation.ispartofdatefrom2008-06-17
dc.relation.ispartofdateto2008-06-19
dc.relation.ispartoflocationNanjing, China
dc.rights.retentionY
dc.subject.fieldofresearchComputational logic and formal languages
dc.subject.fieldofresearchcode461303
dc.titleImproving Encoding Efficiency for Bounded Model Checking
dc.typeConference output
dc.type.descriptionE1 - Conferences
dc.type.codeE - Conference Publications
gro.rights.copyright© 2008 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
gro.date.issued2008
gro.hasfulltextFull Text
gro.griffith.authorSu, Kaile


Files in this item

This item appears in the following Collection(s)

  • Conference outputs
    Contains papers delivered by Griffith authors at national and international conferences.

Show simple item record