Selected Recent Publications

  • 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

  • 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]

Resources

Research Partners

Workshops

Publications

Overview & Vision

  • 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]

Technical Reports

2017

2016

2015

2014

2013

2012

  • 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

2010

2009

  • 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

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

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.
  • J. Krone, W. F. Ogden, and M. Sitaraman, Profiles: A Compositional Mechanism for Performance Specification, Technical Report RSRG-04-03, Department of Computer Science, Clemson University, Clemson, SC 29634-0974, June 2004, 24 pages.

2003

Talks