She earned her doctorate in computer science from the University of Wisconsin–Madison in 1976 under the name Pamela Zave Smith; her thesis, "Functional equivalence of parallel processes", was supervised by Donald R.
[6] In collaboration with Michael A. Jackson, Zave created the set of definitions and reasoning obligations that have become known as the standard model for requirements engineering.
[10] An implementation of DFC was used to build the features for CallVantage (SM), AT&T's first voice-over-IP service, which became publicly available in 2004 and served approximately 100,000 customers world-wide.
[11][12] After CallVantage the DFC implementation was used to build a teleconferencing system used internally by AT&T, which for some time supported millions of user minutes each work day.
[2] Zave's work on finding bugs in the Chord protocol[16] and proving a modified version correct[17] has been credited by engineers in Amazon Web Services for convincing them to start using formal methods on real distributed systems.