Sciweavers

TAP
2010
Springer

Testing First-Order Logic Axioms in Program Verification

13 years 1 months ago
Testing First-Order Logic Axioms in Program Verification
Program verification systems based on automated theorem provers rely on user-provided axioms in order to verify domain-specific properties of code. However, formulating axioms correctly (that is, formalizing properties of an intended mathematical interpretation) is nontrivial in practice, and avoiding or even detecting unsoundness can sometimes be difficult to achieve. Moreover, speculating soundness of axioms based on the output of the provers themselves is not easy since they do not typically give counterexamples. We adopt the idea of model-based testing to aid axiom authors in discovering errors in axiomatizations. To test the validity of axioms, users define a computational model of the axiomatized logic by giving interpretations to the function symbols and constants in a simple declarative programming language. We have developed an axiom testing framework that helps automate model definition and test generation using off-the-shelf tools for meta-programming, property-based random ...
Ki Yung Ahn, Ewen Denney
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where TAP
Authors Ki Yung Ahn, Ewen Denney
Comments (0)