JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking

Zaiyu  Cheng; Tong Wu; Peter Schrammel; Norbert Tihanyi; Eddie B. de Lima Filho; Lucas Cordeiro

doi:10.1145/3650212.3685303

JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking

Zaiyu Cheng, Tong Wu, Peter Schrammel, Norbert Tihanyi, Eddie B. de Lima Filho, Lucas Cordeiro

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

Abstract

Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness’s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers.

Original language	English
Title of host publication	The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)
Pages	1831 - 1835
Number of pages	5
DOIs	https://doi.org/10.1145/3650212.3685303
Publication status	Published - 11 Sept 2024

Keywords

Correctness
Witness Validation
Java Programming
Bounded Model Checking

Access to Document

10.1145/3650212.3685303

Cite this

@inproceedings{5e75d4bcbf8a42a9a915e76576b9dd6e,

title = "JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking",

abstract = "Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness{\textquoteright}s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers. ",

keywords = "Correctness, Witness Validation, Java Programming, Bounded Model Checking",

author = "Zaiyu Cheng and Tong Wu and Peter Schrammel and Norbert Tihanyi and {de Lima Filho}, {Eddie B.} and Lucas Cordeiro",

year = "2024",

month = sep,

day = "11",

doi = "10.1145/3650212.3685303",

language = "English",

pages = "1831 -- 1835",

booktitle = "The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)",

}

TY - GEN

T1 - JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking

AU - Cheng, Zaiyu

AU - Wu, Tong

AU - Schrammel, Peter

AU - Tihanyi, Norbert

AU - de Lima Filho, Eddie B.

AU - Cordeiro, Lucas

PY - 2024/9/11

Y1 - 2024/9/11

N2 - Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness’s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers.

AB - Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness’s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers.

KW - Correctness

KW - Witness Validation

KW - Java Programming

KW - Bounded Model Checking

U2 - 10.1145/3650212.3685303

DO - 10.1145/3650212.3685303

M3 - Conference contribution

SP - 1831

EP - 1835

BT - The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)

ER -

JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking

Abstract

Keywords

Access to Document

Fingerprint

Cite this