Trace-driven verification of multithreaded programs

Zijiang Yang; Karem Sakallah

doi:10.1007/978-3-642-16901-4_27

Trace-driven verification of multithreaded programs

Zijiang Yang
, Karem Sakallah

Faculty of Electronic and Information Engineering

University of Michigan, Ann Arbor

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

1 Scopus citations

Abstract

We present a new method that combines the efficiency of testing with the reasoning power of satisfiability modulo theory (SMT) solvers for the verification of multithreaded programs under a user specified test vector. Our method performs dynamic executions to obtain both under- and over-approximations of the program, represented as quantifier-free first order logic formulas. The formulas are then analyzed by an SMT solver which implicitly considers all possible thread interleavings. The symbolic analysis may return the following results: (1) it reports a real bug, (2) it proves that the program has no bug under the given input, or (3) it remains inconclusive because the analysis is based on abstractions. In the last case, we present a refinement procedure that uses symbolic analysis to guide further executions.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings
Pages	404-419
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-16901-4_27
State	Published - 2010
Event	12th International Conference on Formal Engineering Methods, ICFEM 2010 - Shanghai, China Duration: 17 Nov 2010 → 19 Nov 2010

Publication series

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

Conference

Conference	12th International Conference on Formal Engineering Methods, ICFEM 2010
Country/Territory	China
City	Shanghai
Period	17/11/10 → 19/11/10

Access to Document

10.1007/978-3-642-16901-4_27

Cite this

Yang, Z., & Sakallah, K. (2010). Trace-driven verification of multithreaded programs. In Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings (pp. 404-419). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6447 LNCS). https://doi.org/10.1007/978-3-642-16901-4_27

@inproceedings{8869a86ff51e48bdb911af0767908ca0,

title = "Trace-driven verification of multithreaded programs",

abstract = "We present a new method that combines the efficiency of testing with the reasoning power of satisfiability modulo theory (SMT) solvers for the verification of multithreaded programs under a user specified test vector. Our method performs dynamic executions to obtain both under- and over-approximations of the program, represented as quantifier-free first order logic formulas. The formulas are then analyzed by an SMT solver which implicitly considers all possible thread interleavings. The symbolic analysis may return the following results: (1) it reports a real bug, (2) it proves that the program has no bug under the given input, or (3) it remains inconclusive because the analysis is based on abstractions. In the last case, we present a refinement procedure that uses symbolic analysis to guide further executions.",

author = "Zijiang Yang and Karem Sakallah",

year = "2010",

doi = "10.1007/978-3-642-16901-4\_27",

language = "英语",

isbn = "3642169007",

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

pages = "404--419",

booktitle = "Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings",

note = "12th International Conference on Formal Engineering Methods, ICFEM 2010 ; Conference date: 17-11-2010 Through 19-11-2010",

}

Yang, Z & Sakallah, K 2010, Trace-driven verification of multithreaded programs. in Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6447 LNCS, pp. 404-419, 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, 17/11/10. https://doi.org/10.1007/978-3-642-16901-4_27

Trace-driven verification of multithreaded programs. / Yang, Zijiang; Sakallah, Karem.
Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings. 2010. p. 404-419 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6447 LNCS).

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

TY - GEN

T1 - Trace-driven verification of multithreaded programs

AU - Yang, Zijiang

AU - Sakallah, Karem

PY - 2010

Y1 - 2010

N2 - We present a new method that combines the efficiency of testing with the reasoning power of satisfiability modulo theory (SMT) solvers for the verification of multithreaded programs under a user specified test vector. Our method performs dynamic executions to obtain both under- and over-approximations of the program, represented as quantifier-free first order logic formulas. The formulas are then analyzed by an SMT solver which implicitly considers all possible thread interleavings. The symbolic analysis may return the following results: (1) it reports a real bug, (2) it proves that the program has no bug under the given input, or (3) it remains inconclusive because the analysis is based on abstractions. In the last case, we present a refinement procedure that uses symbolic analysis to guide further executions.

AB - We present a new method that combines the efficiency of testing with the reasoning power of satisfiability modulo theory (SMT) solvers for the verification of multithreaded programs under a user specified test vector. Our method performs dynamic executions to obtain both under- and over-approximations of the program, represented as quantifier-free first order logic formulas. The formulas are then analyzed by an SMT solver which implicitly considers all possible thread interleavings. The symbolic analysis may return the following results: (1) it reports a real bug, (2) it proves that the program has no bug under the given input, or (3) it remains inconclusive because the analysis is based on abstractions. In the last case, we present a refinement procedure that uses symbolic analysis to guide further executions.

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

U2 - 10.1007/978-3-642-16901-4_27

DO - 10.1007/978-3-642-16901-4_27

M3 - 会议稿件

AN - SCOPUS:78649585677

SN - 3642169007

SN - 9783642169007

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

SP - 404

EP - 419

BT - Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings

T2 - 12th International Conference on Formal Engineering Methods, ICFEM 2010

Y2 - 17 November 2010 through 19 November 2010

ER -

Yang Z, Sakallah K. Trace-driven verification of multithreaded programs. In Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings. 2010. p. 404-419. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-16901-4_27

Trace-driven verification of multithreaded programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this