@phdthesis(adcockphddiss:2010,
 author       = {Bruce Adcock},
 year         = {2010},
 title        = {Working Towards the Verified Software Process},
 type         = {Ph{D} thesis},
 school       = {The Ohio State University},
)
@book(wolfgang:2016,
 author       = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Peter H. Schmitt and Mattias Ulbrich},
 year         = {2016},
 title        = {Deductive Software Verification - The KeY Book - From Theory to Practice},
 series       = {LNCS},
 volume       = {10001},
 publisher    = {Springer},
 address      = {Cham},
 doi          = {10.1007/978-3-319-49812-6},
)
@inproceedings(ameri:2016,
 author       = {Michael Ameri and Carlo A. Furia},
 year         = {2016},
 title        = {Why Just {B}oogie?},
 editor       = {Erika {\'A}brah{\'a}m and Marieke Huisman},
 booktitle    = {IFM 2016},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {79--95},
 doi          = {10.1007/978-3-319-33693-0\_6},
)
@inproceedings(cookcseet: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}},
 booktitle    = {26th International Conference on Software Engineering Education and Training, CSEE{\&}T 2013, San Francisco, CA, USA, May 19-21, 2013},
 pages        = {229--238},
 doi          = {10.1109/CSEET.2013.6595254},
)
@inproceedings(cookicse:2012,
 author       = {Charles T. Cook and Heather Harton and Hampton Smith and Murali Sitaraman},
 year         = {2012},
 title        = {{Specification Engineering and Modular Verification Using a Web-integrated Verifying Compiler}},
 booktitle    = {ICSE},
 publisher    = {ACM},
 pages        = {1379--1382},
 doi          = {10.1109/ICSE.2012.6227243},
)
@inproceedings(cook:2012,
 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    = {ICSE 2012},
 publisher    = {{IEEE} Computer Society},
 pages        = {1379--1382},
 doi          = {10.1109/ICSE.2012.6227243},
)
@inproceedings(fillatre:2013,
 author       = {Jean{-}Christophe Filli{\^{a}}tre and Andrei Paskevich},
 year         = {2013},
 title        = {Why3 - Where Programs Meet Provers},
 editor       = {Matthias Felleisen and Philippa Gardner},
 booktitle    = {{ESOP} 2013},
 series       = {LNCS},
 volume       = {7792},
 publisher    = {Springer},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6_8},
)
@inproceedings(fowler:2021,
 author       = {Megan Fowler and Eileen T. Kraemer and Murali Sitaraman and Joseph E. Hollingsworth},
 year         = {2021},
 title        = {Tool-Aided Loop Invariant Development: Insights into Student Conceptions and Difficulties},
 editor       = {Carsten Schulte and Brett A. Becker and Monica Divitini and Erik Barendsen},
 booktitle    = {{IT}i{CSE} 2021},
 publisher    = {{ACM}},
 pages        = {387--393},
 doi          = {10.1145/3430665.3456351},
)
@inproceedings(fowler:2020,
 author       = {Megan Fowler and Eileen T. Kraemer and Yu{-}Shan Sun and Murali Sitaraman and Jason O. Hallstrom and Joseph E. Hollingsworth},
 year         = {2020},
 title        = {Tool-Aided Assessment of Difficulties in Learning Formal Design-by-Contract Assertions},
 editor       = {J{\"{u}}rgen Mottok},
 booktitle    = {{ECSEE} 2020},
 publisher    = {{ACM}},
 pages        = {52--60},
 doi          = {10.1145/3396802.3396807},
)
@inproceedings(furia:2015,
 author       = {Carlo A. Furia and Christopher M. Poskitt and Julian Tschannen},
 year         = {2015},
 title        = {The {A}uto{P}roof Verifier: Usability by Non-Experts and on Standard Code},
 editor       = {Catherine Dubois and Paolo Masci and Dominique M{\'{e}}ry},
 booktitle    = {F-IDE 2015},
 pages        = {42--55},
 doi          = {10.4204/EPTCS.187.4},
)
@phdthesis(smithphddiss:2013,
 author       = {Smith Hampton},
 year         = {2013},
 title        = {Engineering Specifications and Mathematics for Verified Software},
 type         = {{PhD Dissertation}},
 school       = {Clemson University},
)
@article(harms:1991,
 author       = {Douglas E. Harms and Bruce W. Weide},
 year         = {1991},
 title        = {Copying and Swapping: Influences on the Design of Reusable Software Components},
 journal      = {IEEE Trans. Softw. Eng.},
 volume       = {17},
 number       = {5},
 pages        = {424--435},
 doi          = {10.1109/32.90445},
)
@phdthesis(hartonphddiss:2011,
 author       = {Heather Harton},
 year         = {2011},
 title        = {Mechanical and Modular Verification Condition Generation for Object-Based Software},
 type         = {{PhD Dissertation}},
 school       = {Clemson University},
)
@inproceedings(heym:2017,
 author       = {Wayne D. Heym and Paolo A. G. Sivilotti and Paolo Bucci and Murali Sitaraman and Kevin Plis and Joseph E. Hollingsworth and Joan Krone and Nigamanth Sridhar},
 year         = {2017},
 title        = {Integrating Components, Contracts, and Reasoning in {CS} Curricula with {RESOLVE:} Experiences at Multiple Institutions},
 editor       = {Hironori Washizaki and Nancy Mead},
 booktitle    = {CSEE{\&}T},
 publisher    = {{IEEE}},
 pages        = {202--211},
 doi          = {10.1109/CSEET.2017.40},
)
@inproceedings(kabbani:2015,
 author       = {Nabil M. Kabbani and Daniel Welch and Caleb Priester and Stephen Schaub and Blair Durkee and Yu{-}Shan Sun and Murali Sitaraman},
 year         = {2015},
 title        = {Formal Reasoning Using an Iterative Approach with an Integrated Web {IDE}},
 booktitle    = {{F-IDE} 2015},
 pages        = {56--71},
 doi          = {10.4204/EPTCS.187.5},
)
@inproceedings(kirschenbaum:2009,
 author       = {Jason Kirschenbaum and Bruce M. Adcock and Derek Bronish and Hampton Smith and Heather K. Harton and Murali Sitaraman and Bruce W. Weide},
 year         = {2009},
 title        = {Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?},
 editor       = {Stephen H. Edwards and Gregory Kulczycki},
 booktitle    = {ICSR 2009},
 series       = {LNCS},
 volume       = {5791},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {31--40},
 doi          = {10.1007/978-3-642-04211-9_4},
)
@inproceedings(kraemerecsee:2018,
 author       = {Eileen T. Kraemer and Murali Sitaraman and Joseph E. Hollingsworth},
 year         = {2018},
 title        = {{An Activity-Based Undergraduate Software Engineering Course to Engage Students and Encourage Learning}},
 booktitle    = {Proceedings of the 3rd European Conference of Software Engineering Education, {ECSEE} 2018, Seeon Monastery, Bavaria, Germany, June 14-15, 2018},
 pages        = {18--25},
 doi          = {10.1145/3209087.3209100},
)
@inproceedings(legoues:2011,
 author       = {Le Goues, Claire and K. Rustan M. Leino and Micha{\l} Moskal},
 year         = {2011},
 title        = {The Boogie Verification Debugger (Tool Paper)},
 editor       = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
 booktitle    = {SEFM 2011},
 series       = {LNCS},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {407--414},
 doi          = {10.1007/978-3-642-24690-6_28},
)
@inproceedings(leino:2013,
 author       = {K. Rustan M. Leino},
 year         = {2013},
 title        = {Developing verified programs with {D}afny},
 editor       = {David Notkin and Betty H. C. Cheng and Klaus Pohl},
 booktitle    = {{ICSE} 2013},
 publisher    = {{IEEE}},
 pages        = {1488--1490},
 doi          = {10.1109/ICSE.2013.6606754},
)
@inproceedings(leino-autoactive:2010,
 author       = {K. Rustan M. Leino and Moska\l, Michal},
 year         = {2010},
 title        = {Usable Auto-Active Verification},
 editor       = {Tom Ball and Lenore Zuck and Natarajan Shankar},
 booktitle    = {UV 2010},
 url          = {http://fm.csl.sri.com/UV10/},
)
@inproceedings(leino:2016,
 author       = {K. Rustan M. Leino and Pit{-}Claudel, Cl{\'{e}}ment},
 year         = {2016},
 title        = {Trigger Selection Strategies to Stabilize Program Verifiers},
 editor       = {Swarat Chaudhuri and Azadeh Farzan},
 booktitle    = {CAV 2016},
 series       = {LNCS},
 volume       = {9779},
 publisher    = {Springer},
 pages        = {361--381},
 doi          = {10.1007/978-3-319-41528-4_20},
)
@mastersthesis(mbwambomsthesis:2017,
 author       = {Nicodemus M. J. Mbwambo},
 year         = {2017},
 title        = {{A Well-Designed, Tree-Based, Generic Map Component to Challenge the Process Towards Automated Verification}},
 type         = {{Master's Thesis}},
 school       = {Clemson University},
)
@article(meyer:1992,
 author       = {Bertrand Meyer},
 year         = {1992},
 title        = {Applying ``Design by Contract"},
 journal      = {Computer},
 volume       = {25},
 number       = {10},
 pages        = {40--51},
 doi          = {10.1109/2.161279},
)
@inproceedings(demoura:2008,
 author       = {Leonardo de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 editor       = {C. R. Ramakrishnan and Jakob Rehof},
 booktitle    = {TACAS 2008},
 series       = {LNCS},
 volume       = {4963},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@inproceedings(priester:2016,
 author       = {C. Priester and Y. S. Sun and M. Sitaraman},
 year         = {2016},
 title        = {Tool-Assisted Loop Invariant Development and Analysis},
 booktitle    = {2016 IEEE 29th International Conference on Software Engineering Education and Training (CSEET)},
 pages        = {66--70},
 doi          = {10.1109/CSEET.2016.28},
)
@inproceedings(regula:2012,
 author       = {Kalyan C. Regula and Hampton Smith and Heather Keown and Jason O. Hallstrom and Nigamanth Sridhar and Murali Sitaraman},
 year         = {2012},
 title        = {A Case Study in Verification of Embedded Network Software},
 editor       = {Alwyn Goodloe and Suzette Person},
 booktitle    = {{NFM} 2012},
 series       = {LNCS},
 volume       = {7226},
 publisher    = {Springer},
 pages        = {433--448},
 doi          = {10.1007/978-3-642-28891-3\_38},
)
@book(saleh:2015,
 author       = {Iman Saleh},
 year         = {2015},
 title        = {Formalizing Data-Centric Web Services},
 series       = {Web-Scale Workflow and Analytics},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-24678-9},
)
@article(sitaraman:2011,
 author       = {Murali Sitaraman and Bruce M. Adcock and Jeremy Avigad and Derek Bronish and Paolo Bucci and David Frazier and Harvey M. Friedman and Heather K. Harton and Wayne D. Heym and Jason Kirschenbaum and Joan Krone and Hampton Smith and Bruce W. Weide},
 year         = {2011},
 title        = {Building a Push-Button {RESOLVE} Verifier: Progress and Challenges},
 journal      = {{F}ormal {A}spects of {C}omputing},
 volume       = {23},
 number       = {5},
 pages        = {607--626},
 doi          = {10.1007/s00165-010-0154-3},
)
@phdthesis(sunphddiss:2018,
 author       = {Yu{-}Shan Sun},
 year         = {2018},
 title        = {Towards Automated Verification of Object-Based Software with Reference Behavior},
 type         = {{PhD Dissertation}},
 school       = {Clemson University},
)
@inproceedings(tagore:2012,
 author       = {Aditi Tagore and Diego Zaccai and Bruce W. Weide},
 year         = {2012},
 title        = {Automatically Proving Thousands of Verification Conditions Using an {SMT} Solver: An Empirical Study},
 booktitle    = {NFM 2012},
 pages        = {195--209},
 doi          = {10.1007/978-3-642-28891-3_20},
)
@inproceedings(tschannen:2015,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova},
 year         = {2015},
 title        = {AutoProof: Auto-Active Functional Verification of Object-Oriented Programs},
 editor       = {Christel Baier and Cesare Tinelli},
 booktitle    = {TACAS 2015},
 series       = {LNCS},
 volume       = {9035},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {566--580},
 doi          = {10.1007/978-3-662-46681-0_53},
)
@inproceedings(utting:2017,
 author       = {Mark Utting and David J. Pearce and Lindsay Groves},
 year         = {2017},
 title        = {Making {W}hiley {B}oogie!},
 editor       = {Nadia Polikarpova and Steve Schneider},
 booktitle    = {{IFM} 2017},
 series       = {LNCS},
 volume       = {10510},
 publisher    = {Springer},
 pages        = {69--84},
 doi          = {10.1007/978-3-319-66845-1_5},
)
@phdthesis(welch:2019,
 author       = {Daniel Welch},
 year         = {2019},
 title        = {Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software},
 type         = {{PhD Dissertation}},
 school       = {Clemson University},
)
@inproceedings(welch:2017,
 author       = {Daniel Welch and Murali Sitaraman},
 year         = {2017},
 title        = {Engineering and Employing Reusable Software Components for Modular Verification},
 editor       = {Goetz Botterweck and Claudia Werner},
 booktitle    = {{ICSR} 2017},
 series       = {LNCS},
 volume       = {10221},
 publisher    = {Springer},
 pages        = {139--154},
 doi          = {10.1007/978-3-319-56856-0_10},
)