acm-header
Sign In

Communications of the ACM

Contributed articles

Certified Software


Certified Software illustration

Credit: John Hersey

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

The full text of this article is premium content


Comments


Paul Valckenaers

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


Displaying 1 comment

Log in to Read the Full Article

Sign In

Sign in using your ACM Web Account username and password to access premium content if you are an ACM member, Communications subscriber or Digital Library subscriber.

Need Access?

Please select one of the options below for access to premium content and features.

Create a Web Account

If you are already an ACM member, Communications subscriber, or Digital Library subscriber, please set up a web account to access premium content on this site.

Join the ACM

Become a member to take full advantage of ACM's outstanding computing information resources, networking opportunities, and other benefits.
  

Subscribe to Communications of the ACM Magazine

Get full access to 50+ years of CACM content and receive the print version of the magazine monthly.

Purchase the Article

Non-members can purchase this article or a copy of the magazine in which it appears.