3 ms·
> What about less strict and more used languages like C or Java? there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm
by munin 13y ago
> What about less strict and more used languages like C or Java?
there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm http://www.absint.com/astree/index.htm). Airbus, volkswagen, and similar companies use astree (they are, as I understand it, required to by EU law) to verify safety-critical software in their airplanes and cars. though astree has some large limitations on the C code it can verify, for example, no dynamically allocated memory or recursion.
investigating why it has these limitations is a good way to begin investigating what our current limitations are when formally reasoning about computer programs, and why C is so terrible to assure...
- barries 13y agoSee also Frama-C (http://frama-c.com/ http://frama-c.com/), which can use multiple automated and interactive theorem provers. It's really a proof obligation management IDE that you can use with multiple provers / proof assistants.
- joaoff 13y agoDynamically allocated memory is difficult to verify automatically. There are some tools based on separation logic (e.g. Smallfoot, HIP/SLEEK, jStar) that are able to verify C programs (or C-like programs). Current developments in this area are focusing on automatically inferring specifications (also known as abductive reasoning). Moreover, automatically verifying concurrent programs is also difficult and a hot research topic at the moment. If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com http://www.monoidics.com). Interestingly, the company was recently acquired by Facebook :) Update: Here's a link with a list of related tools: http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Friends_of_Invader.html http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...