3 ms·

Things have indeed changed, then. I used to write software destined for avionics (assembler stuff in the 80s) and that was required to apply formal considerati

Things have indeed changed, then. I used to write software destined for avionics (assembler stuff in the 80s) and that was required to apply formal considerations. I think that conservatism in certain avenues of software implementation is essential and one can't even truly be considered an engineer (or software engineer, whatever that currently means) without exposure to formal discipline. Edit: I've never considered myself to be an engineer of any kind nor have I claimed to be one.

arethuza 15y ago
Out of interest, what formal methods were used then? I remember there being some CPU designs in the 80's (e.g. VIPER) that had been formally verified but that all seemed to die out in the 90s.
- Craiggybear 15y ago
  Good point -- VIPER isn't essential and one could argue that an assembler of any kind isn't guaranteed to give rise to totally engineering quality results (ADA and Eiffel were probably better for that at the time) but there were things like VDM, Z notation, ASM's, etc, BNF and Model Checking approaches.
  - pascal_cuoq 15y ago
    Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would be that I see many academics in the field of formal methods act and speak as if these were used everywhere they could be useful, which is vexing when one's job is precisely of doing what is necessary to transfer them. The Z notation / B method community is still strong (though they seem a bit defensive when met at conferences). I only know about VDM because some of the syntax in Caveat is inspired from it (Caveat is the tool whose application is described in the link I provided. It was developed at the lab I work at, but before I was hired). Just in case, here is what we are now working on. One description is "successor to Caveat", but it's more than that. For one thing, it's Open Source (type "apt-get frama-c" or equivalent in most Linux distributions). It allows to combine techniques that range from static analysis to formal verification of functional properties using Hoare logic: http://frama-c.com/try_out.html http://frama-c.com/try_out.html (automatic analyses) http://frama-c.com/jessie/jessie-tutorial.pdf http://frama-c.com/jessie/jessie-tutorial.pdf (verification based on Hoare logic)
    - Craiggybear 15y ago
      You are welcome. I found your comments very interesting. Not harsh at all. Many thanks for the additional links above. I found them well worthwhile reading.

arethuza 15y ago

Out of interest, what formal methods were used then? I remember there being some CPU designs in the 80's (e.g. VIPER) that had been formally verified but that all seemed to die out in the 90s.

Craiggybear 15y ago
Good point -- VIPER isn't essential and one could argue that an assembler of any kind isn't guaranteed to give rise to totally engineering quality results (ADA and Eiffel were probably better for that at the time) but there were things like VDM, Z notation, ASM's, etc, BNF and Model Checking approaches.
- pascal_cuoq 15y ago
  Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would be that I see many academics in the field of formal methods act and speak as if these were used everywhere they could be useful, which is vexing when one's job is precisely of doing what is necessary to transfer them. The Z notation / B method community is still strong (though they seem a bit defensive when met at conferences). I only know about VDM because some of the syntax in Caveat is inspired from it (Caveat is the tool whose application is described in the link I provided. It was developed at the lab I work at, but before I was hired). Just in case, here is what we are now working on. One description is "successor to Caveat", but it's more than that. For one thing, it's Open Source (type "apt-get frama-c" or equivalent in most Linux distributions). It allows to combine techniques that range from static analysis to formal verification of functional properties using Hoare logic: http://frama-c.com/try_out.html http://frama-c.com/try_out.html (automatic analyses) http://frama-c.com/jessie/jessie-tutorial.pdf http://frama-c.com/jessie/jessie-tutorial.pdf (verification based on Hoare logic)
  - Craiggybear 15y ago
    You are welcome. I found your comments very interesting. Not harsh at all. Many thanks for the additional links above. I found them well worthwhile reading.