Quantified Data Automata for Skinny-Trees: an Abstract Domain for Lists


Quantified Data Automata is an automaton model for expressing universally quantified properties over arrays and lists, for eg. sortedness of arrays.

This automata model has several desirable properties. First, the quantified data automaton form a highly expressive and a very powerful abstract domain which we show can prove non-trivial complex properties over arrays and lists. Secondly, quantified data automata are learnable efficiently. We show that using the quantified data automata we can passively-learn universally quantified invariants over arrays and lists very efficiently, from a set of examples and counter-examples. These two techniques using quantified data automata present two orthrogonal ways of inferring universally quantified invariants over linear heap structures.

Additionally, we discover a sub-class of quantified data automata called elastic QDAs which capture formulas in decidable logics --- decidable fragment of Strand over lists and the decidable array property fragment over arrays. Hence, the quantified data automata not only present ways to learn the universally quantified invariants, but also ensure that the invariants thus learned can be used for verification using satisfiability modulo decidable theories (SMT).

Please see the following papers for the technical details.

  • Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists. PDF
    • Pranav Garg, P. Madhusudan and Gennaro Parlato
    20th Static Analysis Symposium (SAS), 2013.

  • Learning Universally Quantified Invariants of Linear Data Structures. PDF, arXiv
    • Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider
    25th Int'l Conf. on Computer Aided Verification (CAV), 2013.


Experimental Results

Results evaluating the abstract domain over quantified data automata can be accessed here. The VirtualBox VM desktop with all the experimental results can be found here. Results on using QDAs to learn invariants from examples and counter-examples can be accessed here.

Back to Homepage

Last Updated: Apr 25 2013.