diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -1,10 +1,16 @@
 -- | ImProve examples.
 module Language.ImProve.Examples
-  ( gcd'
-  , gcdMain
-  , buildGCD
+  ( buildGCD
   , counter
   , verifyCounter
+  , arbiterSpec
+  , arbiter
+  , arbiter1
+  , arbiter2
+  , arbiter3
+  , verifyArbiters
+  , buildArbiters
+  , runAll
   ) where
 
 import Language.ImProve
@@ -70,9 +76,126 @@
   assert "LessThan10"            $ ref counter <.  10
 
   -- Implementation.
-  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (incr counter)
+  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
 
--- Verify the 'counter' example.
+  -- Alternatives to try.
+  --ifelse "ResetCounter" (ref counter >=. 9) (counter <== 0) (counter <== ref counter + 1)
+  --ifelse "ResetCounter" (ref counter >=. 9 ||. ref counter <. 0)  (counter <== 0) (counter <== ref counter + 1)
+
+-- | Verify the 'counter' example.
 verifyCounter :: IO ()
 verifyCounter = verify "yices" 20 counter
+
+
+
+-- | Arbiter specification.
+arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
+arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
+
+  -- Mutual exclusion.  At most, only one requester granted at a time.
+  assert "OneHot" $      grantA &&. not_ grantB &&. not_ grantC
+                ||. not_ grantA &&.      grantB &&. not_ grantC
+                ||. not_ grantA &&. not_ grantB &&.      grantC
+                ||. not_ grantA &&. not_ grantB &&. not_ grantC
+  
+  -- No grants without requests.
+  assert "NotRequestedA" $ imply (not_ requestA) (not_ grantA)
+  assert "NotRequestedB" $ imply (not_ requestB) (not_ grantB)
+  assert "NotRequestedC" $ imply (not_ requestC) (not_ grantC)
+
+  -- Grants to single requests.
+  assert "OnlyRequestA" $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA
+  assert "OnlyRequestB" $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB
+  assert "OnlyRequestC" $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC
+
+  -- Priority.
+  assert "Highest" $ imply requestA grantA
+  assert "Medium"  $ imply (not_ requestA &&. requestB) grantB
+  assert "Lowest"  $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC
+
+-- | An arbiter implementation.
+arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
+arbiter1 (requestA, requestB, requestC) = do
+  let grantA = requestA
+      grantB = requestB
+      grantC = requestC
+  return (grantA, grantB, grantC)
+
+-- | An another arbiter implementation.
+arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
+arbiter2 (requestA, requestB, requestC) = do
+  grantA <- bool "grantA" False
+  grantB <- bool "grantB" False
+  grantC <- bool "grantC" False
+
+  if_ "GrantA" (requestA)                                     (grantA <== true)
+  if_ "GrantB" (not_ requestA &&. requestB)                   (grantB <== true)
+  if_ "GrantC" (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
+
+  return (ref grantA, ref grantB, ref grantC)
+
+-- | Yet another arbiter implementation.
+arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
+arbiter3 (requestA, requestB, requestC) = do
+  let grantA = requestA
+      grantB = not_ requestA &&. requestB
+      grantC = not_ requestA &&. not_ requestB &&. requestC
+  return (grantA, grantB, grantC)
+
+-- | Binding an arbiter implemenation to the arbiter specification.
+arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
+arbiter name implementation = scope name $ do
+  -- Create input variables.
+  requestA <- input bool "requestA"
+  requestB <- input bool "requestB"
+  requestC <- input bool "requestC"
+  let requests = (requestA, requestB, requestC)
+
+  -- Instantiate implementation.
+  grants@(grantA, grantB, grantC) <- scope "impl" $ implementation requests
+
+  -- Bind specification.
+  arbiterSpec requests grants
+
+  -- Create output variables.
+  bool' "grantA" grantA
+  bool' "grantB" grantB
+  bool' "grantC" grantC
+  return ()
+
+-- | Verify the different arbiter implementations.
+verifyArbiters :: IO ()
+verifyArbiters = do
+  putStrLn "\nVerifying arbiter1 ..."
+  verify "yices" 20 $ arbiter "arbiter1" arbiter1
+
+  putStrLn "\nVerifying arbiter2 ..."
+  verify "yices" 20 $ arbiter "arbiter2" arbiter2
+
+  putStrLn "\nVerifying arbiter2 ..."
+  verify "yices" 20 $ arbiter "arbiter3" arbiter3
+
+-- | Build the different arbiter implementations.
+buildArbiters :: IO ()
+buildArbiters = do
+  putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."
+  code "arbiter1" $ arbiter "arbiter1" arbiter1
+
+  putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."
+  code "arbiter2" $ arbiter "arbiter2" arbiter2
+
+  putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."
+  code "arbiter3" $ arbiter "arbiter3" arbiter3
+
+-- | Run all examples.
+runAll :: IO ()
+runAll = do
+  putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."
+  buildGCD
+  putStrLn "\nVerifying counter ..."
+  verifyCounter
+  putStrLn "\nVerifying arbiters ..."
+  verifyArbiters
+  putStrLn "\nBuilding arbiters ..."
+  buildArbiters
 
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,12 +1,15 @@
 name:    improve
-version: 0.0.3
+version: 0.0.4
 
 category: Language
 
-synopsis: An imperative, verifiable programming language for embedded applications.
+synopsis: An imperative, verifiable programming language for high assurance applications.
 
 description:
-    TODO
+  ImProve is an imperative DSL intended for high assurance, embedded applications.
+  ImProve uses infinite state, unbounded model checking to verify programs adhere
+  to specifications, which are written in the form of assertion statements.
+  Yices (required) is the backend SMT solver.
 
 author:     Tom Hawkins <tomahawkins@gmail.com>
 maintainer: Tom Hawkins <tomahawkins@gmail.com>