ProverPSL: A Theorem Prover for Full Separation Logic

Abstract

This report presents a theorem prover for automated verification of program specifications written in separation logic. Our prover supports all new connectives in separation logic including separating conjunction and separating implication. To assist the prover, we integrate a high efficient SMT solver to process arithmetic expression relations, and also present a method to apply inference rules with associativity property.