Drachova, S. V., Hallstrom, J. O., Hollingsworth, J. E.,
Krone, J., Pak, R., and Sitaraman, M.: Teaching Mathematical Reasoning Principles for
Software Correctness and Its Assessment. ACM Trans. Computing Education 15, 3, Article 15 (August 2015), 22 pages.
[INFO]
Sitaraman, M. and Weide, B. W.:
Tutorial: Verified Software Components. ACM SPLASH 2013, Indianapolis, IN, October 2013.
[PDF]
Kulczycki, G., Sitaraman, M., Krone, J., Hillingsworth, J. E.,
Ogden, W. F., Weide, B. W., Bucci, P., Cook, C., Drachova-Strang, S.,
Durkee, B., Harton, H. K., Heym, W., Hoffman, D., Smith, H., Sun, Y.,
Tagore, A., Yasmin, N., and Zaccai, D.: A Language for Building
Verified Software Components. ICSR 2013.
[INFO]
Kulczycki, G., Smith, H., Harton, H. K., Sitaraman, Ogden, W. F., Hollingsworth, J. E.:
The Location Linking Concept: A Basis for Verification of Code Using Pointers. VSTTE 2012: 34-49.
[INFO]
Cook, C. T., Harton, H. K., Smith, H., and Sitaraman, M.: Specification engineering and modular verification
using a web-integrated verifying compiler. ICSE 2012: 1379-1382.
[INFO]
Sitaraman, M., Adcock, B. M., Avigad, J., Bronish, D., Bucci, P., Frazier, D., Fiedman, H. M., Harton, H. K., Heym, W. D.,
Kirschenbaum, J., Krone, J., Smith, H., Weide, B. W.: Building a push-button RESOLVE verifier: Progress and challenges.
Formal Asp. Comput. 23(5): 607-626 (2011)
[INFO]
Recent Dissertations/Thesis
Welch, D. T. (2019) Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software,
Ph. D. Dissertation, Clemson University.
[INFO and PDF]
Sun, Y-S. (2018) Towards Automated Verification of Object-Based Software with Reference Behavior,
Ph. D. Dissertation, Clemson University.
[INFO and PDF]
Mbwambo, N. M. J. (2017) A Well-Designed, Tree-Based, Generic Map Component to Challenge the Process Towards Automated Verification,
Master's Thesis, Clemson University.
[PDF]
Yasmin, N. (2015) Specification and Mechanical Verification of Performance Profiles of Software Components,
Ph. D. Thesis, The University of Mississippi.
[PDF]
Smith, H. (2013) Engineering Specifications and Mathematics for Verified Software,
Ph. D. Dissertation, Clemson University.
[PDF]
Drachova-Strang, S. V. (2013) Teaching and Assessment of Mathematical Principles for Software Correctness
Using a Reasoning Concept Inventory, Ph. D. Dissertation, Clemson University.
[PDF]
Harton H. K. (2011) Mechanical and Modular Verification Condition Generation For Object-Based Software,
Ph. D. Dissertation, Clemson University.
[PDF]
Sitaraman M., Adcock B., Avigad J., Bronish D., Bucci P.,
Frazier D., Friedman H., Harton H., Heym W.,
Kirschenbaum J., Krone J., Smith H., Weide B.W.: Building
a Pushbutton RESOLVE Verifier: Progress and Challenges.
To appear in Formal Aspects of Computing, Springer (2010)
[PDF]
Odgen W. F., Hollingsworth J. E., Krone J., Sitaraman M.,
Weide B. W. (2007) The RESOLVE Software Verification
Vision. In Proceedings of the RESOLVE 2007 Workshop,
pp 1-3.
[PDF]
Sitaraman M., Weide B. W.: Component-based software
using RESOLVE. Softw. Eng. Notes 19(4) pp.
21-22 (1994)
[INFO]
RESOLVE Language
Kulczycki G., Sitaraman M., Yasmin N., Roche K. (2009)
Formal Specification. In: Wah B (ed.),
Wiley Encyclopedia of Computer Science and Engineering.
John Wiley & Sons.
[INFO]
Kulczycki G., Sitaraman M., Weide B. W., Rountev A. (2006)
A specification-based approach to reasoning about pointers.
ACM SIGSOFT Software Engineering Notes 31:55-62.
Odgen W. F., Sitaraman M., Weide B. W., Zweben S. H.:
Part I: the RESOLVE framework and discipline: a research synopsis.
Softw. Eng. Notes 19(4) pp. 23-38 (1994)
[INFO]
Edwards S. H., Heym W. D., Long T. J., Sitaraman M.,
Weide B. W.: Part II: specifying components in RESOLVE.
SIGSOFT Softw. Eng. Notes 19(4) pp. 29-39 (1994)
[INFO]
Bucci P., Hollingsworth J. E., Krone J., Weide B. W.:
Part III: implementing components in RESOLVE.
SIGSOFT Softw. Eng. Notes 19(4) pp. 40-51 (1994)
[INFO]
Harms D. E., Weide B. W.: (1991) Copying and swapping:
Influences on the design of reusable software components.
IEEE TSE 17(5):424–435.
[INFO]
Semantics and Foundations
Harton H. K. (2011) Mechanical and Modular Verification Condition Generation For Object-Based Software, Ph. D. Dissertation,
Clemson University.
[PDF]
Kulczycki G. (2004) Direct Reasoning, Ph. D. Dissertation,
Clemson University.
[PDF]
Heym, W. (1995) Computer Program Verification:
Improvements for Human Reasoning. Ph.D. thesis,
The Ohio State University, 1995.
[PDF]
Krone J (1988) The Role of Verification in Software
Reusability. PhD. Thesis, The Ohio State University.
Verification Tools and Experimentation
Sitaraman M., Adcock B., Avigad J., Bronish D., Bucci P.,
Frazier D., Friedman H., Harton H., Heym W.,
Kirschenbaum J., Krone J., Smith H., Weide B.W.: Building
a Pushbutton RESOLVE Verifier: Progress and Challenges.
To appear in Formal Aspects of Computing, Springer (2010)
[PDF]
Kirschenbaum J., Adcock B., Bronish D., Smith H.,
Harton H., Sitaraman M., Weide B. W. (2009) Verifying
Component-Based Software: Deep Mathematics or Simple
Bookkeeping? In: Edwards S. H., Kulczycki G. (eds.)
Proc. ICSR, LNCS 5791. Springer. pp 31-40.
[INFO]
Weide, B. W., Sitaraman, M., Harton, H. K., Adcock, B.,
Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J.,
Frazier, D., "Incremental Benchmarks for Software
Verification Tools and Techniques", Proceedings of
VSTTE 2008 (Verified Software: Theories, Tools, and
Experiments), Springer-Verlag LNCS 5295, October 2008, 84-98
[PDF]
Harton H K, Sitaraman M, Krone J (2008) Formal Program
Verification. In: Wah B (ed.), Wiley Encyclopedia of
Computer Science and Engineering. John Wiley & Sons.
[INFO]
Sitaraman M., Atkinson S., Kulczycki G., Weide B. W., Long T.,
Bucci P., Pike S., Heym W., Hollingsworth J. (2000)
Reasoning about software-component behavior. In
Proceedings of the 6th International Conference on
Software Reuse, LCNS 1844. Springer Berlin, pp 266-283.
[INFO]
Education
Drachova-Strang S., Teaching and Assessment of Mathematical
Principles for Software Correctness Using a Reasoning Concept
Inventory, Ph. D. Dissertation, Clemson University. (2013)
[PDF]
Sitaraman M., Hallstrom J. O., White J., Drachova-Strang S.,
Harton H. K., Leonard D., Krone J., Pak R., Engaging Students
in Specification and Reasoning: "hands-on" Experimentation
and Evaluation, In Proceedings of the 14th Annual ACM
SIGCSE Conference on Innovation and Technology in Computer
Science Education, ACM. pp 50-54. (2009)
[INFO]
Sitaraman M., Hallstrom J. O., White J., Drachova-Strang S.,
Harton H. K., Leonard D., Krone J., Pak R., Talk Slides:
Engaging Students in Specification and Reasoning:
"hands-on" Experimentation and Evaluation. (2009)
[PPT]
Leonard D. P, Hallstrom J. O., Sitaraman M., Injecting
Rapid Feedback and Collaborative Reasoning in Teaching
Specifications, In Proceedings of the 40th ACM Technical
Symposium on Computer Science Education, ACM. pp 524-528.
(2009)
[INFO]
Drachova-Strang S., Teaching Design-By-Contract
with Formal Specifications. (2009)
[PDF]
Performance Specification and Verification
Krone J., Odgen W. F., Sitaraman M., (2006) Performance
Analysis Based Upon Complete Profiles. In: Proceedings
of the 2006 conference on Specification and verification of
component-based systems. ACM, pp 3-10.
[INFO]
RESOLVE Application to Other Languages
Smith H., Harton H., Frazier D., Mohan R., Sitaraman M.,
(2009) Generating Verified Java Components through
RESOLVE. In: Edwards S H, Kulc-zycki G (eds.)
Proc. ICSR, LNCS 5791. Springer. pp 11-20.
[INFO]
Hollingsworth J. E., Blankenship L., Weide B. W. (2000)
Experience report: using RESOLVE/C++ for commercial
software. In: Schneir B (ed.) Proc. FSE. ACM, pp 11-19.
[INFO]
Kulczycki G., Vasudeo J., (2006) Simplifying Reasoning
About Objects in Tako. In: Proceedings of the 2006
conference on Specification and verification of
component-based systems. ACM, pp 57-64.
[INFO]
Michelle Cook, Megan Fowler, Jason O. Hallstrom, Joesph E. Hollingsworth, Matthew P. Pfister, Tim Schwab, Yu-Shan Sun, and Murali Sitaraman,
Pinpointing Student Obstacles to Logical Reasoning about Code,
Technical Report RSRG-17-01, School of Computing, Clemson University,
Clemson, SC 29634, April 2017, 9 pages.
Gregory Kulczycki, Murali Sitaraman, Joan Krone, Joseph E. Hollingsworth,
William F. Ogden, Bruce W. Weide, Paolo Bucci, Charles T. Cook, Svetlana Drachova,
Blair Durkee, Heather Harton, Wayne Heym, Dustin Hoffman, Hampton Smith,
Yu-Shan Sun, Aditi Tagore, Nighat Yasmin, and Diego Zaccai,
A Language for Building Verified Software Components,
Technical Report RSRG-13-01, School of Computing, Clemson University,
Clemson, SC 29634-0974, February 2013, 16 pages.
Charles T. Cook, Svetlana Drachova, Yu-Shan Sun, Murali Sitaraman, Jeff C. Carver,
and Joseph E. Hollingsworth,
Specification and Reasoning in SE Projects Using a Web IDE,
Technical Report RSRG-13-02, School of Computing, Clemson University,
Clemson, SC 29634-0974, February 2013, 10 pages.
Svetlana Drachova, Jason O. Hallstrom, Murali Sitaraman, Joseph E. Hollingsworth, and Joan Krone,
Assessment of Learning Outcomes Using a Mathematical Reasoning Concept Inventory,
Technical Report RSRG-13-03, School of Computing, Clemson University,
Clemson, SC 29634-0974, February 2013, 6 pages; superceded by Technical Report RSRG-13-06.
M. Sitaraman, W. F. Ogden, B. W. Weide,
Verified Software Components,
Technical Report RSRG-12-01, School of Computing, Clemson University,
Clemson, SC 29634-0974, January 2012, 129 pages.
2011
S. V. Drachova, J. E. Hollingsworth, J. Krone, J. O. Hallstrom,
R. Pak, and M. Sitaraman,
Assessment of Learning Outcomes Using a Mathematical Reasoning Concept Inventory,
Technical Report RSRG-11-01, School of Computing,
Clemson University, Clemson, SC 29634-0974, September 2011, 6 pages.
S. V. Drachova, J. O. Hallstrom, J. E. Hollingsworth, D. P. Jacobs,
J. Krone, and M. Sitaraman,
A Systematic Approach to Teaching
Abstraction and Mathematical Modeling,
Technical Report
RSRG-11-02, School of Computing, Clemson University, Clemson,
SC 29634-0974, September 2011, 6 pages.
J. Krone, J. E. Hollingsworth, M. Sitaraman and J. O. Hallstrom,
A Reasoning Concept Inventory for
Computer Science,
Technical Report RSRG-10-01, School of Computing, Clemson University,
Clemson, SC 29634-0974, September 2010, 6 pages.
M. Sitaraman, B. Adcock, J. Avigad, D. Bronish, P. Bucci,
D. Frazier, H. M. Friedman, H. Harton, W. Heym, J. Kirschenbaum,
J. Krone, H. Smith, and B. W. Weide,
Building a Push-Button RESOLVE Verifier:
Progress and Challenges,
Technical Report RSRG-09-01, School of Computing, Clemson University,
Clemson, SC 29634-0974, January 2009, 34 pages.
2008
J. Krone, W. F. Ogden, M. Sitaraman, and B. W. Weide,
Refocusing the
Verifying Compiler Grand Challenge,
Technical Report RSRG-08-01, School of Computing, Clemson University,
Clemson, SC 29634-0974, June 2008, 10 pages.
B. W. Weide, M. Sitaraman, H. K. Harton, B. Adcock, P. Bucci,
D. Bronish, W. D. Heym, J. Kirschenbaum, D. Frazier,
Incremental Benchmarks for
Software Verification Tools and Techniques,
Technical Report RSRG-08-02, School of Computing, Clemson University,
Clemson, SC 29634-0974, June 2008, 16 pages.
J. Kirschenbaum, H. K. Harton, and M. Sitaraman,
A Case Study in Automated Verification,
Technical Report RSRG-08-04, School of Computing, Clemson University,
Clemson, SC 29634-0974, June 2008, 6 pages.
2006
G. Kulczycki, S. Duckworth, M. Sitaraman, and B. W. Weide,
Abstracting Pointers
for a Verifying Compiler,
Technical Report RSRG-06-01, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, March 2006, 19 pages.
2005
G. Kulczycki, M. Sitaraman, W. F. Ogden, and B. W. Weide,
Clean Semantics for
Calls with Repeated Arguments,
Technical Report RSRG-05-01, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, March 2005, 13 pages.
2004
G. Kulczycki, et al., Preserving Clean Semantics for Calls with
Repeated Arguments,
Technical Report RSRG-04-01. Superceded by Technical Report RSRG-05-01.
S. H. Edwards, M. Sitaraman, B. W. Weide, and J. E. Hollingsworth,
Contract-Checking Wrappers for C++ Components,
Technical Report RSRG-04-02, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, January 2004, 23 pages. Please see IEEE Transactions on Software Engineering, November 2004.
G. Kulczycki, et al.,
Reasoning about Procedure Calls with Repeated Arguments
and the Reference-Value Distinction,
Technical Report RSRG-03-01. Superceded by Technical Report RSRG-05-01.
G. Kulczycki, M. Sitaraman, W. F. Ogden, and J. E. Hollingsworth,
Component Technology for Pointers:
Why and How,
Technical Report RSRG-03-03, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, April 2003, 19 pages.
J. Krone, W. F. Ogden, and, M. Sitaraman,
Modular Verification of Performance Constraints,
Technical Report RSRG-03-04, Department of Computer Science, Clemson University,
Clemson, SC 29634-0974, May 2003, 25 pages.
M. Sitaraman, D. P. Gandi, W. Kuechlin, C. Sinz, and B. W. Weide,
The Humane Bugfinder: Modular
Static Analysis Using a SAT Solver,
Technical Report RSRG-03-05, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, May 2003, 18 pages.
J. Krone, W. F. Ogden, and, M. Sitaraman,
OO Big O: A Sensitive
Notation for Software Engineering,
Technical Report RSRG-03-06, Department of Computer Science,
Clemson University, Clemson, SC 29634-0974, September 2003, 10 pages.