Title: Symbolic object code analysis
Authors: Mühlberg, Jan Tobias ×
Gerald, Lüttgen #
Issue Date: Feb-2014
Publisher: Springer
Series Title: International Journal on Software Tools for Technology Transfer vol:16 issue:1 pages:81-102
Abstract: Software model checkers quickly reach their limits when being
applied to verifying pointer safety properties in source code that
includes function pointers and inlined assembly. This article
introduces a novel technique for checking pointer safety violations,
called Symbolic Object Code Analysis (SOCA), which is based
on bounded symbolic execution, incorporates path-sensitive
slicing, and employs the SMT solver Yices as its execution and
verification engine. Extensive experimental results of a prototypic
SOCA Verifier, using the Verisec suite and almost 10,000 Linux
device driver functions as benchmarks, show that SOCA performs
competitively to modern source-code model checkers, scales well when
applied to real operating systems code and pointer safety issues,
and effectively explores niches of pointer-complex software that
current software verifiers do not reach.
ISSN: 1433-2779
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
soca-sttt-2012.pdf Accepted 1426KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science