Model checking pointer safety in compiled programs
This thesis introduces a novel technique for the automated analysis of compiled programs, which is focused on, but not restricted to, pointer safety properties. Our approach, which we refer to as Symbolic Object Code Analysis (SOCA), employs bounded symbolic execution, and uses an SMT solver as exec...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
University of York
2009
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.516419 |