A. Arusoaie, Engineering Hoare Logic-Based Program Verification in K Framework, 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013.
DOI : 10.1109/SYNASC.2013.31

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Framework for Symbolic Execution, 6th International Conference on Software Language Engineering, pp.281-301, 2013.
DOI : 10.1007/978-3-319-02654-1_16
URL : https://hal.archives-ouvertes.fr/hal-00853588

S. ¸tefan-ciobâc?-a, D. Lucanu, V. Rusu, and G. Ro¸suro¸su, A Language-Independent Proof System for Mutual Program Equivalence (revisited), 2014.

G. Ro¸suro¸su and A. Stefanescu, Checking reachability using matching logic, OOPSLA, pp.555-574, 2012.

G. Rosu, A. Stefanescu, and B. M. Moore, One-Path Reachability Logic, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.358-367, 2013.
DOI : 10.1109/LICS.2013.42