Seminar on Symbolic Execution for Program Reasoning, Friday 1 April, 12-1pm, Theatre 3, ICT building
Bernard Pope
What: Symbolic Execution for Program Reasoning
Who: Andrew Santosa
Where: Theatre 3, ICT Building, The University of Melbourne, 111 Barry Street Carlton
When: 12-1pm, Friday 1 April
Abstract
We present TRACER, a tool for symbolic execution of C programs. The
input C program is annotated with target properties. Instead of
performing a traditional rendition of abstract interpretation where an
abstract domain is defined statically, TRACER employs a synergy of two
methods. The first is to start with a concrete model of the program
but progressively abstracts away details only when these are known to
be irrelevant. The second is an extension to the first, to handle
unbounded loops. The idea is to progressively discover the strongest
loop invariants through a process of loop unrolling.
The underlying C program may also be annotated with target properties
(assertions) and localized abstractions which abstract symbolic states
during symbolic execution. Informally speaking, this means that when a
symbolic trace C is subjected to a localized abstraction F, we
abstract away only the component of C which entails F, and add F as a
conjunct to the result.
TRACER is to allow more elaborate assertions and abstractions. We
will also mention our idea on a proof method for establishing
entailment constructed from recursive predicates. The method is based
on an unfolding algorithm that reduces recursive definitions to a
point where only constraint solving is necessary. The algorithm
executes the proof by a search-based method which automatically
discovers the opportunity of applying induction instead of the user
having to specify some induction schema.
We are developing TRACER to become a software development tool that,
once augmented with a powerful language for expressing recursively
defined abstractions, spans the spectrum from a fully automatic
verifier to a functional verifier.
Biodata
Andrew Santosa obtained his PhD degree from the National University of
Singapore in 2008 under the supervision of Joxan Jaffar. He is
currently a research fellow at the University of Sydney. His area of
interest is software verification and analysis, focusing on applying
constraint logic programming (CLP) technology. He is also generally
interested in software engineering.