[SystemSafety] A realistic view of formal verification

[Dr. Brendan Patrick Mahony]

@Derek,

Surely this is a potential flaw inherent to all of science, engineering and I might suggest mathematics itself.

Given the massive efforts now underway to “assure down to the silicon” (see CompCert, DeepSpec, Everest, Cheri etc) it can not be seen as a minority view in the digital engineering mathematics community. The grand challenge of formal methods is to synthesise assurance arguments of correct behaviour of digital designs from a basis of accepted scientific theory.

A possibly more subtle and interesting threat to this assurance project is the relationship between assured designs and manufactured objects.

Brendan

> On 8 Dec 2022, at 12:39 am, Derek M Jones <derek at knosof.co.uk> wrote:
> 
> All,
> 
> I was pleased to see that some researchers have a realistic
> view of formal verification
> "... as with all formal verification, a possible weak link
> is the connection between the formal models and the real world"
> https://arxiv.org/abs/2212.01748
> 
> -- 
> Derek M. Jones           Evidence-based software engineering
> blog:https://shape-of-code.com
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>