Predicate Abstraction Examples

Here is a list of examples that have been frequently cited in papers about predicate abstraction and other related topics.

• AlternatingBitProtocol
• BakeryMutualExclusion
• BoundedRetransmissionProtocol
• BurnsMutualExclusion
• CacheCoherence
• DijkstraMutualExclusion
• MuxAstProtocol
• PetersonMutualExclusion
• SifakisMutualExclusion
• SemaphoreMutualExclusion
• TicketMutualExclusion
• TarSimple
• TarProducerConsumer
• TimeVarying

Here are some larger examples that we have applied predicate abstraction to:

• On-The-Fly Garbage Collection
• FLASH Cache Coherence
• IBM Cache Coherence
• Secure Contract Signing
• AODV Routing Protocol