Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 658582

Sigma*: Symbolic Learning of Input-Output Specifications


Botinčan, Matko; Babić, Domagoj
Sigma*: Symbolic Learning of Input-Output Specifications // Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), 2013 / Gicobazzi, Roberto ; Cousot Radhia (ur.).
New York, USA: ACM, 2012. str. 443-456 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 658582 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

Naslov
Sigma*: Symbolic Learning of Input-Output Specifications

Autori
Botinčan, Matko ; Babić, Domagoj

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), 2013 / Gicobazzi, Roberto ; Cousot Radhia - New York, USA : ACM, 2012, 443-456

ISBN
978-1-4503-1832-7

Skup
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Rome, Italy — January 23 - 25, 2013.

Mjesto i datum
Rim, Italija, 23-25-01.2013

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Inductive learning; Specification synthesis; Behavioral properties; Equivalence checking; Stream programs; Compiler optimization; Parallelization

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo



POVEZANOST RADA


Projekti:
037-0362980-2774 - Distribuirani algoritmi za pronalaženje optimalnih putova u grafovima (Manger, Robert, MZOS ) ( CroRIS)

Ustanove:
Prirodoslovno-matematički fakultet, Matematički odjel, Zagreb

Profili:

Avatar Url Domagoj Babić (autor)

Avatar Url Matko Botinčan (autor)


Citiraj ovu publikaciju:

Botinčan, Matko; Babić, Domagoj
Sigma*: Symbolic Learning of Input-Output Specifications // Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), 2013 / Gicobazzi, Roberto ; Cousot Radhia (ur.).
New York, USA: ACM, 2012. str. 443-456 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Botinčan, M. & Babić, D. (2012) Sigma*: Symbolic Learning of Input-Output Specifications. U: Gicobazzi, R. & Cousot Radhia (ur.)Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), 2013.
@article{article, author = {Botin\v{c}an, Matko and Babi\'{c}, Domagoj}, editor = {Gicobazzi, R. and Cousot Radhia}, year = {2012}, pages = {443-456}, keywords = {Inductive learning, Specification synthesis, Behavioral properties, Equivalence checking, Stream programs, Compiler optimization, Parallelization}, isbn = {978-1-4503-1832-7}, title = {Sigma\ast: Symbolic Learning of Input-Output Specifications}, keyword = {Inductive learning, Specification synthesis, Behavioral properties, Equivalence checking, Stream programs, Compiler optimization, Parallelization}, publisher = {ACM}, publisherplace = {Rim, Italija} }
@article{article, author = {Botin\v{c}an, Matko and Babi\'{c}, Domagoj}, editor = {Gicobazzi, R. and Cousot Radhia}, year = {2012}, pages = {443-456}, keywords = {Inductive learning, Specification synthesis, Behavioral properties, Equivalence checking, Stream programs, Compiler optimization, Parallelization}, isbn = {978-1-4503-1832-7}, title = {Sigma\ast: Symbolic Learning of Input-Output Specifications}, keyword = {Inductive learning, Specification synthesis, Behavioral properties, Equivalence checking, Stream programs, Compiler optimization, Parallelization}, publisher = {ACM}, publisherplace = {Rim, Italija} }




Contrast
Increase Font
Decrease Font
Dyslexic Font