Detail publikace

Flatten and conquer: a framework for efficient analysis of string constraints

HOLÍK, L. ABDULLA, P. ATIG, M. BUI PHI, D. CHEN, Y. REZINE, A. RUMMER, P.

Originální název

Flatten and conquer: a framework for efficient analysis of string constraints

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

Klíčová slova

Automata Theory, Formal Verification, String Equation

Autoři

HOLÍK, L.; ABDULLA, P.; ATIG, M.; BUI PHI, D.; CHEN, Y.; REZINE, A.; RUMMER, P.

Vydáno

18. 6. 2017

Nakladatel

Association for Computing Machinery

Místo

New York

ISBN

978-1-4503-4988-8

Kniha

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

Edice

ACM

Strany od

602

Strany do

617

Strany počet

16

URL

https://dl.acm.org/citation.cfm?doid=3062341.3062384

BibTex

@inproceedings{BUT146274,
  author="Lukáš {Holík} and Parosh {Abdulla} and Mohamed {Atig} and Diep {Bui Phi} and Yu-Fang {Chen} and Ahmed {Rezine} and Philipp {Rummer}",
  title="Flatten and conquer: a framework for efficient analysis of string constraints",
  booktitle="Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation",
  year="2017",
  series="ACM",
  pages="602--617",
  publisher="Association for Computing Machinery",
  address="New York",
  doi="10.1145/3062341.3062384",
  isbn="978-1-4503-4988-8",
  url="https://dl.acm.org/citation.cfm?doid=3062341.3062384"
}

Dokumenty

pldi17-main300.pdf