Matching logic has been recently proposed as an alternative program verification approach. Unlike Hoare logic, where one defines a language-specific proof system that needs to be proved sound for each language separately, ...

This paper presents a nine-rule *language-independent* proof system that takes an operational semantics as axioms and derives program properties, including ones corresponding to Hoare triples. This eliminates the ...