Trabalho em anais de eventoOpen Access

Wit4Java: A violation-witness validator for Java Verifiers (Competition Paper

WU, T.; SCHRAMMEL, P.; CORDEIRO, L. C

2022 • 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems • 10 citações

Resumo

Resumo

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.

palavras-chave

Palavras-chave

program verificationsafety properties

Status

Published

links

Links e arquivos

DOI

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

Link Externo

https://doi.org/10.1007/978-3-030-99527-0_36

Repositório

https://research.manchester.ac.uk/en/publications/27ff35a0-93c3-4690-a7fe-6c88537bbbf0

Abrir publicação

Trabalho em anais de evento

Leveraging Template Matching for Efficient Android Screenshot Visual InspectionMYRRIA, ABDA; CASTRO, ALICE; MUNIZ, CAIQUE; BARBOSA, HERYCK; SILVA, ANDRÉ; CORDOVIL, LUIZ; PORTY, ROGER; SOUTO, THIAGO2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)1citações

Comparative Evaluation of DNNs and Template Matching for GUI Validation on Android DevicesMYRRIA, ABDA; CASTRO, ALICE; MUNIZ, CAIQUE; BARBOSA, HERYCK; SILVA, ANDRÉ; CORDOVIL-JR, LUIZ; PORTY, ROGER; SOUTO, THIAGO2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)

LLM-based text-to-JQL Generation: an automated test using execution and structural indicatorsLIMA, RAYFRAN ROCHA; DE BRITO, IRINEU EVANGELISTA CRUZ; NASCIMENTO, JARDEL DA CUNHA; CORDOVIL-JR, LUIZ2026 • 2026 IEEE International Conference on Consumer Electronics (ICCE)

Bearing fault prognosis based on evolving granular modelsMARTINIANO, ALEXANDRE; VITÓRIO, ANDEVALDO; AYRES, FLORINDO; OTANI, MARIO; MEDEIROS, JOSÉ; NUNES, RIVELINO; SILVA, RENAN; VARELA, JERRY; MOURA, DAVIDSON; SANTOS, KENNY; COSTA, JEFERSON; MENDONÇA, RAFAEL; BESSA, IURY2026 • XX Simpósio Brasileiro de Automação Inteligente (SBAI 2025) e XII Simpósio Brasileiro de Sistemas Elétricos (SBSE 2025)

Ver todas as publicações