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 <[email protected] > <javascript:>> 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 <[email protected] <javascript:>> 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 [email protected] <javascript:>. >>> 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 [email protected] <javascript:>. >> 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
