Open Access 2022 | OriginalPaper | Buchkapitel
Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)
verfasst von : Tong Wu, Peter Schrammel, Lucas C. Cordeiro
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
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.