High-assurance systems of the 70’s-80’s used formal specification in languages like Z and VDM to increase correctness of software. These were often hard to use for a lot of people involved. The ASM’s did similar stuff in a way that’s easy for programmers and even non-programmers to understand. Lots of tooling got built for various stages of ASM development. These and similar things like B method (esp Atlier-B) were used in industry to produce highly-robust software proven correct from requirements to design to accurate models of code.
Most verification uses Coq, Isabelle/HOL, etc these days. Closest thing to this with adoption is TLA+. People using that or frustrated with the difficulty of semantic methods definitely should look into ASM’s.
Use in verified compilation is particularly interesting. The components are so small vs what I see in semantic methods. Here’s the best one that I’m aware of:
High-assurance systems of the 70’s-80’s used formal specification in languages like Z and VDM to increase correctness of software. These were often hard to use for a lot of people involved. The ASM’s did similar stuff in a way that’s easy for programmers and even non-programmers to understand. Lots of tooling got built for various stages of ASM development. These and similar things like B method (esp Atlier-B) were used in industry to produce highly-robust software proven correct from requirements to design to accurate models of code.
Most verification uses Coq, Isabelle/HOL, etc these days. Closest thing to this with adoption is TLA+. People using that or frustrated with the difficulty of semantic methods definitely should look into ASM’s.
Survey of many uses of the method:
https://pdfs.semanticscholar.org/81aa/8726219c4145ff6b8932837203d07b34b51e.pdf
Use in verified compilation is particularly interesting. The components are so small vs what I see in semantic methods. Here’s the best one that I’m aware of:
http://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf
In other words, is this an underappreciated (by way of historical reasons) method of formal verification?
That’s part of what I’m saying. The point of posts like this is to draw attention to such things in case people benefit from them.