Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category

[David D. <da...@di...>]

Hi Christoph,

I was wondering if there exists a document that specifies this floating point logic? Also could you inform me some solvers that support them? Besides z3 I suppose…

Best regards,

— David.

> On Feb 11, 2015, at 11:20 AM, Christoph Wintersteiger <cw...@mi...> wrote:
> 
> Hi Sylvain, David, Tjark,
>  
> Martin Brain and I discussed the possibility of a category for floating-point arithmetic at this year’s SMT comp. We believe that there are enough solvers and sufficient interest, and the theory definition has recently been finalized. We are happy to collect benchmarks (we have a few ready) and to assist with the running of the competition if there are any issues of course. What would be the next steps for us to make this happen?
>  
> Thanks!
> Christoph
>  
>  
> Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 |research.microsoft.com/people/cwinter
>  
> <image001.jpg>
> 
> Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 
>  
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming. The Go Parallel Website,
> sponsored by Intel and developed in partnership with Slashdot Media, is your
> hub for all things parallel software development, from weekly thought
> leadership blogs to news, videos, case studies, tutorials and more. Take a
> look and join the conversation now. http://goparallel.sourceforge.net/_______________________________________________
> Smtcomp-discussion mailing list
> Smt...@li...
> https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion