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. but starting out with some basics could go a long way. bit blasting code with no concurrency into a transition system is an obvious starting point. modelling the concurrency in some clean, symbolic or compact way to represent all possible interleavings would enable lots of possibilities downstream (spin,smt, and the go tools that are starting to show up). 2016-06-28 0:24 GMT+02:00 Daniel Skinner <dan...@dasa.cc>: > > 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. > > 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. >> > -- 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.
