@inproceedings(DBLP:conf/fmco/BarnettCDJL05,
 author       = {Michael Barnett and Bor{-}Yuh Evan Chang and Robert DeLine and Bart Jacobs and K. Rustan M. Leino},
 year         = {2005},
 title        = {Boogie: {A} Modular Reusable Verifier for Object-Oriented Programs},
 editor       = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever},
 booktitle    = {Formal Methods for Components and Objects, 4th International Symposium, {FMCO} 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures},
 series       = {Lecture Notes in Computer Science},
 volume       = {4111},
 publisher    = {Springer},
 pages        = {364--387},
 doi          = {10.1007/11804192\_17},
)
@article(barrett2010smt,
 author       = {Clark Barrett and Aaron Stump and Cesare Tinelli},
 year         = {2010},
 title        = {The {SMT-LIB} Standard Version 2.0},
 journal      = {SMT-LIB.org},
 url          = {http://SMT-LIB.org},
)
@inproceedings(bendisposto2014prob,
 author       = {Jens Bendisposto and Sebastian Krings and Michael Leuschel},
 year         = {2014},
 title        = {Who watches the watchers: Validating the ProB Validation Tool},
 editor       = {Dubois},
 pages        = {16--29},
 doi          = {10.4204/EPTCS.149.3},
)
@inproceedings(chalin2008jml4,
 author       = {Patrice Chalin and Perry R. James and George Karabotsos},
 year         = {2008},
 title        = {{JML4:} Towards an Industrial Grade {IVE} for Java and Next Generation Research Platform for {JML}},
 editor       = {Natarajan Shankar and Jim Woodcock},
 booktitle    = {Verified Software: Theories, Tools, Experiments, Second International Conference, {VSTTE} 2008, Toronto, Canada, October 6-9, 2008. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5295},
 publisher    = {Springer},
 pages        = {70--83},
 doi          = {10.1007/978-3-540-87873-5\_9},
)
@inproceedings(cok2014openjml,
 author       = {David R. Cok},
 year         = {2014},
 title        = {OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse},
 editor       = {Dubois},
 pages        = {79--92},
 doi          = {10.4204/EPTCS.149.8},
)
@inproceedings(cok2014speedy,
 author       = {David R. Cok and Scott C. Johnson},
 year         = {2014},
 title        = {{SPEEDY:} An Eclipse-based {IDE} for invariant inference},
 editor       = {Dubois},
 pages        = {44--57},
 doi          = {10.4204/EPTCS.149.5},
)
@inproceedings(cook:2013,
 author       = {Charles T. Cook and Drachova{-}Strang, Svetlana and Yu{-}Shan Sun and Murali Sitaraman and Jeffrey C. Carver and Joseph E. Hollingsworth},
 year         = {2013},
 title        = {Specification and reasoning in {SE} projects using a Web {IDE}},
 editor       = {Tony Cowling and Shawn Bohner and Mark A. Ardis},
 booktitle    = {26th International Conference on Software Engineering Education and Training, CSEE{\&}T 2013, San Francisco, CA, USA, May 19-21, 2013},
 publisher    = {{IEEE}},
 pages        = {229--238},
 doi          = {10.1109/CSEET.2013.6595254},
)
@inproceedings(cook2012specification,
 author       = {Charles T. Cook and Heather K. Harton and Hampton Smith and Murali Sitaraman},
 year         = {2012},
 title        = {Specification engineering and modular verification using a web-integrated verifying compiler},
 editor       = {Martin Glinz and Gail C. Murphy and Mauro Pezz{\`{e}}},
 booktitle    = {34th International Conference on Software Engineering, {ICSE} 2012, June 2-9, 2012, Zurich, Switzerland},
 publisher    = {{IEEE}},
 pages        = {1379--1382},
 doi          = {10.1109/ICSE.2012.6227243},
)
@article(cook:2014,
 author       = {Charles T. Cook and Yu{-}Shan Sun and Murali Sitaraman},
 year         = {2015},
 title        = {Experience report: evolution of a web-integrated software development and verification environment},
 journal      = {Softw., Pract. Exper.},
 volume       = {45},
 number       = {6},
 pages        = {857--872},
 doi          = {10.1002/spe.2259},
)
@article(Simplify,
 author       = {David Detlefs and Greg Nelson and James B. Saxe},
 year         = {2005},
 title        = {Simplify: a theorem prover for program checking},
 journal      = {J. {ACM}},
 volume       = {52},
 number       = {3},
 pages        = {365--473},
 doi          = {10.1145/1066100.1066102},
)
@phdthesis(drachova:2013,
 author       = {Drachova-Strang, Svetlana},
 year         = {2013},
 title        = {Teaching and Assessment of Mathematical Principles for Software Correctness Using a Reasoning Concept Inventory},
 school       = {Clemson University},
 url          = {http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Drachova-Strang.pdf},
)
@article(drachova:2015,
 author       = {Drachova-Strang, Svetlana and Jason Hallstrom and Murali Sitaraman and Joe Hollingsworth and Joan Krone},
 year         = {2015},
 title        = {Teaching Mathematical Reasoning Principles for Software Correctness and its Assessment},
 journal      = {ACM Transactions on Computing Education},
 pages        = {accepted, to appear},
)
@proceedings(DBLP:journals/corr/DuboisGM14,
 editor       = {Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
 year         = {2014},
 title        = {Proceedings 1st Workshop on Formal Integrated Development Environment, {F-IDE} 2014, Grenoble, France, April 6, 2014},
 series       = {{EPTCS}},
 volume       = {149},
 doi          = {10.4204/EPTCS.149},
)
@inproceedings(furiaeptcs,
 author       = {Carlo A. Furia and Julian Tschannen and Bertrand Meyer},
 year         = {2014},
 title        = {The {G}otthard Approach: Designing an Integrated Verification Environment for {E}iffel},
 editor       = {Dubois},
 pages        = {1--2},
 doi          = {10.4204/EPTCS.149},
 note         = {Abstract of invited talk},
)
@phdthesis(harton:2011,
 author       = {Heather Harton},
 year         = {2011},
 title        = {Mechanical and Modular Verification Condition Generation For Object-Based Software},
 school       = {Clemson University},
 url          = {http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Harton_2_1.pdf},
)
@article(hatcliff2012behavioral,
 author       = {John Hatcliff and Gary T. Leavens and K. Rustan M. Leino and Peter M{\"{u}}ller and Matthew J. Parkinson},
 year         = {2012},
 title        = {Behavioral interface specification languages},
 journal      = {{ACM} Comput. Surv.},
 volume       = {44},
 number       = {3},
 pages        = {16},
 doi          = {10.1145/2187671.2187678},
)
@inproceedings(jacobs2011verifast,
 author       = {Bart Jacobs and Jan Smans and Pieter Philippaerts and Fr{\'{e}}d{\'{e}}ric Vogels and Willem Penninckx and Frank Piessens},
 year         = {2011},
 title        = {VeriFast: {A} Powerful, Sound, Predictable, Fast Verifier for {C} and Java},
 editor       = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
 booktitle    = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6617},
 publisher    = {Springer},
 pages        = {41--55},
 doi          = {10.1007/978-3-642-20398-5\_4},
)
@inproceedings(jaume2014teaching,
 author       = {Mathieu Jaume and Th{\'{e}}o Laurent},
 year         = {2014},
 title        = {Teaching Formal Methods and Discrete Mathematics},
 editor       = {Dubois},
 pages        = {30--43},
 doi          = {10.4204/EPTCS.149.4},
)
@inproceedings(kirschenbaum:2009,
 author       = {Jason Kirschenbaum and Bruce M. Adcock},
 year         = {2009},
 title        = {Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?},
 editor       = {Stephen H. Edwards and Gregory Kulczycki},
 booktitle    = {Formal Foundations of Reuse and Domain Engineering, 11th International Conference on Software Reuse, {ICSR} 2009, Falls Church, VA, USA, September 27-30, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5791},
 publisher    = {Springer},
 pages        = {31--40},
 doi          = {10.1007/978-3-642-04211-9\_4},
)
@inproceedings(kulczycki:icsr2013,
 author       = {Gregory Kulczycki and Murali Sitaraman},
 year         = {2013},
 title        = {A Language for Building Verified Software Components},
 editor       = {John M. Favaro and Maurizio Morisio},
 booktitle    = {Safe and Secure Software Reuse - 13th International Conference on Software Reuse, {ICSR} 2013, Pisa, Italy, June 18-20. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7925},
 publisher    = {Springer},
 pages        = {308--314},
 doi          = {10.1007/978-3-642-38977-1\_23},
)
@phdthesis(kulczycki:2004,
 author       = {Gregory W. Kulczycki},
 year         = {2004},
 title        = {Direct Reasoning},
 school       = {Clemson University},
 url          = {http://www.nvc.vt.edu/gregwk/assets/research-papers/kulczycki04direct.pdf},
)
@article(leavens2006preliminary,
 author       = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
 year         = {2006},
 title        = {Preliminary design of {JML:} a behavioral interface specification language for java},
 journal      = {{ACM} {SIGSOFT} Software Engineering Notes},
 volume       = {31},
 number       = {3},
 pages        = {1--38},
 doi          = {10.1145/1127878.1127884},
)
@inproceedings(leino2010dafny,
 author       = {K. Rustan M. Leino},
 year         = {2010},
 title        = {Dafny: An Automatic Program Verifier for Functional Correctness},
 editor       = {Edmund M. Clarke and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {6355},
 publisher    = {Springer},
 pages        = {348--370},
 doi          = {10.1007/978-3-642-17511-4\_20},
)
@inproceedings(leino2014dafny,
 author       = {K. Rustan M. Leino and Valentin W{\"{u}}stholz},
 year         = {2014},
 title        = {The Dafny Integrated Development Environment},
 editor       = {Dubois},
 pages        = {3--15},
 doi          = {10.4204/EPTCS.149.2},
)
@article(EiffelRef,
 author       = {Bertrand Meyer},
 year         = {1988},
 title        = {Eiffel: {A} language and environment for software engineering},
 journal      = {Journal of Systems and Software},
 volume       = {8},
 number       = {3},
 pages        = {199--246},
 doi          = {10.1016/0164-1212(88)90022-2},
)
@book(meyer:1997,
 author       = {Bertrand Meyer},
 year         = {1997},
 title        = {Object-Oriented Software Construction, 2nd Edition},
 publisher    = {Prentice-Hall},
)
@inproceedings(de2008z3,
 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},
)
@article(Fast,
 author       = {Greg Nelson and Derek C. Oppen},
 year         = {1980},
 title        = {Fast Decision Procedures Based on Congruence Closure},
 journal      = {J. {ACM}},
 volume       = {27},
 number       = {2},
 pages        = {356--364},
 doi          = {10.1145/322186.322198},
)
@book(nipkow2002isabelle,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(pessaux2014focalize,
 author       = {Fran{\c{c}}ois Pessaux},
 year         = {2014},
 title        = {FoCaLiZe: Inside an {F-IDE}},
 editor       = {Dubois},
 pages        = {64--78},
 doi          = {10.4204/EPTCS.149.7},
)
@article(sitaraman:2011,
 author       = {Murali Sitaraman and Bruce M. Adcock},
 year         = {2011},
 title        = {Building a push-button {RESOLVE} verifier: Progress and challenges},
 journal      = {Formal Asp. Comput.},
 volume       = {23},
 number       = {5},
 pages        = {607--626},
 doi          = {10.1007/s00165-010-0154-3},
)
@article(sitaraman:1994,
 author       = {Murali Sitaraman and Bruce Weide},
 year         = {1994},
 title        = {Component-based Software Using {RESOLVE}},
 journal      = {SIGSOFT Software Engineering Notes},
 volume       = {19},
 number       = {4},
 pages        = {21--22},
 doi          = {10.1145/190679.199221},
)
@incollection(smans2013verifast,
 author       = {Jan Smans and Bart Jacobs and Frank Piessens},
 year         = {2013},
 title        = {VeriFast for Java: {A} Tutorial},
 editor       = {Dave Clarke and James Noble and Tobias Wrigstad},
 booktitle    = {Aliasing in Object-Oriented Programming. Types, Analysis and Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {7850},
 publisher    = {Springer},
 pages        = {407--442},
 doi          = {10.1007/978-3-642-36946-9\_14},
)
@phdthesis(smith:2013,
 author       = {Hampton Smith},
 year         = {2013},
 title        = {Engineering Specifications and Mathematics for Verified Software},
 school       = {Clemson University},
 url          = {http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Smith.pdf},
)
@article(DBLP:journals/corr/abs-1106-4700,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
 year         = {2011},
 title        = {Verifying Eiffel Programs with Boogie},
 journal      = {CoRR},
 volume       = {abs/1106.4700},
 url          = {http://arxiv.org/abs/1106.4700},
)
@inproceedings(welch:2014,
 author       = {Daniel Welch and Charles T. Cook and Yu{-}Shan Sun and Murali Sitaraman},
 year         = {2014},
 title        = {A web-integrated verifying compiler for {RESOLVE:} a research perspective},
 editor       = {Dharanipragada Janakiram and Koushik Sen and Vinay Kulkarni},
 booktitle    = {7th India Software Engineering Conference, Chennai, {ISEC} '14, Chennai, India - February 19 - 21, 2014},
 publisher    = {{ACM}},
 pages        = {12:1--12:6},
 doi          = {10.1145/2590748.2590760},
)
@inproceedings(witulski2014prob,
 author       = {John Witulski and Michael Leuschel},
 year         = {2014},
 title        = {Checking Computations of Formal Method Tools - {A} Secondary Toolchain for ProB},
 editor       = {Dubois},
 pages        = {93--105},
 doi          = {10.4204/EPTCS.149.9},
)