A model check in a test file is a great idea. In fact, one of the hot topics of formal technologies is automatic test generation (at least in the hardware world).
2016-06-28 15:33 GMT+02:00 Daniel Skinner <dan...@dasa.cc>: > 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. >>> >> -- Scott Cotton President, IRI France SAS http://www.iri-labs.com -- 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.
