PV1 nonreachdetermines whether a problem for a rewrite system is nonreachable or infeasible

nonreach is an automated tool for nonreachability analysis that is intended as a drop-in addition to existing termination and confluence tools for term rewriting

Application domain/field

Type of tool

Nonreachability tool

Expected input

Format:

Expected output

NO if nonreachability can be established for the problem. YES if it was given an infeasibility problem which is infeasible. MAYBE or TIMEOUT otherwise.

Internals

nonreach has been made to be a back end for reachability analysis tools.

Links

Repository: https://bitbucket.org/fmessner/nonreach/src/master/

Last commit date

6 December 2020

Related papers

https://doi.org/10.1007/978-3-030-17462-0_19 (TACAS '19)

Last publication date

4 April 2019

ProVerB specific

View/edit source (Markdown)



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