Quantified Data Automata for SkinnyTrees: 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 nontrivial complex properties over arrays and lists. Secondly, quantified data automata are learnable efficiently. We show that using the quantified data automata we can passivelylearn universally quantified invariants over arrays and lists very efficiently, from a set of examples and counterexamples. These two techniques using quantified data automata present two orthrogonal ways of inferring universally quantified invariants over linear heap structures. Additionally, we discover a subclass 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.
20th Static Analysis Symposium (SAS), 2013. 25th Int'l Conf. on Computer Aided Verification (CAV), 2013. Experimental ResultsResults 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 counterexamples can be accessed here. 

Last Updated: Apr 25 2013. 