Towards Automation for Pointer Algebra

erschienen 2011 in H. de Swart (eds.): Relational and Algebraic Methods in Computer Science PhD Programme (RAMiCS 12), 2011.

Abstract: First-order automated verification within algebraic structures has proven to be widely applicable. In this work we deal with automation for pointer algebra. We evaluate the adequacy of its original axioms for theorem proving tools. Moreover we give a different algebraic approach for projections which turns out to be more suitable for automation.