PV4 Z3str3RE:part of Z3, produces a satisfiability result for a set of constrains

Application domain/field

Type of tool

Algorithm for SMT solving

Internals

Implemented as part of Z3 for solving regex constraints and linear integer arithmetic over length of string terms.
SMT

Links

Artifact/reproduction package for CAV '21 paper: https://figshare.com/s/5ae73a6f3c55f5c5e4c1

Related papers

https://doi.org/10.1007/978-3-030-81688-9_14 (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.