On Tue, Jun 28, 2016 at 12:24 AM, Daniel Skinner <dan...@dasa.cc> wrote:
> > I think a better question is: can go tools for formal verification > become available? > > I did some research on formal verification recently, no experience > previously. I don't really see why not. Just digging through my own code, I > have an implementation of the simplex method which I could use to solve > boolean and integer linear optimizations. Gonum likely has better > optimizers up for the tasks, though i haven't looked. > FYI, they are here: https://godoc.org/github.com/gonum/optimize/convex/lp https://godoc.org/github.com/gonum/optimize#Method examples: https://godoc.org/github.com/gonum/optimize#example-Local https://godoc.org/github.com/gonum/optimize/convex/lp#example-Simplex hth, -s > It just seemed like the most difficult part would be providing an > intuitive way of defining the problem given a domain. Of course, static > analysis is great too and you made me curious, what's missing from the `go` > package to go that route? > > On Sun, Jun 26, 2016 at 3:49 PM <w...@iri-labs.com> wrote: > >> 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 are >> highly optimised. Go can easily compete with "standard" C/C++, i.e. >> software which has not been highly optimised. It also provides enough >> low-level access to be competitive against highly optimised C/C++ (e.g. >> assembly, precision of memory representations) but it takes work. >> >> One of the research initiatives we are taking up is "scalable cloud >> architectures for formal technologies". Basically, composable cloud >> microservices for formal technologies like model checking, SAT/BDD/SMT, >> theorem proving, as well as encoders for verification problems, etc, but in >> terms of deployment in the cloud. A related startup is satalia. Go is a >> natural fit for this initiative, and we already have some results with go. >> >> I think the biggest obstacle to formal tools targeting analysis of go >> programs is formal representations in the golang "go" package. Once that >> is available, things will start to snowball. >> >> >> >> >> >> Le lundi 9 mars 2015 01:07:36 UTC+1, Camilo Aguilar a écrit : >>> >>> I ran across this post today: >>> http://blog.adacore.com/testing-static-formal. Basically, showing how >>> you can do formal verifications in ADA2012. Is it realistic to think that a >>> feature like that would someday arrive to Go? >> >> -- >> You received this message because you are subscribed to the Google Groups >> "golang-nuts" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to golang-nuts+unsubscr...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >> > -- > You received this message because you are subscribed to the Google Groups > "golang-nuts" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to golang-nuts+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
