- Driscoll, Thakur, and Reps, OpenNWA: A Nested-Word-Automaton Library [draft PDF], To appear: CAV 2012.
- Driscoll, Thakur, Burton, and Reps, WALi: Nested-Word Automata, UW TR #1675 (2011). (The TR proper is now out-of-date. A version is kept up-to-date in the OpenNWA/WALi distribution in the Doc/ directory, and is available here, now re-titled.)
- Thakur, Lim, Lal, Burton, Driscoll, Elder, Anderson, and Reps, Directed Proof Generation for Machine Code, CAV '10. [PDF]. Expanded version available as UW TR #1669 (2010) [PDF].
- Driscoll, Burton, and Reps, Checking Conformance of a Producer and a Consumer, FSE '11. [PDF]
- Fredrikson, Joiner, Jha, Reps, Porras, Sadi, and Yegneswaran, Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement, under submission.
NWA fundamentals and external references
The fundamentals of NWAs were worked out by Alur and Madhusudan. They originally presented Visibly Pushdown Automata (VPAs), a closely related formalism, then developed Nested Word Automata as they are implemented in OpenNWA, and finally better unified the two models with an expanded definition of NWAs. (Though not more powerful in terms of language acceptance, the expanded definition allows NWAs which may be more compact. However, OpenNWA uses the original definition from the DLT paper, which would later be known as a weakly-hierarchical, linearly-accepting NWA. The more restrictive formalism has benefits; in particular, many of the closure operations require "lowering" the input NWAs to the restricted form.)
Both Alur and Madhusudan maintain a bibliography of papers related to VPAs and NWAs. They have received a lot of attention over the last few years, both for applications and theoretical results.