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

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

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.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
Editors	Yamine Ait-Ameur, Shengchao Qin
Publisher	Springer
Pages	36-51
Number of pages	16
ISBN (Print)	9783030324087
DOIs	https://doi.org/10.1007/978-3-030-32409-4_3
State	Published - 2019
Event	21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, China Duration: 5 Nov 2019 → 9 Nov 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11852 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Formal Engineering Methods, ICFEM 2019
Country/Territory	China
City	Shenzhen
Period	5/11/19 → 9/11/19

Keywords

Backbone
SMT
Verification

Access to Document

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

Cite this

Zhang, Y., Pu, G., & Zhang, M. (2019). SMTBCF: Efficient Backbone Computing for SMT Formulas. In Y. Ait-Ameur, & S. Qin (Eds.), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings (pp. 36-51). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 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. editor / Yamine Ait-Ameur ; Shengchao Qin. Springer, 2019. pp. 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. in Y Ait-Ameur & S Qin (eds), 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), vol. 11852 LNCS, Springer, pp. 36-51, 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, 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. ed. / Yamine Ait-Ameur; Shengchao Qin. Springer, 2019. p. 36-51 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11852 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In Ait-Ameur Y, Qin S, editors, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Springer. 2019. p. 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

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this