Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Weighted PDS library



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 this article (long, complete version) and this conference paper (short, abridged version).



The library is written and maintained by Stefan Schwoon, with contributions from Thomas Reps 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.