A program's exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program's correctness. On the other hand, formally verifying realistic programs is likely to involve exceptions -- a ubiquitous feature in modern programming languages. In this paper, we present a novel approach to verify the exceptional behavior of Java programs, which extends our previous work on ByteBack. ByteBack works on a program's bytecode, while providing means to specify the intended behavior at the source-code level; this approach sets ByteBack apart from most state-of-the-art verifiers that target source code. To explicitly model a program's exceptional behavior in a way that is amenable to formal reasoning, we introduce Vimp: a high-level bytecode representation that extends the Soot framework's Grimp with verification-oriented features, thus serving as an intermediate layer between bytecode and the Boogie intermediate verification language. Working on bytecode through this intermediate layer brings flexibility and adaptability to new language versions and variants: as our experiments demonstrate, ByteBack can verify programs involving exceptional behavior in all versions of Java, as well as in Scala and Kotlin (two other popular JVM languages).

翻译：程序的异常行为会显著增加其控制流的复杂性，从而影响程序正确性推理的准确性。另一方面，对实际程序进行形式化验证很可能涉及异常处理——这是现代编程语言中普遍存在的特性。本文提出了一种验证Java程序异常行为的新方法，该方法扩展了我们先前在ByteBack上的研究工作。ByteBack直接在程序的字节码层面进行操作，同时提供在源代码层面描述预期行为的方法；这种设计使ByteBack有别于大多数针对源代码的先进验证器。为了以适合形式化推理的方式显式建模程序的异常行为，我们引入了Vimp：一种高层字节码表示形式，它在Soot框架的Grimp基础上扩展了面向验证的特性，从而作为字节码与Boogie中间验证语言之间的中间层。通过该中间层在字节码上进行操作，为适应新的语言版本和变体带来了灵活性与适应性：如实验所示，ByteBack能够验证涉及异常行为的全版本Java程序，以及Scala和Kotlin（另外两种流行的JVM语言）程序。