This library provides functions to compute finite automata for the set
of forwards or backwards reachable configurations in a weighted
pushdown system, and for the recovery of witness sets. The interested
programmer may make use of this library in other programs.
The theory behind weighted pushdown systems is explained in
(long, complete version) and
this conference paper (short, abridged version).
The library is written and maintained by
Stefan Schwoon, with contributions from
and Somesh Jha.
- 24.03.2003: First public release
- 15.05.2003: Bugfix in sat_add_rule_post (thanks to David Melski),
moved WPDS homepage to present location
- 06.04.2004: Complete overhaul of the code and new functionality.
- 16.05.2006: New release with better trace generation etc,
see Readme for details.