Re: [go-nuts] Re: formal verification in Go? someday perhaps?

A late followup, shameless plug https://github.com/irifrance/gini Best, Scott Le mardi 28 juin 2016 09:49:21 UTC+2, Sebastien Binet a écrit : > > > > On Tue, Jun 28, 2016 at 12:24 AM, Daniel Skinner > wrote: > >> > I think a better question is: can go tools for formal

Re: [go-nuts] Re: formal verification in Go? someday perhaps?

Actually, I was thinking there's probably something in gonum more suitable than expressing it as a linear program. When I do searches for boolean satisfiability problem for example, simplex is not what's mentioned in papers. From what I have understood (I'm by no means an expert in any of this),

Re: [go-nuts] Re: formal verification in Go? someday perhaps?

I don't see why not either. I think what's missing for targeting go is this: A library taking ssa representation and producing formal representations (formulae, transition systems, models of parallelism,...) I guess that may actually be many libraries, as there are many different ways to model.

[go-nuts] Re: formal verification in Go? someday perhaps?

I think a better question is: can go tools for formal verification become available? The distinction is that formal verification tools can be applied to hardware, protocols, assembly, software, etc. Why not do that in go? Most such tools are in C or C++, and the low level engines/components