@inproceedings(DBLP:conf/icfp/Augustsson98,
 author       = {Lennart Augustsson},
 year         = {1998},
 title        = {Cayenne - a Language with Dependent Types},
 editor       = {Matthias Felleisen and Paul Hudak and Christian Queinnec},
 booktitle    = {ICFP},
 publisher    = {ACM},
 pages        = {239--250},
 url          = {http://doi.acm.org/10.1145/289423.289451},
)
@inproceedings(DBLP:conf/cav/BarrettCDHJKRT11,
 author       = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1\_14},
)
@article(Burdy05,
 author       = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joseph R. Kiniry and Gary T. Leavens and K. Rustan Leino and Erik Poll},
 year         = {2005},
 title        = {An overview of {JML} tools and applications},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {7},
 number       = {3},
 pages        = {212--232},
 doi          = {10.1007/s10009-004-0167-4},
)
@inproceedings(Chalin05,
 author       = {Patrice Chalin and Joseph R. Kiniry and Gary T. Leavens and Erik Poll},
 year         = {2005},
 title        = {Beyond Assertions: Advanced Specification and Verification with {JML} and {ESC}/Java2},
 booktitle    = {FMCO},
 series       = {Lecture Notes in Computer Science},
 volume       = {4111},
 publisher    = {Springer},
 pages        = {342--363},
 doi          = {10.1007/11804192\_16},
)
@inproceedings(DBLP:conf/cav/GrafS97,
 author       = {Susanne Graf and Sa\"{\i}di, Hassen},
 year         = {1997},
 title        = {Construction of Abstract State Graphs with PVS},
 editor       = {Orna Grumberg},
 booktitle    = {CAV},
 series       = {Lecture Notes in Computer Science},
 volume       = {1254},
 publisher    = {Springer},
 pages        = {72--83},
 doi          = {10.1007/3-540-63166-6\_10},
)
@inproceedings(DBLP:conf/fp/HallHPJW92,
 author       = {Cordelia V. Hall and Kevin Hammond and Will Partain and Simon L. Peyton Jones and Philip Wadler},
 year         = {1992},
 title        = {The Glasgow Haskell Compiler: {A} Retrospective},
 editor       = {John Launchbury and Patrick M. Sansom},
 booktitle    = {Functional Programming, Glasgow 1992, Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, 6-8 July 1992},
 series       = {Workshops in Computing},
 publisher    = {Springer},
 pages        = {62--71},
)
@proceedings(DBLP:conf/pldi/2009,
 editor       = {Michael Hind and Amer Diwan},
 year         = {2009},
 title        = {Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009},
 publisher    = {ACM},
)
@article(Hoa.69,
 author       = {C. A. R. Hoare},
 year         = {1969},
 title        = {An {A}xiomatic {B}asis for {C}omputer {P}rogramming},
 journal      = {Comm. ACM},
 volume       = {12},
 number       = {10},
 pages        = {89--100},
 doi          = {10.1145/363235.363259},
)
@book(HSM.97,
 author       = {E. Horowitz and S. Sahni and D. Mehta},
 year         = {1997},
 title        = {Fundamentals of Data Structures in C++},
 edition      = {4th},
 publisher    = {Computer Science Press},
)
@inproceedings(DBLP:conf/pldi/KawaguchiRJ09,
 author       = {Ming Kawaguchi and Patrick Maxim Rondon and Ranjit Jhala},
 year         = {2009},
 title        = {Type-based data structure verification},
 editor       = {Hind and Diwan},
 pages        = {304--315},
 doi          = {10.1145/1542476.1542510},
)
@inproceedings(DBLP:conf/tacas/MouraB08,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 editor       = {C. R. Ramakrishnan and Jakob Rehof},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@book(Pen.05,
 author       = {Pe{\~n}a, R.},
 year         = {2005},
 title        = {Dise{\~n}o de Programas: Formalismo y Abstracci\'on},
 publisher    = {Tercera edici\'on. Pearson Prentice-Hall},
)
@inproceedings(DBLP:conf/cav/RondonBKJ12,
 author       = {Patrick Maxim Rondon and Alexander Bakst and Ming Kawaguchi and Ranjit Jhala},
 year         = {2012},
 title        = {CSolve: Verifying C with Liquid Types},
 editor       = {P. Madhusudan and Sanjit A. Seshia},
 booktitle    = {CAV},
 series       = {Lecture Notes in Computer Science},
 volume       = {7358},
 publisher    = {Springer},
 pages        = {744--750},
 url          = {http://dx.doi.org/10.1007/978-3-642-31424-7\_59},
)
@inproceedings(DBLP:conf/pldi/RondonKJ08,
 author       = {Patrick Maxim Rondon and Ming Kawaguchi and Ranjit Jhala},
 year         = {2008},
 title        = {Liquid types},
 editor       = {Rajiv Gupta and Saman P. Amarasinghe},
 booktitle    = {PLDI},
 publisher    = {ACM},
 pages        = {159--169},
 doi          = {10.1145/1375581.1375602},
)
@inproceedings(DBLP:conf/pldi/SrivastavaG09,
 author       = {Saurabh Srivastava and Sumit Gulwani},
 year         = {2009},
 title        = {Program verification using templates over predicate abstraction},
 editor       = {Hind and Diwan},
 pages        = {223--234},
 doi          = {10.1145/1542476.1542501},
)
@inproceedings(Turing49,
 author       = {A. M. Turing},
 year         = {1949},
 title        = {{Checking a Large Routine}},
 booktitle    = {Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge},
 pages        = {67--69},
)
@inproceedings(DBLP:conf/haskell/VazouSJ14,
 author       = {Niki Vazou and Eric L. Seidel and Ranjit Jhala},
 year         = {2014},
 title        = {LiquidHaskell: experience with refinement types in the real world},
 editor       = {Wouter Swierstra},
 booktitle    = {Proceedings of the 2014 {ACM} {SIGPLAN} symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014},
 publisher    = {{ACM}},
 pages        = {39--51},
 doi          = {10.1145/2633357.2633366},
)
@inproceedings(DBLP:conf/icfp/VazouSJVJ14,
 author       = {Niki Vazou and Eric L. Seidel and Ranjit Jhala and Dimitrios Vytiniotis and Simon L. Peyton Jones},
 year         = {2014},
 title        = {Refinement types for Haskell},
 editor       = {Johan Jeuring and Manuel M. T. Chakravarty},
 booktitle    = {Proceedings of the 19th {ACM} {SIGPLAN} international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014},
 publisher    = {{ACM}},
 pages        = {269--282},
 doi          = {10.1145/2628136.2628161},
)