String Analysis as an Abstract Interpretation

Abstract

I will present a string analysis designed within abstract interpretation framework. To this end, I introduce novel predicates which are derived from the reference pushdown automaton. Using these predicates, we can design a conjunctive domain whose element is a conjunction of the predicates. We can establish the correctness relation by Galois connection and define correct abstract concatenation operation on the domain. I also present a family of pushdown automata called epsilon bounded pushdown automata. This family covers all context-free languages. By using this family of pushdown automata, we can prevent abstract values from becoming infinite conjunctions and guarantee that all the operations required in the analyzer are computable. Using our string analyzer designed in abstract interpretation framework, we can easily compose the string analysis with other analyses to improve the precision, and it is also possible to design modular string analyzer.

Short bio