Static Analysis of Hurd Source Code?

[Rauf Salimi Khaligh]

Dear Hurd People,

I am currently doing research on static analysis algorithms for parallel
programs, and I am collecting large multi-threaded programs based on
"POSIX-like" threading and synchronization primitives.I will use these
programs as  benchmarks and the results will be published in my Master's
Thesis. I am not much familiar with hurd internals.so before getting
involved : is the latest version of Hurd based on pthreads? Has there been
any previous work on static analysis or formal verification of Hurd?

I would appreciate any comments.

Best Regards,

Rauf Salimi Khaligh

Faculty of Computer Science
Institute of Software Technology
University of Stuttgart
Germany