Sigma*: Symbolic Learning of Input-Output Specifications (CROSBI ID 603341)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Botinčan, Matko ; Babić, Domagoj
engleski
Sigma*: Symbolic Learning of Input-Output Specifications
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.
Inductive learning ; Specification synthesis ; Behavioral properties ; Equivalence checking ; Stream programs ; Compiler optimization ; Parallelization
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
443-456.
2012.
objavljeno
Podaci o matičnoj publikaciji
Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), 2013
Gicobazzi, Roberto ; Cousot Radhia
New York (NY): The Association for Computing Machinery (ACM)
978-1-4503-1832-7
Podaci o skupu
Nepoznat skup
predavanje
29.02.1904-29.02.2096