• Small Example short.sal
• Peterson's Protocol peterson.sal
• Synchronous Bus Arbiter arbiter.sal
• Bounded Bakery Protocol bakery.sal
• Bakery Protocol inf-bakery.sal
• Simpson's Protocol description, fourslot.sal
• Fischer's Protocol description, fischer.sal
• Stack description, stack.sal
• Priority Ceiling Protocol description, set.sal, math.sal, pcp_task.sal, pcp_rsrc.sal, pcp_scheduler.sal, pcp_generic.sal, tst_pcp_generic.sal, tst_pcp_generic2.sal
• Needham-Schroeder Protocol description, network.sal, needhamschroeder.sal
• Queue Lock Protocol description, qlock1.sal, qlock2.sal, qlock3.sal
• Suzuki-Kasami Distributed Mutual Exclusion Algorithm description, skdmxa.sal, fix_skdmxa.sal, inf_skdmxa.sal
• Ultra*log ultralog.sal, ultralog_light.sal,