Databases
StackOverflow2013
Postsdbo
POSMT solvers for bit vector arithmetic
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POSMT solvers for bit vector arithmetic
    primarykey
    data
    text
    <p>I'm planning some experiments in symbolic execution of C code, using an off-the-shelf SMT solver, and wondering which solver to use; looking at e.g. the SMT contest entrants, and taking only the open-source systems, narrows it down to Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; which is still a long list.</p> <p>Trying to narrow it down a little further, I notice that some of the systems advertise the ability to handle bit vector arithmetic, whereas others only advertise the ability to handle general integer arithmetic. In principle, the former is correct for C, where variables are machine words, not unbounded integers. How much difference does it make in practice? What happens if you try to use a general integer system for this kind of job? Does one of the following scenarios apply?</p> <ol> <li><p>A bit vector system is slightly more efficient, but you can use either, no problem.</p></li> <li><p>You can use a general integer system with a bit of tweaking.</p></li> <li><p>A general integer system is fine for signed int (because the result of overflow is undefined) but will give the wrong answer for unsigned.</p></li> <li><p>A general integer system just isn't correct for machine word arithmetic, and I can reduce my short list to only those systems that provide bit vector arithmetic.</p></li> <li><p>Something else...?</p></li> </ol> <p>I've tried to ask as specific a question as possible, but if anyone can suggest any other criteria for narrowing down the list, that would be great!</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. This table or related slice is empty.
    1. USrwallace
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    2. PO
      singulars
      1. PTAnswer
    1. VO
      singulars
      1. POSMT solvers for bit vector arithmetic
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. POSMT solvers for bit vector arithmetic
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. POSMT solvers for bit vector arithmetic
      1. USGrzegorz Wierzowiecki
      1. VTFavorite
    1. This table or related slice is empty.
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload