smtcomp-discussion Mailing List for SMTCOMP (Page 2)
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
You can subscribe to this list here.
2014 |
Jan
(4) |
Feb
(11) |
Mar
|
Apr
(18) |
May
(104) |
Jun
(124) |
Jul
|
Aug
(2) |
Sep
|
Oct
|
Nov
(1) |
Dec
|
---|---|---|---|---|---|---|---|---|---|---|---|---|
2015 |
Jan
|
Feb
(4) |
Mar
(8) |
Apr
|
May
(4) |
Jun
(10) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2016 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2017 |
Jan
|
Feb
|
Mar
(8) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2018 |
Jan
|
Feb
|
Mar
(2) |
Apr
(2) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: David D. <da...@di...> - 2015-05-06 14:24:38
|
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 |
From: Christoph W. <cw...@mi...> - 2015-05-06 13:54:28
|
Hi David, The theory definitions is here: http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2 There are no formal logic definitions yet, but for QF_FP and QF_BVFP it's straightforward (with the exception that FP uses bit-vector numerals, but no other BV operations). Solvers that support FP and that I know of are: Z3, MathSAT, Sonolar. AFAIK, CVC4 will have support soon, it would great to get them to participate in the demo track, but I don't know how much effort this will take on their end. CBMC is not an SMT solver, but it has a bit-blaster that can emit SMT2 formatted queries. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter 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 -----Original Message----- From: David Deharbe [mailto:da...@di...] Sent: 06 May 2015 14:30 To: Christoph Wintersteiger Cc: smt...@li...; Martin Brain Subject: Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category 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 |
From: Dejan J. <dej...@gm...> - 2015-05-04 18:41:14
|
On Sun, Feb 8, 2015 at 7:20 AM Tjark Weber <tja...@it...> wrote: > ====================================================================== > > 10th International Satisfiability Modulo Theories Competition > (SMT-COMP'15) > > July 19, 2015 > San Francisco, USA > > CALL FOR COMMENTS > CALL FOR BENCHMARKS > PRELIMINARY CALL FOR SOLVERS > > ====================================================================== > > SMT-COMP is the annual competition among Satisfiability Modulo Theories > (SMT) solvers. The goals of SMT-COMP are to spur solver advances, > collect benchmarks, and encourage adoption of the SMT-LIB standard, > through friendly competition. > > SMT-COMP'15 will end in time to be described and the results announced > at the SMT Workshop (July 18-19), which is affiliated with the 27th > International Conference on Computer Aided Verification (CAV 2015). > > SMT-COMP'15 is organized under the direction of the SMT Steering > committee. The organizing team for SMT-COMP'15 is > > . Sylvain Conchon - Paris-Sud University, France > . David Deharbe - Federal University of Rio Grande do Norte, Brazil > . Tjark Weber - Uppsala University, Sweden > > This is a call for three things: > > CALL FOR COMMENTS: > > The organizing team is preparing the schedule and rules for 2015. > Any comments you may have to improve the competition over past years > or to redirect its focus are welcome and will be considered by the > team. Please submit such comments by *** 22 February 2015. *** > > For SMT-COMP'15, we are particularly interested in comments regarding: > > - Sequential vs. parallel performance: All solvers will have several > CPU cores available, and we plan to measure CPU and wall time. Solver > developers might wish to prepare both sequential and parallel versions > of their solvers. > > - Benchmark selection: We will likely have sufficient computational > resources to run all solvers on all eligible benchmarks. Therefore, we > are interested in proposals for weighing the results so as to avoid > over-representation of certain (large) benchmark families. > > - Scope: After the successful migration to StarExec in 2013/14, we are > considering to broaden the scope of SMT-COMP again. We might reinstate > additional tracks, e.g., for unsat core extraction and proof-producing > solvers. > > CALL FOR BENCHMARKS: > > The competition is enhanced by new sets of benchmarks to add to those > already in use (and used in past competitions). A selection of > benchmarks in various categories is used for the competition (according > to rules that are currently being revised). > > If you have benchmarks that you think would be useful to SMT-LIB and > SMT-COMP (and may be made public), please let us know as soon as > possible, even if the material is not quite ready. We will work in > close cooperation with the SMT-LIB maintainers to include such > benchmarks in the SMT-LIB in time to be taken into account for the > competition. The deadline for benchmarks to be used in the 2015 > competition will be announced when the schedule and rules are > finalized. > > PRELIMINARY CALL FOR SOLVERS: > > A submission deadline for solvers will be announced along with the > rules. However, it is useful to the organizing team to know in advance > which and how many solvers may be entering. Thus we request that you > let us know at your earliest convenience if you think you may be > submitting one or more solvers to SMT-COMP'15, particularly if you > think there may be unusual circumstances. > > COMMUNICATION: > > The competition web-site will be at www.smtcomp.org. > > Public email regarding the competition may be sent to > smt...@cs.... > > Announcements will be sent on both smt...@cs... and > sm...@cs.... > > Email to the organizers only may be sent to > smt...@li... > > Sincerely, > The organizing team > > > _______________________________________________ > SMT-LIB mailing list > SM...@cs... > http://www.cs.nyu.edu/mailman/listinfo/smt-lib > |
From: Christoph W. <cw...@mi...> - 2015-05-01 16:26:00
|
Hi Tjark, I've uploaded a first set of benchmarks for QF_FP onto starexec, they are in SMT-LIB benchmarks/2015/non-incremental/QF_FP. I've added you to the user list, I hope that makes them visible to you but if not, let me know. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter 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 -----Original Message----- From: Tjark Weber [mailto:tja...@it...] Sent: 11 February 2015 15:19 To: Christoph Wintersteiger Cc: smt...@li...; Martin Brain; ces...@ui... Subject: Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category Christoph, On Wed, 2015-02-11 at 14:20 +0000, Christoph Wintersteiger wrote: > 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? I think this is an excellent suggestion. I reckon the next step would be for you to make these benchmarks available to us, so that they can be reviewed and (hopefully) incorporated into SMT-LIB. Best, Tjark |
From: Clark B. <ba...@cs...> - 2015-03-24 21:12:28
|
David, I have been maintaining the official SMT-LIB benchmark library. Currently, the most recent copy is on StarExec. There is one major update pending: we need to update the status of many of the "unknown" benchmarks based on a run David Cok did last summer. I hope to be able to complete this before May 1. Otherwise, for new benchmarks, the typical approach is to run them with a large timeout through several solvers (the competition solvers from last year, say) to determine well-formedness and status. If at least two solvers agree on their status, we typically accept that as the status. Otherwise, the status is unknown. Sometimes the benchmark providers know the status for one reason or another. Whenever possible, we ask them to provide the status. My suggestion would be to follow the above process for any newly submitted benchmarks and then contact me to upload the benchmarks once you have verified that things look good. We are in the process of developing a special-purpose tool for checking well-formedness of bechmarks, but I don't know if it will be ready before May 1. -Clark On Mon, Mar 16, 2015 at 5:25 AM, David Deharbe <da...@di...> wrote: > Dear Coordinators of the SMT-LIB and Maintainer of the SMT-LIB Benchmarks Repository, > > As a responsible for handling the submissions of benchmarks for the 2015 edition of SMT-COMP, I am contacting you to obtain informations on the procedure to get new benchmarks to the SMT-LIB repository. In particular, I would like to know if there is an official tool to check well-formedness of the benchmarks, and a standard way to decide the status of the benchmarks. > > We (the SMT-COMP organisers) have established May 1st as deadline for benchmark submissions. We would like to handle such submissions as early as possible so that any problem that may happen can be solved and have as wide a variety of benchmarks as possible for the next edition of our contest. > > Best regards, > > — David. |
From: Tjark W. <tja...@it...> - 2015-03-17 17:10:07
|
On Tue, 2015-03-17 at 18:00 +0100, Matthias Heizmann wrote: > Will it increase the chances for including the unsat core track if I submit > benchmarks for the unsat core track soon? New benchmarks certainly won't hurt; but additional expressions of interest by other users and/or solver developers would be even more persuasive in my (personal) view. Best, Tjark |
From: Matthias H. <hei...@in...> - 2015-03-17 16:59:46
|
Hi Tjark, On Tuesday 17 March 2015 17:26:33 Tjark Weber wrote: > Note that we have not yet made a final decision on whether an unsat core > track will be included in SMT-COMP this year. I know. That was the main reason for to mention that we can provide benchmarks for this track. > > When do you need these benchmarks? > > The deadline for benchmark submission (has not been finalized yet, but) > will likely be around May 1. Earlier submission is encouraged (and > appreciated). Ok, I will try to submit (at least some of them) earlier. Will it increase the chances for including the unsat core track if I submit benchmarks for the unsat core track soon? Best, Matthias |
From: Matthias H. <hei...@in...> - 2015-03-17 16:34:12
|
Hi, On Sunday 08 February 2015 16:18:21 Tjark Weber wrote: > If you have benchmarks that you think would be useful to SMT-LIB and > SMT-COMP (and may be made public), please let us know as soon as > possible, even if the material is not quite ready. We will work in > close cooperation with the SMT-LIB maintainers to include such > benchmarks in the SMT-LIB in time to be taken into account for the > competition. The deadline for benchmarks to be used in the 2015 > competition will be announced when the schedule and rules are > finalized. sorry for the late reply. I would like to contribute new benchmarks for this year's competition. I can generate benchmarks from different applications related to software verification. These include .smt2 scripts for the one-shot track, the application track and the unsat core track. (Since we have an application that relies on unsat cores, I like this track very much). Last year I already submitted benchmarks, hence I am a bit familiar with this process. I need some time to prepare the benchmarks. Especially because I would like to submit the (difficult) SMT problems that bother our tools the most. When do you need these benchmarks? Best, Matthias |
From: Tjark W. <tja...@it...> - 2015-03-17 16:26:44
|
Matthias, On Tue, 2015-03-17 at 17:18 +0100, Matthias Heizmann wrote: > I would like to contribute new benchmarks for this year's competition. Excellent. We are looking forward to receiving your benchmarks. > I can generate benchmarks from different applications related to software > verification. > These include .smt2 scripts for the one-shot track, the application track and > the unsat core track. (Since we have an application that relies on unsat > cores, I like this track very much). Note that we have not yet made a final decision on whether an unsat core track will be included in SMT-COMP this year. > When do you need these benchmarks? The deadline for benchmark submission (has not been finalized yet, but) will likely be around May 1. Earlier submission is encouraged (and appreciated). Best, Tjark |
From: Tjark W. <tja...@it...> - 2015-03-16 13:52:20
|
Dear Indranil, On Thu, 2015-02-12 at 15:40 -0500, Indranil Saha wrote: > My name is Indranil Saha. I am a postdoc with the ExCAPE project led > by Prof. Rajeev Alur. I am working on a project where the goal is to > generate motion plans for a group of robots automatically from LTL > specifications. I reduce the problem to an SMT solving problem. From > the project, I have a set of benchmarks that might be interesting for > the SMT competition. The benchmarks use linear arithmetic and equality > with uninterpreted functions. If you are interested in such > benchmarks, please let me know the process of submitting the > benchmarks and the deadline. We would be happy to take a look at your benchmarks and, if possible, integrate them into SMT-LIB in collaboration with the SMT-LIB maintainers. Please make your benchmarks available to us (e.g., by providing a URL) in SMT-LIB v2 format, and in as polished a form as possible. The deadline for submission of benchmarks to SMT-COMP 2015 will likely be around May 1. Of course, earlier submissions are welcome. Best, Tjark |
From: David D. <da...@di...> - 2015-03-16 12:33:31
|
Dear Coordinators of the SMT-LIB and Maintainer of the SMT-LIB Benchmarks Repository, As a responsible for handling the submissions of benchmarks for the 2015 edition of SMT-COMP, I am contacting you to obtain informations on the procedure to get new benchmarks to the SMT-LIB repository. In particular, I would like to know if there is an official tool to check well-formedness of the benchmarks, and a standard way to decide the status of the benchmarks. We (the SMT-COMP organisers) have established May 1st as deadline for benchmark submissions. We would like to handle such submissions as early as possible so that any problem that may happen can be solved and have as wide a variety of benchmarks as possible for the next edition of our contest. Best regards, — David. |
From: David D. <da...@di...> - 2015-03-16 12:25:29
|
Dear Indranil Saha, I am responsible to handle the benchmarks submission for the 2015 edition of SMTCOMP. I will work in cooperation with the SMT-LIB maintainers to guarantee that the submitted benchmarks are integrated in a suitable manner. Are your benchmarks already available? If so, could you make them available on the internet so that I can download them? Otherwise, the deadline for benchmark submission being May 1st, you still have plenty of time to prepare them. If you need my assistance to do so, please contact me. Best regards, — David Deharbe. > On Feb 12, 2015, at 5:40 PM, Indranil Saha <sah...@gm...> wrote: > > Hello SMTCOMP organizing team, > > My name is Indranil Saha. I am a postdoc with the ExCAPE project led by Prof. Rajeev Alur. I am working on a project where the goal is to generate motion plans for a group of robots automatically from LTL specifications. I reduce the problem to an SMT solving problem. From the project, I have a set of benchmarks that might be interesting for the SMT competition. The benchmarks use linear arithmetic and equality with uninterpreted functions. If you are interested in such benchmarks, please let me know the process of submitting the benchmarks and the deadline. > > Thanks, > Indranil Saha > ------------------------------------------------------------------------------ > 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 |
From: Indranil S. <sah...@gm...> - 2015-02-12 20:40:34
|
Hello SMTCOMP organizing team, My name is Indranil Saha. I am a postdoc with the ExCAPE project led by Prof. Rajeev Alur. I am working on a project where the goal is to generate motion plans for a group of robots automatically from LTL specifications. I reduce the problem to an SMT solving problem. From the project, I have a set of benchmarks that might be interesting for the SMT competition. The benchmarks use linear arithmetic and equality with uninterpreted functions. If you are interested in such benchmarks, please let me know the process of submitting the benchmarks and the deadline. Thanks, Indranil Saha |
From: Tjark W. <tja...@it...> - 2015-02-11 15:19:16
|
Christoph, On Wed, 2015-02-11 at 14:20 +0000, Christoph Wintersteiger wrote: > 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? I think this is an excellent suggestion. I reckon the next step would be for you to make these benchmarks available to us, so that they can be reviewed and (hopefully) incorporated into SMT-LIB. Best, Tjark |
From: Christoph W. <cw...@mi...> - 2015-02-11 14:20:32
|
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<http://research.microsoft.com/people/cwinter> [MSFT_logo_Gray DE sized SIG1.png] 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 |
From: Tjark W. <tja...@it...> - 2015-02-08 15:37:15
|
====================================================================== 10th International Satisfiability Modulo Theories Competition (SMT-COMP'15) July 19, 2015 San Francisco, USA CALL FOR COMMENTS CALL FOR BENCHMARKS PRELIMINARY CALL FOR SOLVERS ====================================================================== SMT-COMP is the annual competition among Satisfiability Modulo Theories (SMT) solvers. The goals of SMT-COMP are to spur solver advances, collect benchmarks, and encourage adoption of the SMT-LIB standard, through friendly competition. SMT-COMP'15 will end in time to be described and the results announced at the SMT Workshop (July 18-19), which is affiliated with the 27th International Conference on Computer Aided Verification (CAV 2015). SMT-COMP'15 is organized under the direction of the SMT Steering committee. The organizing team for SMT-COMP'15 is . Sylvain Conchon - Paris-Sud University, France . David Deharbe - Federal University of Rio Grande do Norte, Brazil . Tjark Weber - Uppsala University, Sweden This is a call for three things: CALL FOR COMMENTS: The organizing team is preparing the schedule and rules for 2015. Any comments you may have to improve the competition over past years or to redirect its focus are welcome and will be considered by the team. Please submit such comments by *** 22 February 2015. *** For SMT-COMP'15, we are particularly interested in comments regarding: - Sequential vs. parallel performance: All solvers will have several CPU cores available, and we plan to measure CPU and wall time. Solver developers might wish to prepare both sequential and parallel versions of their solvers. - Benchmark selection: We will likely have sufficient computational resources to run all solvers on all eligible benchmarks. Therefore, we are interested in proposals for weighing the results so as to avoid over-representation of certain (large) benchmark families. - Scope: After the successful migration to StarExec in 2013/14, we are considering to broaden the scope of SMT-COMP again. We might reinstate additional tracks, e.g., for unsat core extraction and proof-producing solvers. CALL FOR BENCHMARKS: The competition is enhanced by new sets of benchmarks to add to those already in use (and used in past competitions). A selection of benchmarks in various categories is used for the competition (according to rules that are currently being revised). If you have benchmarks that you think would be useful to SMT-LIB and SMT-COMP (and may be made public), please let us know as soon as possible, even if the material is not quite ready. We will work in close cooperation with the SMT-LIB maintainers to include such benchmarks in the SMT-LIB in time to be taken into account for the competition. The deadline for benchmarks to be used in the 2015 competition will be announced when the schedule and rules are finalized. PRELIMINARY CALL FOR SOLVERS: A submission deadline for solvers will be announced along with the rules. However, it is useful to the organizing team to know in advance which and how many solvers may be entering. Thus we request that you let us know at your earliest convenience if you think you may be submitting one or more solvers to SMT-COMP'15, particularly if you think there may be unusual circumstances. COMMUNICATION: The competition web-site will be at www.smtcomp.org. Public email regarding the competition may be sent to smt...@cs.... Announcements will be sent on both smt...@cs... and sm...@cs.... Email to the organizers only may be sent to smt...@li... Sincerely, The organizing team |
From: David R. C. <dc...@gr...> - 2014-11-06 16:05:01
|
SMTCOMP 2014 participants The organizers are preparing a paper for publication on the experience and results of the 2014 SMT competition. This includes a list of participating solvers. If you have a 'canonical' reference you would like us to use for your solver, or the most appropriate one for the 2014 version (which might be a paper in preparation or under review), please reply to this note with a BibTex for your tool. ASAP - our submission deadline is next week. Thanks, David, David & Tjark |
From: David D. <dav...@lo...> - 2014-08-04 13:17:45
|
David, Your answer includes all the remarks that I could have made. Best regards, -- David. On Aug 2, 2014, at 1:34 PM, co...@fr... wrote: > Tjark, David, > > This is what I sent Aaron - I should have asked for your input, but in my eagerness to get this off my plate, I just sent it without thinking. Additional comments are welcome and I'll amend the response. > > - David > > > ----- Forwarded Message ----- > From: "co...@fr..." <co...@fr...> > To: Aaron Stump <aar...@ui...> > Sent: Wednesday, July 30, 2014 3:05 PM > Subject: Re: StarExec competitions '14 questionnaire > > Feel free to send follow-up questions if you need more detail. > > - David > > > > > From: Aaron Stump <aar...@ui...> > To: Martina Seidl <mar...@jk...>; Harald Roman Zankl <Har...@ui...>; Dana Fisman <fi...@se...>; Rishabh Singh <ri...@cs...>; Skip (Charles) Jordan <sk...@is...>; David Cok <co...@fr...>; Geoff Sutcliffe <ge...@cs...>; Johannes Waldmann <joh...@ht...>; Tjark Weber <tja...@it...>; David Deharbe <dav...@lo...> > Cc: "Tinelli, Cesare" <ces...@ui...> > Sent: Monday, July 28, 2014 2:15 PM > Subject: StarExec competitions '14 questionnaire > > Dear Summer 2014 competition organizers, > > Now that all your events have concluded -- and things have consequently > calmed down a bit for the StarExec team! -- we are writing to ask for > your feedback on the system and your experience using it this summer for > your competitions. Many of you have already offered feedback in various > forms, for which we are grateful. And the data you supplied Cesare for > his talk about StarExec at IJCAR was also very helpful. Appreciative of > your patience with more requests for feedback, we are asking for your > responses to the questions below, to try to get even more specific > guidance and make plans for the future. We have to turn in a report at > the end of August to the government funders, so we would be very > grateful if you could give us your responses within, say, one week (so > please return to us by August 5th, if possible). If vacation time and > such prevents that, then please just get us your responses whenever you > can, as they will be valuable regardless of whether they arrive in time > for our report or not. > > Best wishes, and thanks in advance, > Aaron & Cesare > -------------------------------------------------------------------- > Questionnaire for organizers of Summer 2014 competitions running on StarExec > > 1. What is the full official name of your competition, and what are the > names and affiliations of all the organizers? > > 2. What are all the StarExec job ids for jobs that were part of your > competition? > > 3. Are those competition jobs currently publicly visible on StarExec > (i.e., in a public space -- you can make a space public with one of the > actions at the bottom of the page on the space explorer)? > > 4. What were the advantages and disadvantages of using StarExec for you > as competition organizer, in comparison with whatever alternative you > would have utilized instead of StarExec? > > 5. What were the most positive aspects of your experience running your > competition on StarExec? > > 6. What were the negative aspects? > > 7. Roughly how many questions would you estimate you fielded about > StarExec from participants in your competition? > > 8. Did you use StarExec's pages for viewing job results, or did you > create your own web display for showing the data from StarExec? > > 9. (Very) roughly what percentages of your interactions with StarExec > for organizing the competition were through the web interface, through > StarExecCommand, and through other browser-free interaction with the > StarExec web server (e.g., sending POST and GET requests directly to > StarExec URLs)? > > 10. Where do you think we should focus our development efforts going > forward? A few of the things we are considering are: additional > interfaces for viewing job results (maybe similar to the 2-dimensional > grid used in Termination; other suggestions?), solver pipelines (output > from one stage becomes benchmark for input to the next stage; other > details to be determined), more work to make it possible to install and > run StarExec on your own server or computer (abstract out > security-critical details, installation documention, and abstract the > interface to GridEngine so you can use a different third-party tool to > run jobs on a cluster, or even just your own desktop), commitment to and > documentation of the URLs used for communicating directly with the server. > > 11. Do you expect you or your colleagues will likely want to run the > next edition of your competition on StarExec? > > 12. How adequate was the help you were able to get either directly from > the StarExec team or from the forum? > > 13. How satisfied do you perceive the participants in your competition > were with their experience using StarExec? > > 14. Were there any recurring issues or complaints from the participants > in your competition? > > 15. Any further comments or suggestions? > > > > > <StarExecQuestionnaire-SMTCOMP.rtf>------------------------------------------------------------------------------ > Want fast and easy access to all the code in your enterprise? Index and > search up to 200,000 lines of code with a free copy of Black Duck > Code Sight - the same software that powers the world's largest code > search on Ohloh, the Black Duck Open Hub! Try it now. > http://p.sf.net/sfu/bds_______________________________________________ > Smtcomp-discussion mailing list > Smt...@li... > https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion |
From: <co...@fr...> - 2014-06-29 17:09:31
|
Thanks, I have a mailing list I use, which is all the people listed on the participants web page. That should be the same as one of the emails to all participants. - David ________________________________ From: David Deharbe <dav...@lo...> To: smt...@li... Sent: Sunday, June 29, 2014 12:22 PM Subject: [Smtcomp-discussion] Fwd: Social event, T-shirts. Hello, I have already sent an email to the SMTCOMP contestants informing them about the dinner and inviting them to register. But I am not sure that I have joined them all (I copied the list of destinataries of one of the emails sent by David). Is there an "official" list of emails that I could use for that matter? Also I assumed that we do not have financial resources to pay for the participants, so I informed the participants each would pay his expenses. Best regards, -- David. ------------------------------------------------------------------------------ Open source business process management suite built on Java and Eclipse Turn processes into business applications with Bonita BPM Community Edition Quickly connect people, data, and systems into organized workflows Winner of BOSSIE, CODIE, OW2 and Gartner awards http://p.sf.net/sfu/Bonitasoft _______________________________________________ Smtcomp-discussion mailing list Smt...@li... https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion |
From: David D. <dav...@lo...> - 2014-06-29 16:23:04
|
Hello, I have already sent an email to the SMTCOMP contestants informing them about the dinner and inviting them to register. But I am not sure that I have joined them all (I copied the list of destinataries of one of the emails sent by David). Is there an "official" list of emails that I could use for that matter? Also I assumed that we do not have financial resources to pay for the participants, so I informed the participants each would pay his expenses. Best regards, -- David. |
From: David D. <dav...@lo...> - 2014-06-29 16:15:18
|
Dear SMTCOMP contestants, We are proposing to have a SMTCOMP dinner at the Feuerwehr Wagner Heuriger (i.e. traditional Austrian young wine oriented restaurant): http://www.feuerwehrwagner.at/ It will be on Friday, 18th of July, starting around 19:15. It is buffet with various Austrian specialties for 22 euros per person (drinks not included, and each participant will pay for himself). Note that this restaurant is 30 minutes away from the conference venue via public transportation.. On the other hand, the "Heuriger"neighbourhood (known as "Grinzing" and close to the vineyards of Vienna) also counts as a minor, off the beaten track, touristic attraction in Vienna. We are organizing this event together with the APPA, CASC and QED workshops. If you are planning to participate, please add your name to the following doodle: http://doodle.com/qzys8sanskqiss45. See you in Vienna! Best regards, -- David Deharbe. |
From: David D. <dav...@lo...> - 2014-06-29 16:04:40
|
Hello, I will send an email to the list of SMTCOMP contestants with a link to a doodle where the interested people have to add their name. I assume that we have no fund to invite the participants of SMTCOMP for the dinner, and each participant will pay for its dinner. Best regards, -- David. On Jun 28, 2014, at 1:54 AM, David Cok <co...@fr...> wrote: > David > > - Please look into joining in a social event - we joined in with the CASC dinner in 2012, as I recall. I expect you would inquire of Geoff. > > - As for T-shirts - they were some work and expense in 2012, and I'm not sure of the benefit - but am willing to hear discussion. > > David > > On 6/27/14 3:31 AM, David Deharbe wrote: >> David, Tjark, >> >> Pascal Fontaine asked me whether there would be a social event for SMT-COMP. The APPA and CASC dinners are already co-located (see information hereafter), and Bruno Wolzenlogel Paleo asked him if the SMT-COMP community would like to join them. Another suggestion Pascal made is to have T-shirts for the competitors (I think that TPTP has this tradition). >> >> The date for the dinner does not appear in the messages below; Pascal told me it would be on the second day of the workshops (July 18th). >> >> What do you think? >> >> Best regards, >> >> -- David. >> >> Begin forwarded message: >> >> >>> From: Pascal Fontaine <Pas...@in...> >>> >>> Subject: Fwd: Fwd: ?X.X?: APPA: Social Event >>> Date: June 27, 2014 at 9:20:54 AM GMT+2 >>> To: David Deharbe >>> <de...@gm...> >>> >>> >>> Signed PGP part >>> For your information. >>> >>> T-shirts are great, and there is still time to organize a quick call >>> for drawings (alternatively, you can recycle a previous one and >>> adapt). We could reception the T-shirts at our apartment, or pick >>> them the week before the SMT workshop. >>> >>> Best, >>> >>> Pascal >>> >>> >>> -------- Original Message -------- >>> Subject: Fwd: ?X.X?: APPA: Social Event >>> Date: Wed, 25 Jun 2014 08:41:23 +0200 >>> From: Bruno Woltzenlogel Paleo >>> <bru...@gm...> >>> >>> To: Pascal Fontaine >>> <Pas...@in...> >>> >>> CC: David Delahaye >>> <dav...@cn...> >>> >>> >>> Hi Pascal! >>> >>> If the SMT community would like to co-locate the SMT-Comp dinner with >>> the APPA and CASC dinners, let me know. >>> >>> Best regards, >>> >>> Bruno >>> >>> >>> >>> Begin forwarded message: >>> >>> >>>> From: Bruno Woltzenlogel Paleo <bru...@gm...> >>>> Subject: Re: >>>> ?X.X?: APPA: Social Event Date: 25 Jun 2014 8:39:33 GMT+2 To: Geoff >>>> Sutcliffe >>>> <ge...@cs...> >>>> Cc: David Delahaye >>>> >>>> <dav...@cn...>, Stephan Schulz <sc...@ep...> >>>> , >>>> Clark Barrett >>>> <ba...@cs...> >>>> , Pascal Fontaine >>>> >>>> <Pas...@in...> >>>> >>>> >>>> Hi Geoff, >>>> >>>> On 19 Jun 2014, at 14:39 , Geoff Sutcliffe >>>> <ge...@cs...> >>>> >>>> wrote: >>>> >>>> >>>>>> If you like this idea, I could already make a pre-reservation >>>>>> for about 30 people (20 for CASC and 10 for APPA), and later >>>>>> we could compute the exact numbers of participants. >>>>>> >>>>> Great - go for it! Let me know what time, etc. Thanks for >>>>> organizing! >>>>> >>>> Done. It will be at 18:30 in Heuriger Feuerwehr Wagner >>>> ( >>>> http://www.feuerwehrwagner.at/ >>>> ). The food will cost 22 euros per >>>> person and will consist of a buffet with typical Austrian food. >>>> Drinks are not included >>>> ( >>>> http://www.feuerwehrwagner.at/buffet/getraenkekarte.pdf >>>> ). >>>> >>>> When do you think you will know the exact number of participants of >>>> the CASC dinner? >>>> >>>> Best regards, >>>> >>>> Bruno >>>> >>> >>> >>> >>> >> >> >> ------------------------------------------------------------------------------ >> Open source business process management suite built on Java and Eclipse >> Turn processes into business applications with Bonita BPM Community Edition >> Quickly connect people, data, and systems into organized workflows >> Winner of BOSSIE, CODIE, OW2 and Gartner awards >> >> http://p.sf.net/sfu/Bonitasoft >> >> >> _______________________________________________ >> Smtcomp-discussion mailing list >> >> Smt...@li... >> https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion > > ------------------------------------------------------------------------------ > Open source business process management suite built on Java and Eclipse > Turn processes into business applications with Bonita BPM Community Edition > Quickly connect people, data, and systems into organized workflows > Winner of BOSSIE, CODIE, OW2 and Gartner awards > http://p.sf.net/sfu/Bonitasoft_______________________________________________ > Smtcomp-discussion mailing list > Smt...@li... > https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion |
From: David C. <co...@fr...> - 2014-06-27 23:54:56
|
David - Please look into joining in a social event - we joined in with the CASC dinner in 2012, as I recall. I expect you would inquire of Geoff. - As for T-shirts - they were some work and expense in 2012, and I'm not sure of the benefit - but am willing to hear discussion. David On 6/27/14 3:31 AM, David Deharbe wrote: > David, Tjark, > > Pascal Fontaine asked me whether there would be a social event for SMT-COMP. The APPA and CASC dinners are already co-located (see information hereafter), and Bruno Wolzenlogel Paleo asked him if the SMT-COMP community would like to join them. Another suggestion Pascal made is to have T-shirts for the competitors (I think that TPTP has this tradition). > > The date for the dinner does not appear in the messages below; Pascal told me it would be on the second day of the workshops (July 18th). > > What do you think? > > Best regards, > > -- David. > > Begin forwarded message: > >> From: Pascal Fontaine <Pas...@in...> >> Subject: Fwd: Fwd: ?X.X?: APPA: Social Event >> Date: June 27, 2014 at 9:20:54 AM GMT+2 >> To: David Deharbe <de...@gm...> >> >> Signed PGP part >> For your information. >> >> T-shirts are great, and there is still time to organize a quick call >> for drawings (alternatively, you can recycle a previous one and >> adapt). We could reception the T-shirts at our apartment, or pick >> them the week before the SMT workshop. >> >> Best, >> >> Pascal >> >> >> -------- Original Message -------- >> Subject: Fwd: ?X.X?: APPA: Social Event >> Date: Wed, 25 Jun 2014 08:41:23 +0200 >> From: Bruno Woltzenlogel Paleo <bru...@gm...> >> To: Pascal Fontaine <Pas...@in...> >> CC: David Delahaye <dav...@cn...> >> >> Hi Pascal! >> >> If the SMT community would like to co-locate the SMT-Comp dinner with >> the APPA and CASC dinners, let me know. >> >> Best regards, >> >> Bruno >> >> >> >> Begin forwarded message: >> >>> From: Bruno Woltzenlogel Paleo <bru...@gm...> Subject: Re: >>> ?X.X?: APPA: Social Event Date: 25 Jun 2014 8:39:33 GMT+2 To: Geoff >>> Sutcliffe <ge...@cs...> Cc: David Delahaye >>> <dav...@cn...>, Stephan Schulz <sc...@ep...>, >>> Clark Barrett <ba...@cs...>, Pascal Fontaine >>> <Pas...@in...> >>> >>> Hi Geoff, >>> >>> On 19 Jun 2014, at 14:39 , Geoff Sutcliffe <ge...@cs...> >>> wrote: >>> >>>>> If you like this idea, I could already make a pre-reservation >>>>> for about 30 people (20 for CASC and 10 for APPA), and later >>>>> we could compute the exact numbers of participants. >>>> Great - go for it! Let me know what time, etc. Thanks for >>>> organizing! >>> Done. It will be at 18:30 in Heuriger Feuerwehr Wagner >>> (http://www.feuerwehrwagner.at/). The food will cost 22 euros per >>> person and will consist of a buffet with typical Austrian food. >>> Drinks are not included >>> (http://www.feuerwehrwagner.at/buffet/getraenkekarte.pdf). >>> >>> When do you think you will know the exact number of participants of >>> the CASC dinner? >>> >>> Best regards, >>> >>> Bruno >> >> >> > > > ------------------------------------------------------------------------------ > Open source business process management suite built on Java and Eclipse > Turn processes into business applications with Bonita BPM Community Edition > Quickly connect people, data, and systems into organized workflows > Winner of BOSSIE, CODIE, OW2 and Gartner awards > http://p.sf.net/sfu/Bonitasoft > > > _______________________________________________ > Smtcomp-discussion mailing list > Smt...@li... > https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion |
From: David D. <de...@gm...> - 2014-06-27 07:32:11
|
David, Tjark, Pascal Fontaine asked me whether there would be a social event for SMT-COMP. The APPA and CASC dinners are already co-located (see information hereafter), and Bruno Wolzenlogel Paleo asked him if the SMT-COMP community would like to join them. Another suggestion Pascal made is to have T-shirts for the competitors (I think that TPTP has this tradition). The date for the dinner does not appear in the messages below; Pascal told me it would be on the second day of the workshops (July 18th). What do you think? Best regards, -- David. Begin forwarded message: > From: Pascal Fontaine <Pas...@in...> > Subject: Fwd: Fwd: ?X.X?: APPA: Social Event > Date: June 27, 2014 at 9:20:54 AM GMT+2 > To: David Deharbe <de...@gm...> > > Signed PGP part > For your information. > > T-shirts are great, and there is still time to organize a quick call > for drawings (alternatively, you can recycle a previous one and > adapt). We could reception the T-shirts at our apartment, or pick > them the week before the SMT workshop. > > Best, > > Pascal > > > -------- Original Message -------- > Subject: Fwd: ?X.X?: APPA: Social Event > Date: Wed, 25 Jun 2014 08:41:23 +0200 > From: Bruno Woltzenlogel Paleo <bru...@gm...> > To: Pascal Fontaine <Pas...@in...> > CC: David Delahaye <dav...@cn...> > > Hi Pascal! > > If the SMT community would like to co-locate the SMT-Comp dinner with > the APPA and CASC dinners, let me know. > > Best regards, > > Bruno > > > > Begin forwarded message: > > > From: Bruno Woltzenlogel Paleo <bru...@gm...> Subject: Re: > > ?X.X?: APPA: Social Event Date: 25 Jun 2014 8:39:33 GMT+2 To: Geoff > > Sutcliffe <ge...@cs...> Cc: David Delahaye > > <dav...@cn...>, Stephan Schulz <sc...@ep...>, > > Clark Barrett <ba...@cs...>, Pascal Fontaine > > <Pas...@in...> > > > > Hi Geoff, > > > > On 19 Jun 2014, at 14:39 , Geoff Sutcliffe <ge...@cs...> > > wrote: > > > >>> If you like this idea, I could already make a pre-reservation > >>> for about 30 people (20 for CASC and 10 for APPA), and later > >>> we could compute the exact numbers of participants. > >> > >> Great - go for it! Let me know what time, etc. Thanks for > >> organizing! > > > > Done. It will be at 18:30 in Heuriger Feuerwehr Wagner > > (http://www.feuerwehrwagner.at/). The food will cost 22 euros per > > person and will consist of a buffet with typical Austrian food. > > Drinks are not included > > (http://www.feuerwehrwagner.at/buffet/getraenkekarte.pdf). > > > > When do you think you will know the exact number of participants of > > the CASC dinner? > > > > Best regards, > > > > Bruno > > > > |
From: Tjark W. <tja...@it...> - 2014-06-23 11:41:08
|
Bruno, On Fri, 2014-06-13 at 10:33 -0700, Bruno Dutertre wrote: > Whichever way we define the semantics of divide by zero. This will > always be a corner case and I doubt we can get a definition that > will immediately satisfy every user. I agree. > Saying that (bvdiv x 0) should be undefined may be convenient and > familiar for people in the Isabelle/HOL world but they are many other > users outside this world. Who is to say that (bvdiv x 0x000) = 0xfff is > incorrect for them? Nobody, of course. At present, users who want (bvdiv x 0x000) = 0xfff can easily assert this. But it makes little sense, other than for implementation reasons, to impose this equality on every user. > The best choice is to provide a basic semantics that is clear and > easy to support, so that the tools actually implement it. Users > who want something else can easily encode whatever they need on > top of that by using the (define-fun ..) commands of SMT-LIB. > It is straightforward to encode the 'div-by-zero is undefined' > semantics by moving to the QF_UFBV or UFBV logics. These logics > are very appropriate for this purpose. This -- users who want something else can easily encode it -- is true no matter how bvdiv is defined. But for users to provide their own encoding, they must be aware of the issue in the first place. For the soundness of models that unwary users build, it is much safer to have a weak semantics by default than to have one that makes potentially surprising assumptions about a corner case. Of course, I fully understand your argument that the current semantics is awkward to implement and basically requires UF support. Best, Tjark |