POPL'24 Tutorial: String Solving for Verification

OSTRICH is an SMT solver for string constraints. Constraints for OSTRICH can be written using a superset of a subset of the SMT-LIB string theory. For more details, see the OSTRICH github page.

Load a predefined example: ... or enter some formulas:

Send given input to OSTRICH
Save input on the server and make it available through a private link
   
Enable incremental SMT-LIB processing
 
Output models/ countermodels
 
Use Parikh images as a heuristic to detect unsatisfiability of equations
      Backend:
OSTRICH back-end to apply to this problem
  Propagation:
Direction of constraint propagation to apply (only for standard back-end)