11 citations · 24 across the 4 of their papers we have counts for
4 papers
Smtlink 2.0
Yan Peng, Mark R. Greenstreet
Smtlink is an extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers. We presented an earlier version at ACL2'2015. Smtlink 2.0 makes major improvements over the initi…
Convex Functions in ACL2(r)
Carl Kwan, Mark R. Greenstreet
This paper builds upon our prior formalisation of R^n in ACL2(r) by presenting a set of theorems for reasoning about convex functions. This is a demonstration of the higher-dimensi…
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)
Carl Kwan, Mark R. Greenstreet
We present a mechanical proof of the Cauchy-Schwarz inequality in ACL2(r) and a formalisation of the necessary mathematics to undertake such a proof. This includes the formalisatio…
Extending ACL2 with SMT Solvers
Yan Peng, Mark Greenstreet
We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using ACL2's trusted clause processor mechanism. We are particularly interested in the verificati…