Affordable Access

The Verified Software Challenge: A Call for a Holistic Approach to Reliability

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Engineering


The software analysis community has made a lot of progress in creating software tools for detecting defects and performing proofs of shallow properties of programs. We are witnessing the birth of a virtuous cycle between software tools and their consumers and I, for one, am very excited about this. We understand much better how to engineer program analyses to scale to large code bases and deal with the difficult problem of false errors and reducing their number. We understand better the tradeoffs in sound vs. unsound analyses. The software tools developed and applied over the last eight years have had impact. This list of tools includes Blast [HJMS02], CCured [NMW02], CQual [FTA02], ESC/Java [FLL02], ESP [DLS02], Feaver [Hol00], MAGIC [CCG04], MC [HCXE02], MOPS [CDW04], Prefast [LBD+04], Prefix [BPS00], SLAM [BR01], Splint [EL02] and Verisoft [God97], to name a few.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.