Sigma*: Symbolic Learning of Input-Output Specifications
[PDF]
[PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{bb13sigma,
author = {Matko Botin\v{c}an and Domagoj Babi\'c},
title = {{Sigma*: Symbolic Learning of Input-Output Specifications}},
booktitle = {POPL'13: Proceedings of the 40th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages},
year = {2013},
publisher = {ACM},
address = {New York, NY, USA},
location = {Rome, Italy},
pages = {443--456},
}
Abstract:
We present Sigma*, a novel technique for learning symbolic models
of software behavior. Sigma* addresses the challenge of synthesizing
models of software by using symbolic conjectures and abstraction.
By combining dynamic symbolic execution to discover
symbolic input-output steps of the programs and counterexample
guided abstraction refinement to over-approximate program
behavior, Sigma* transforms arbitrary source representation of
programs into faithful input-output models. We define a class of
stream filters—programs that process streams of data items—for
which Sigma* converges to a complete model if abstraction refinement
eventually builds up a sufficiently strong abstraction. In other
words, Sigma* is complete relative to abstraction. To represent inferred
symbolic models, we use a variant of symbolic transducers
that can be effectively composed and equivalence checked. Thus,
Sigma* enables fully automatic analysis of behavioral properties
such as commutativity, reversibility and idempotence, which is
useful for web sanitizer verification and stream programs compiler
optimizations, as we show experimentally.We also show how models
inferred by Sigma* can boost performance of stream programs
by parallelized code generation.