The Oprop Verification Tool: Object Propositions in Action
In this Student Research Competition submission we present Oprop, a tool that implements the theory of object propositions. We have recently introduced object propositions as a modular verification technique that combines abstract predicates and fractional permissions. The Oprop tool verifies programs written in a simplified version of Java, augmented with the object propositions specifications. Our tool parses the input files and automatically translates them into the intermediate verification language Boogie, which is verified by the Boogie verifier. We present the details of our implementation, the lessons that we learned and a number of examples that we have verified using the Oprop tool.