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
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
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.
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.