@inproceedings{kovacs:2009:fli,
 author = {Kov\'acs, Laura and Voronkov, Andrei},
 title = {Finding Loop Invariants for Programs over Arrays Using a Theorem Prover},
 booktitle = {Proceedings of the 2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
 series = {SYNASC '09},
 year = {2009},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}

@inproceedings{gulwani:2008:popl,
 author = {Gulwani, Sumit and McCloskey, Bill and Tiwari, Ashish},
 title = {Lifting abstract interpreters to quantified logical domains},
 booktitle = {Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '08},
 year = {2008},
 isbn = {978-1-59593-689-9},
 location = {San Francisco, California, USA},
 pages = {235--246},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1328438.1328468},
 doi = {http://doi.acm.org/10.1145/1328438.1328468},
 acmid = {1328468},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {abstract interpreter, logical lattices, quantified invariants, underapproximation algorithms},
}

@inproceedings{halbwachs:2008:pldi,
 author = {Halbwachs, Nicolas and P\'{e}ron, Mathias},
 title = {Discovering properties about arrays in simple programs},
 booktitle = {Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation},
 series = {PLDI '08},
 year = {2008},
 isbn = {978-1-59593-860-2},
 location = {Tucson, AZ, USA},
 pages = {339--348},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1375581.1375623},
 doi = {http://doi.acm.org/10.1145/1375581.1375623},
 acmid = {1375623},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {"sentinel", abstract interpretation, arrays, invariant synthesis, program verification, sorting algorithms},
}

@inproceedings{mcmillan:2008:tacas,
 author = {McMillan, K. L.},
 title = {Quantified invariant generation using an interpolating saturation prover},
 booktitle = {Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems},
 series = {TACAS'08/ETAPS'08},
 year = {2008},
 isbn = {3-540-78799-2, 978-3-540-78799-0},
 location = {Budapest, Hungary},
 pages = {413--427},
 numpages = {15},
 url = {http://portal.acm.org/citation.cfm?id=1792734.1792775},
 acmid = {1792775},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{cousot:1978:popl,
 author = {Cousot, Patrick and Halbwachs, Nicolas},
 title = {Automatic discovery of linear restraints among variables of a program},
 booktitle = {Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
 series = {POPL '78},
 year = {1978},
 location = {Tucson, Arizona},
 pages = {84--96},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/512760.512770},
 doi = {http://doi.acm.org/10.1145/512760.512770},
 acmid = {512770},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{mine:2006:hosc,
 author = {Min\'{e}, Antoine},
 title = {The octagon abstract domain},
 journal = {Higher Order Symbol. Comput.},
 volume = {19},
 issue = {1},
 month = {March},
 year = {2006},
 issn = {1388-3690},
 pages = {31--100},
 numpages = {70},
 url = {http://portal.acm.org/citation.cfm?id=1145489.1145526},
 doi = {10.1007/s10990-006-8609-1},
 acmid = {1145526},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {Abstract interpretation, Numerical abstract domains, Relational numerical invariants, Static analysis},
}

@inproceedings{sankaranarayanan:2004:popl,
 author = {Sankaranarayanan, Sriram and Sipma, Henny B. and Manna, Zohar},
 title = {Non-linear loop invariant generation using Gröbner bases},
 booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '04},
 year = {2004},
 isbn = {1-58113-729-X},
 location = {Venice, Italy},
 pages = {318--329},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/964001.964028},
 doi = {http://doi.acm.org/10.1145/964001.964028},
 acmid = {964028},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Gr\"{o}bner bases, constraint programming, ideals, invariant generation, program analysis, symbolic computation, verification},
}

@inproceedings{colon:2003:cav,
  author    = {Michael Col{\'o}n and
               Sriram Sankaranarayanan and
               Henny Sipma},
  title     = {Linear Invariant Generation Using Non-linear Constraint
               Solving},
  booktitle = {CAV},
  year      = {2003},
  pages     = {420-432},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=420},
  crossref  = {DBLP:conf/cav/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2003,
  editor    = {Warren A. Hunt Jr. and
               Fabio Somenzi},
  title     = {Computer Aided Verification, 15th International Conference,
               CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2725},
  year      = {2003},
  isbn      = {3-540-40524-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{graf:1997:cav,
 author = {Graf, Susanne and Sa\"{\i}di, Hassen},
 title = {Construction of Abstract State Graphs with PVS},
 booktitle = {Proceedings of the 9th International Conference on Computer Aided Verification},
 series = {CAV '97},
 year = {1997},
 isbn = {3-540-63166-6},
 pages = {72--83},
 numpages = {12},
 url = {http://portal.acm.org/citation.cfm?id=647766.733618},
 acmid = {733618},
 publisher = {Springer-Verlag},
 address = {London, UK},
}

@inproceedings{mcmillan:2003:cav,
  author    = {Kenneth L. McMillan},
  title     = {Interpolation and SAT-Based Model Checking},
  booktitle = {CAV},
  year      = {2003},
  pages     = {1-13},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=1},
  crossref  = {DBLP:conf/cav/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{mcmillan:2006:cav,
  author    = {Kenneth L. McMillan},
  title     = {Lazy Abstraction with Interpolants},
  booktitle = {CAV},
  year      = {2006},
  pages     = {123-136},
  ee        = {http://dx.doi.org/10.1007/11817963_14},
  crossref  = {DBLP:conf/cav/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2006,
  editor    = {Thomas Ball and
               Robert B. Jones},
  title     = {Computer Aided Verification, 18th International Conference,
               CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4144},
  year      = {2006},
  isbn      = {3-540-37406-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{kovacs:2008:csr,
 author = {Kov\'{a}cs, Laura},
 title = {Invariant generation for P-solvable loops with assignments},
 booktitle = {Proceedings of the 3rd international conference on Computer science: theory and applications},
 series = {CSR'08},
 year = {2008},
 isbn = {3-540-79708-4, 978-3-540-79708-1},
 location = {Moscow, Russia},
 pages = {349--359},
 numpages = {11},
 url = {http://portal.acm.org/citation.cfm?id=1813695.1813734},
 acmid = {1813734},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@misc{sparkskein:url,
 key = {sparkskein},
 note = {\url{http://www.skein-hash.info/SPARKSkein-release}},
}

@inproceedings{Mauborgne:trace-partitioning,
author = {Laurent Mauborgne and Xavier Rival},
title = {Trace Partitioning in Abstract Interpretation Based Static Analyzers},
booktitle = {Proc. ESOP'05},
volume = {3444},
series = {Lecture Notes in Computer Science},
year = {2005},
editor = {M. Sagiv},
pages = {5--20},
}

@inproceedings{Harris:2010:PAV,
 author = {Harris, William R. and Sankaranarayanan, Sriram and Ivan\v{c}i\'{c}, Franjo and Gupta, Aarti},
 title = {Program analysis via satisfiability modulo path programs},
 booktitle = {Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '10},
 year = {2010},
 isbn = {978-1-60558-479-9},
 location = {Madrid, Spain},
 pages = {71--82},
 numpages = {12},
 acmid = {1706309},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{Sharma:2011:cav,
 author = {Rahul Sharma and Isil Dillig and Thomas Dillig and Alex Aiken},
 title = {Simplifying Loop Invariant Generation Using Splitter Predicates},
 booktitle = {Proceedings of the 23rd International Conference on Computer Aided Verification},
 series = {CAV '11},
 year = {2011},
 month = jul,
 location = {Snowbird, UT, USA},
 publisher = {ACM},
 address = {New York, NY, USA},
}


@book{dijkstra(scholten:1990,
  author = {Edsger W. Dijkstra and Carel S. Scholten},
  interhash = {ab7f203610fb09bc81189a8ddb9a5a3e},
  intrahash = {b415fb704a4c87dd8c0d0caeff2da89a},
  publisher = {Springer},
  title = {Predicate calculus and program semantics},
  year = 1990,
  timestamp = {2010-05-10T11:03:40.000+0200},
  keywords = {handbib regal:68},
  added-at = {2010-05-10T11:03:40.000+0200},
  biburl = {http://www.bibsonomy.org/bibtex/2b415fb704a4c87dd8c0d0caeff2da89a/algebradresden}
}

@inproceedings{Gannod:1995:SPS:832303.836920,
 author = {Gannod, G. C. and Cheng, B. H. C.},
 title = {Strongest postcondition semantics as the formal basis for reverse engineering},
 booktitle = {Proceedings of the Second Working Conference on Reverse Engineering},
 series = {WCRE '95},
 year = {1995},
 isbn = {0-8186-7111-4},
 pages = {166--},
 url = {http://portal.acm.org/citation.cfm?id=832303.836920},
 acmid = {836920},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {formal methods, formal specification, geriatric system, higher level abstraction,
imperative program code, legacy system, object-oriented programming, program understanding,
reverse engineering, software development, strongest postcondition predicate transformer,
strongest postcondition semantics, system re-engineering, systems re-engineering},
}