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), it just so happens people have been able to coerce a solution to these kinds of problems (boolean and integer) with simplex. To me that read as do-able but not efficient.
I also found it curious what those solutions actually meant when expressed from an LP. For example, for boolean the problem/solution were considered relaxed since the result is in range 0..1 instead of 0 or 1 and there was another step for further resolving i forget. That also brings into question accumulated floating point error for something that really shouldn't suffer from that, boolean or integer operations. I didn't dig too much further since I was mostly just interested in what formal verification entailed and understanding what many of the tools were doing, but i certainly felt like if i really wanted to I could manually express a model check today in a test file. On Tue, Jun 28, 2016 at 2:49 AM Seb Binet <seb.bi...@gmail.com> wrote: > 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.
