CACM logo

This Article

Contributed articles

Certified Software

[article image]
Credit: John Hersey

Zhong Shao

December 1, 2010

Only if the programmer can prove (through formal machine-checkable proofs) it is free of bugs with respect to a claim of dependability.

User Comments

 (1)

Years ago, I followed a course on formal semantics... and, although I could follow all the theory and mathematics with little effort, I was uneasy with the material. More recently, I got to know the concept of an ontology, and realized that it covers concepts but not instances (i.e. a car but not your car parked in front of your office building). Suddenly, while studying Pi-calculus, I realized the cause of my uneasiness: those formal techniques, languages, ... could not even capture a real-world concept, and surely not its real-world instances. This is unfortunate since "dependability" is most relevant when the real world is involved in a physical manner. If certified software wants our respect, it should at least show evidence that it is trying to address the certification of "a person will not be stuck between computer-controlled doors" and if it happens "the subway train will not start moving with a person hanging halfway out of the wagon". Can anyone point me to publications looking into this matter? Which research is going beyond "the rewriting of computations"? I recognize the merit of "treating certification separately from ..." but I have to point out that there is little added value in reinforcing what already are the stronger links. It may be useful but does not merit priority over efforts looking at the weakest link (outside the comfort zones of research communities).

   — Paul Valckenaers, November 25, 2010
Post a comment...
Name: Anonymous

Signed and anonymous comments submitted to this site are moderated and will appear if they are relevant to the topic and not abusive. Your comment will appear with your username if you are signed into the site, and will be anonymous if you are not signed in. View our policy on comments

Tools For Readers

Bookmark and Share
Default Font Size Large Font Size X-Large Font Size Text Size
Author profiles and more in the Digital Library

Related ACM Resources

Conferences:

Courses:

  • Storage Network Management - Understanding SAN management challenges, requirements, and solutions will help you design more robust SAN solutions and recommend storage management products for potential clients. After completing …
More About ACM Resources

In The Digital Library

About Communications | Join ACM External Link | Renew External Link | Subscribe External Link | Sign In | For Authors | For Advertisers External Link | Privacy | Site Map | Help | Contact Us | Mobile Site

Copyright © 2012 by the ACM. All rights reserved.

Back to Top