RSL to Viper Front end

This dataset consists of the prototype verifier and examples accompanying the paper "Automating Deductive Verification for Weak-Memory Programs", published at TACAS 2018.<br><br>Programs running on weak memory models, such as the C11 memory model, present challenges when attempting their verification due to the non-sequentially consistent execution that they permit. Program logics such as Relaxed Separation Logic (RSL), GPS, Fenced Separation Logic (FSL) and FSL++ address some of these challenges, however their existing implementations require significant manual work. <br>This work presents a novel approach to automating deductive verification for weak memory using the aforementioned program logics. Large fractions of RSL, FSL and FSL++ are encoded in Viper, an intermediate verification language, permitting automated verification by existing tools.<br>Here, the prototype verifier is presented as the front-end program <b>RSLFrontend.jar</b>. 13 test cases currently supported by the prototype are provided in the <b>/InputExamples </b>directory and a further 6 currently unsupported examples are provided in the <b>/ExtraViperExamples </b>directory. These can all be run according to the instructions in <b>README.txt.</b>