Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

Tong Wu; Peter Schrammel; Lucas Cordeiro

doi:10.1007/978-3-030-99527-0_36

Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

Tong Wu, Peter Schrammel, Lucas Cordeiro

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

Abstract

We describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II
Editors	Dana Fisman, Grigore Rosu
Publisher	Springer Nature
Pages	484-489
Number of pages	6
Volume	13244
ISBN (Print)	9783030995263
DOIs	https://doi.org/10.1007/978-3-030-99527-0_36
Publication status	Published - 30 Mar 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Keywords

Java Bytecode
Software Verification
Witness Validation

Access to Document

10.1007/978-3-030-99527-0_36Licence: CC BY

1 Finished
1 Active

EnnCore: End-to-End Conceptual Guarding of Neural Architectures
Cordeiro, L. (PI), Brown, G. (CoI), Freitas, A. (CoI), Luján, M. (CoI) & Mustafa, M. (CoI)
1/02/21 → 31/12/24
Project: Research
SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research

Cite this

Wu, T., Schrammel, P., & Cordeiro, L. (2022). Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). In D. Fisman, & G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II (Vol. 13244, pp. 484-489). (Lecture Notes in Computer Science). Springer Nature. https://doi.org/10.1007/978-3-030-99527-0_36

Wu, Tong ; Schrammel, Peter ; Cordeiro, Lucas. / Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. editor / Dana Fisman ; Grigore Rosu. Vol. 13244 Springer Nature, 2022. pp. 484-489 (Lecture Notes in Computer Science).

@inproceedings{27ff35a093c34690a7fe6c88537bbbf0,

title = "Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)",

abstract = "We describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.",

keywords = "Java Bytecode, Software Verification, Witness Validation",

author = "Tong Wu and Peter Schrammel and Lucas Cordeiro",

year = "2022",

month = mar,

day = "30",

doi = "10.1007/978-3-030-99527-0_36",

language = "English",

isbn = "9783030995263",

volume = "13244",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "484--489",

editor = "Dana Fisman and Grigore Rosu",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II",

address = "United States",

}

Wu, T, Schrammel, P & Cordeiro, L 2022, Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). in D Fisman & G Rosu (eds), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. vol. 13244, Lecture Notes in Computer Science, Springer Nature, pp. 484-489. https://doi.org/10.1007/978-3-030-99527-0_36

Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). / Wu, Tong; Schrammel, Peter; Cordeiro, Lucas.
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. ed. / Dana Fisman; Grigore Rosu. Vol. 13244 Springer Nature, 2022. p. 484-489 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

AU - Wu, Tong

AU - Schrammel, Peter

AU - Cordeiro, Lucas

PY - 2022/3/30

Y1 - 2022/3/30

N2 - We describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.

AB - We describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.

KW - Java Bytecode

KW - Software Verification

KW - Witness Validation

U2 - 10.1007/978-3-030-99527-0_36

DO - 10.1007/978-3-030-99527-0_36

M3 - Conference contribution

SN - 9783030995263

VL - 13244

T3 - Lecture Notes in Computer Science

SP - 484

EP - 489

BT - Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II

A2 - Fisman, Dana

A2 - Rosu, Grigore

PB - Springer Nature

ER -

Wu T, Schrammel P, Cordeiro L. Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). In Fisman D, Rosu G, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Vol. 13244. Springer Nature. 2022. p. 484-489. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-99527-0_36

Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

EnnCore: End-to-End Conceptual Guarding of Neural Architectures

SCorCH: Secure Code for Capability Hardware

Cite this