Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?

Anecdotal experience constructing proofs of correctness of code built from reusable software components reveals that they tend to be relatively trivial bookkeeping exercises: they rarely require a substantive mathematical deduction. A careful empirical analysis of hundreds of verification conditions (VCs) for a library of component-client code shows the level of sophistication each proof requires, and suggests how to use the results to characterize a notion of mathematical "obviousness."

• Type: Journal
• Year: 2009
• Where: ICSR
• Authors: Jason Kirschenbaum, Bruce M. Adcock, Derek Bronish, Hampton Smith, Heather K. Harton, Murali Sitaraman, Bruce W. Weide
• Keywords: Careful Empirical Analysis, ICSR 2009, Reusable Software Components, Software Engineering, Substantive Mathematical Deduction