The breakneck evolution of modern programming languages aggravates the development of deductive verification tools, which struggle to timely and fully support all new language features. To address this challenge, we present ByteBack: a verification technique that works on Java bytecode. Compared to high-level languages, intermediate representations such as bytecode offer a much more limited and stable set of features; hence, they may help decouple the verification process from changes in the source-level language. ByteBack offers a library to specify functional correctness properties at the level of the source code, so that the bytecode is only used as an intermediate representation that the end user does not need to work with. Then, ByteBack reconstructs some of the information about types and expressions that is erased during compilation into bytecode but is necessary to correctly perform verification. Our experiments with an implementation of ByteBack demonstrate that it can successfully verify bytecode compiled from different versions of Java, and including several modern language features that even state-of-the-art Java verifiers (such as KeY and OpenJML) do not directly support$\unicode{x2013}$thus revealing how ByteBack's approach can help keep up verification technology with language evolution.

翻译：现代编程语言的飞速发展加剧了演绎验证工具的开发难度，这些工具难以及时且全面地支持所有新语言特性。为应对这一挑战，我们提出了ByteBack：一种在Java字节码上工作的验证技术。与高级语言相比，字节码等中间表示提供了更为有限且稳定的特性集合；因此，它们有助于将验证过程与源代码级语言的变化解耦。ByteBack提供了一个在源代码层面指定功能正确性属性的库，使得字节码仅作为最终用户无需直接操作的中间表示。随后，ByteBack重建了部分在编译为字节码过程中被擦除、但对正确执行验证至关重要的类型和表达式信息。我们通过ByteBack实现进行的实验表明，该技术能成功验证从不同Java版本编译的字节码，并支持包括若干现代语言特性在内的验证——这些特性甚至是最先进的Java验证器（如KeY和OpenJML）都未直接支持的——从而揭示了ByteBack的方法如何帮助验证技术跟上语言演进的步伐。