Installing

This library can be installed via OPAM.

Building

This project uses Dune as a build tool. After cloning this repository, it should be sufficient to perform the following steps:

1. Install dependencies.

`opam install jbuilder batteries jhupllib monadlib ocaml-monadic ppx_deriving ppx_deriving_yojson yojson`

1. Build the project.

`make && make test`

Performance Foci

This library aims to answer reachability queries quickly even on very large push-down systems. The following points were taken into consideration in pursuit of this goal:

• The user specifies how transitions may be computed for each state and arriving stack element and generally does not add states or transitions directly. The library will construct only the part of the PDS necessary to answer the presented reachability questions.
• The transitions themselves are abstracted via "dynamic pop" functions. A "dynamic pop" edge is permitted to compute how a transition should proceed based upon the top element of the stack. This is useful, for instance, to encode a step which checks that the top element of the stack is not a particular value: rather than enumerating stack elements which may be popped and then re-pushed, a single dynamic pop can address all of these cases.
• The reachability analysis can reuse the information it gathers over multiple queries. The same query performed on the same structure twice will, the second time it is made, take on the order of constant time to answer. Queries which rely upon similar proofs or otherwise overlap in their reachability closure can share work.