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

  • 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

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

Page last updated March 10, 2010 by Chuck Cook