TR-IIS-07-002    Fulltext

Soundness of compositional reasoning rules depends on computational models and sometimes is rather involved. Since it is tedious to establish new rules, verifiers are forced to mould verification problems into a handful of proof rules available to them. In this paper, a syntactic approach to establishing soundness of proof rules in automated compositional reasoning is shown. Not only can our work justify all proof rules known to us automatically, but also derive new circular rules by intuitionistic reasoning without human intervention. Practitioners can now develop their own rules in automated compositional reasoning through learning rather easily.