BSP-WHY: an Intermediate Language for Deductive Verification of BSP Programs

摘要

We present BSP-Why, a tool for verifying BSP programs. It is intended to be used as an intermediate core-language for verification tools (mainly condition generators) of BSP extensions of realistic programming languages such as C, Java, etc. BSP-Why is based on a sequential simulation of the BSP programs which allows to generate pure sequential codes for the back-end condition generator Why and thus benefit of its large range of existing provers — proof assistants or automatic decision procedures. In this manner, BSP-Why is able to generate proof obligations for BSP programs.Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F. 1.2 [Computation by Abstract Devices]: Modes of Computation, Parallelism and concurrencyGeneral Terms Languages, Verification