SMTBCF: Efficient Backbone Computing for SMT Formulas

Yueling Zhang; Geguang Pu; Min Zhang

doi:10.1007/978-3-030-32409-4_3

SMTBCF: Efficient Backbone Computing for SMT Formulas

Yueling Zhang^*
, Geguang Pu
, Min Zhang

^*此作品的通讯作者

软件工程学院

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

2 引用（Scopus）

摘要

SMT (Satisfiable Module Theory) formulas have been widely used in practical applications. In some of the applications, including finding program bugs, plainly solving an SMT formula is sufficient. For other applications, besides solving the SMT formula, backbone variables of the SMT formulas are also needed in order to tackle the practical problems including finding invariant of certain properties in program analysis. This paper proposed a new approach SMTBCF to compute backbone variables for SMT formulas in order to accelerate the computing of backbone variables in SMT formulas and increase the efficiency of SMT formulas in practical applications. SMTBCF is the first algorithm that uses the backbone predicates to find part of the backbone variables in the SMT formulas. SMTBCF is also the first algorithm that uses the constants in the relating predicates of a backbone variable to quickly find the Unsatisfiable Evaluation of the backbone variable. In this way, SMTBCF is able to find backbone variables of SMT formulas, reduce the number of SMT solving in SMT backbone computing, and increase the efficiency of backbone variables in SMT formulas.

源语言	英语
主期刊名	Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
编辑	Yamine Ait-Ameur, Shengchao Qin
出版商	Springer
页	36-51
页数	16
ISBN（印刷版）	9783030324087
DOI	https://doi.org/10.1007/978-3-030-32409-4_3
出版状态	已出版 - 2019
活动	21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, 中国期限: 5 11月 2019 → 9 11月 2019

出版系列

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	11852 LNCS
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	21st International Conference on Formal Engineering Methods, ICFEM 2019
国家/地区	中国
市	Shenzhen
时期	5/11/19 → 9/11/19

访问文件

10.1007/978-3-030-32409-4_3

其它文件与链接

链接到 Scopus 的出版物

引用此

Zhang, Y., Pu, G., & Zhang, M. (2019). SMTBCF: Efficient Backbone Computing for SMT Formulas. 在 Y. Ait-Ameur, & S. Qin (编辑), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings (页码 36-51). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 11852 LNCS). Springer. https://doi.org/10.1007/978-3-030-32409-4_3

Zhang, Yueling ; Pu, Geguang ; Zhang, Min. / SMTBCF : Efficient Backbone Computing for SMT Formulas. Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. 编辑 / Yamine Ait-Ameur ; Shengchao Qin. Springer, 2019. 页码 36-51 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ccb9508dc0a4443e8e141c83766b3dda,

title = "SMTBCF: Efficient Backbone Computing for SMT Formulas",

abstract = "SMT (Satisfiable Module Theory) formulas have been widely used in practical applications. In some of the applications, including finding program bugs, plainly solving an SMT formula is sufficient. For other applications, besides solving the SMT formula, backbone variables of the SMT formulas are also needed in order to tackle the practical problems including finding invariant of certain properties in program analysis. This paper proposed a new approach SMTBCF to compute backbone variables for SMT formulas in order to accelerate the computing of backbone variables in SMT formulas and increase the efficiency of SMT formulas in practical applications. SMTBCF is the first algorithm that uses the backbone predicates to find part of the backbone variables in the SMT formulas. SMTBCF is also the first algorithm that uses the constants in the relating predicates of a backbone variable to quickly find the Unsatisfiable Evaluation of the backbone variable. In this way, SMTBCF is able to find backbone variables of SMT formulas, reduce the number of SMT solving in SMT backbone computing, and increase the efficiency of backbone variables in SMT formulas.",

keywords = "Backbone, SMT, Verification",

author = "Yueling Zhang and Geguang Pu and Min Zhang",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 21st International Conference on Formal Engineering Methods, ICFEM 2019 ; Conference date: 05-11-2019 Through 09-11-2019",

year = "2019",

doi = "10.1007/978-3-030-32409-4\_3",

language = "英语",

isbn = "9783030324087",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "36--51",

editor = "Yamine Ait-Ameur and Shengchao Qin",

booktitle = "Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings",

address = "德国",

}

Zhang, Y , Pu, G & Zhang, M 2019, SMTBCF: Efficient Backbone Computing for SMT Formulas. 在 Y Ait-Ameur & S Qin (编辑), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 卷 11852 LNCS, Springer, 页码 36-51, 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, 中国, 5/11/19. https://doi.org/10.1007/978-3-030-32409-4_3

SMTBCF: Efficient Backbone Computing for SMT Formulas. / Zhang, Yueling ; Pu, Geguang ; Zhang, Min.
Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. 编辑 / Yamine Ait-Ameur; Shengchao Qin. Springer, 2019. 页码 36-51 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 11852 LNCS).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

TY - GEN

T1 - SMTBCF

T2 - 21st International Conference on Formal Engineering Methods, ICFEM 2019

AU - Zhang, Yueling

AU - Pu, Geguang

AU - Zhang, Min

PY - 2019

Y1 - 2019

N2 - SMT (Satisfiable Module Theory) formulas have been widely used in practical applications. In some of the applications, including finding program bugs, plainly solving an SMT formula is sufficient. For other applications, besides solving the SMT formula, backbone variables of the SMT formulas are also needed in order to tackle the practical problems including finding invariant of certain properties in program analysis. This paper proposed a new approach SMTBCF to compute backbone variables for SMT formulas in order to accelerate the computing of backbone variables in SMT formulas and increase the efficiency of SMT formulas in practical applications. SMTBCF is the first algorithm that uses the backbone predicates to find part of the backbone variables in the SMT formulas. SMTBCF is also the first algorithm that uses the constants in the relating predicates of a backbone variable to quickly find the Unsatisfiable Evaluation of the backbone variable. In this way, SMTBCF is able to find backbone variables of SMT formulas, reduce the number of SMT solving in SMT backbone computing, and increase the efficiency of backbone variables in SMT formulas.

AB - SMT (Satisfiable Module Theory) formulas have been widely used in practical applications. In some of the applications, including finding program bugs, plainly solving an SMT formula is sufficient. For other applications, besides solving the SMT formula, backbone variables of the SMT formulas are also needed in order to tackle the practical problems including finding invariant of certain properties in program analysis. This paper proposed a new approach SMTBCF to compute backbone variables for SMT formulas in order to accelerate the computing of backbone variables in SMT formulas and increase the efficiency of SMT formulas in practical applications. SMTBCF is the first algorithm that uses the backbone predicates to find part of the backbone variables in the SMT formulas. SMTBCF is also the first algorithm that uses the constants in the relating predicates of a backbone variable to quickly find the Unsatisfiable Evaluation of the backbone variable. In this way, SMTBCF is able to find backbone variables of SMT formulas, reduce the number of SMT solving in SMT backbone computing, and increase the efficiency of backbone variables in SMT formulas.

KW - Backbone

KW - SMT

KW - Verification

UR - https://www.scopus.com/pages/publications/85076185075

U2 - 10.1007/978-3-030-32409-4_3

DO - 10.1007/978-3-030-32409-4_3

M3 - 会议稿件

AN - SCOPUS:85076185075

SN - 9783030324087

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 36

EP - 51

BT - Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings

A2 - Ait-Ameur, Yamine

A2 - Qin, Shengchao

PB - Springer

Y2 - 5 November 2019 through 9 November 2019

ER -

Zhang Y , Pu G , Zhang M. SMTBCF: Efficient Backbone Computing for SMT Formulas. 在 Ait-Ameur Y, Qin S, 编辑, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Springer. 2019. 页码 36-51. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-32409-4_3

SMTBCF: Efficient Backbone Computing for SMT Formulas

摘要

出版系列

会议

访问文件

其它文件与链接

指纹

引用此