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