Proof logging for computer algebra based SMT solving. - Oliver Marx; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Alexander Dreyer (ICCAD, 2013)

A computer-algebraic approach to formal verification of data-centric low-level software. - Oliver Marx; Carlos Villarraga; Dominik Stoffel; Wolfgang Kunz (MEMOCODE, 2016)