Trabalho em anais de eventoOpen Access
JCWIT: A Correctness-Witness Validator for Java Programs based on Bounded Model Checking
CHENG, Z.; WU, T.; SCHRAMMEL, P.; TIHANYI, N.; Lima Filho, E. B.; CORDEIRO, L. C
Resumo
Resumo
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.
palavras-chave
Palavras-chave
witness validationJava programsbounded model checkingprogram verificationprogram instrumentationassertionformal verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento