diff --git a/Language/Atom.hs b/Language/Atom.hs
--- a/Language/Atom.hs
+++ b/Language/Atom.hs
@@ -1,8 +1,12 @@
 {- |
-  Atom is a Haskell DSL for designing hard realtime embedded programs.  Based
-  on conditional term rewriting, atom will compile a collection of atomic state
-  transition rules to a C program with constant memory use and deterministic
-  execution time.
+  Atom is a Haskell DSL for designing hard realtime embedded software.
+  Based on guarded atomic actions (similar to STM), Atom enables highly
+  concurrent programming without the need for mutex locking.
+  In addition, Atom performs compile-time task scheduling and generates code
+  with deterministic execution time and constant memory use, simplifying the
+  process of timing verification and memory consumption in hard realtime
+  applications. Without mutex locking and run-time task scheduling,
+  Atom eliminates the need and overhead of RTOSs for many embedded applications.
 -}
 
 module Language.Atom
@@ -11,7 +15,6 @@
   , module Language.Atom.Common
   , module Language.Atom.Language
   , module Language.Atom.Unit
-  , module Language.Atom.Verification
   ) where
 
 import Language.Atom.Code
@@ -19,4 +22,3 @@
 import Language.Atom.Common
 import Language.Atom.Language
 import Language.Atom.Unit
-import Language.Atom.Verification
diff --git a/Language/Atom/Code.hs b/Language/Atom/Code.hs
--- a/Language/Atom/Code.hs
+++ b/Language/Atom/Code.hs
@@ -12,10 +12,8 @@
 import Data.List
 import Data.Maybe
 import Data.Function
-import Data.Word
 import System.IO
 import Text.Printf
-import Unsafe.Coerce
 
 import Language.Atom.Analysis
 import Language.Atom.Elaboration
@@ -181,14 +179,8 @@
   CWord16 a   -> show a
   CWord32 a   -> show a ++ "UL"
   CWord64 a   -> show a ++ "ULL"
-  CFloat  a   -> show $ floatBits  a
-  CDouble a   -> show $ doubleBits a
-
-floatBits :: Float -> Word32
-floatBits = unsafeCoerce
-
-doubleBits :: Double -> Word64
-doubleBits = unsafeCoerce
+  CFloat  a   -> show a ++ "F"
+  CDouble a   -> show a
 
 codeRule :: Config -> Rule -> String
 codeRule config rule@(Rule _ _ _ _ _ _ _) =
diff --git a/Language/Atom/Language.hs b/Language/Atom/Language.hs
--- a/Language/Atom/Language.hs
+++ b/Language/Atom/Language.hs
@@ -44,6 +44,7 @@
   , double'
   -- * Custom Actions
   , action
+  , call
   -- * Probing
   , probe
   , probes
@@ -223,6 +224,10 @@
 action f ues = do
   (g, a) <- get
   put (g, a { atomActions = atomActions a ++ [(f, ues)] })
+
+-- | Calls an external C function of type 'void f(void)'.
+call :: Name -> Atom ()
+call n = action (\ _ -> n ++ "()") []
 
 -- | Declares a probe.
 probe :: Expr a => Name -> E a -> Atom ()
diff --git a/Language/Atom/Verification.hs b/Language/Atom/Verification.hs
deleted file mode 100644
--- a/Language/Atom/Verification.hs
+++ /dev/null
@@ -1,219 +0,0 @@
-module Language.Atom.Verification
-  ( Model
-  , model
-  -- , verify
-  -- , kInduction
-  -- , boundedModelChecking
-  , test
-  ) where
-
-import Data.Char ()
-import Data.Function ()
-import Data.Int ()
-import Data.List ()
-import Data.Ratio ()
-import Data.Word ()
-import Math.SMT.Yices.Pipe
-import Math.SMT.Yices.Syntax
-import System.Process ()
-
-import Language.Atom.Elaboration ()
-import Language.Atom.Expressions
-import Language.Atom.Scheduling
-
--- | A model of a scheduled program for model checking.
-data Model = Model
-  --{ transition :: Int -> [Name] -> ([CmdY], [CmdY])
-  --, names :: [(Name, Int)]
-  --, 
-  --}
-
--- | Create a model from a scheduled program.
-model :: Schedule -> [UV] -> [UA] -> Model 
-model _ _ _ = Model
-
--- | A list of assertions captured by a model.
---assertions :: Model -> [Name]
-
--- | Bounded model checking starting from the initial state.
---boundedModelChecking :: Model -> Int -> Name -> IO (Maybe Witness)
-
--- | K-induction model checking given a min and a max k-depth.
---kInduction :: Model -> Int -> Int -> Name -> IO ()
-
-
-test :: IO ()
-test = do
-  print test
-  result <- runY test
-  print result
-  where
-  test =
-    [ DEFINE ("a", VarT "int") Nothing
-    , DEFINE ("b", VarT "int") Nothing
-    , ASSERT (VarE "a" := VarE "b")
-    -- , ASSERT (YNe (YVar "a") (YVar "b"))
-    ]
-  
--- | Runs a Yices program.  Returns a list of variable values if satisfiable.
-runY :: [CmdY] -> IO ResY
-runY a = do
-  p <- createYicesPipe "yices" []
-  runCmdsY p a
-  r <- checkY p
-  exitY p
-  return r
-
-
-
-{-
-yType :: Type -> YT
-yType t = case t of
-  Bool   -> YBool
-  Int8   -> YInt
-  Int16  -> YInt
-  Int32  -> YInt
-  Int64  -> YInt
-  Word8  -> YNat
-  Word16 -> YNat
-  Word32 -> YNat
-  Word64 -> YNat
-  Float  -> YReal
-  Double -> YReal
--}
-
-{-
-vars :: [UV] -> Int -> String
-vars uvs step = concatMap (var step) uvs
-  where
-  var :: Int -> UV -> String
-  var step uv = "(define " ++ uvName step uv ++ "::" ++ yicesType (uvType uv) ++ ")\n"
-
-uvName :: Int -> UV -> String
-uvName step (UV i _ _) = "v" ++ show i ++ "_" ++ show step
-
-initialize :: [UV] -> String
-initialize uvs = vars uvs 0 ++ concatMap initialize uvs
-  where
-  initialize :: UV -> String
-  initialize uv@(UV _ _ (Local c)) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"
-  initialize (UV _ _ (External _)) = ""
-  const :: Const -> String
-  const c = case c of
-    CBool   c -> if c then "true" else "false"
-    CInt8   c -> "0b" ++ bits  8 (fromIntegral c)
-    CInt16  c -> "0b" ++ bits 16 (fromIntegral c)
-    CInt32  c -> "0b" ++ bits 32 (fromIntegral c)
-    CInt64  c -> "0b" ++ bits 64 (fromIntegral c)
-    CWord8  c -> "0b" ++ bits  8 (fromIntegral c)
-    CWord16 c -> "0b" ++ bits 16 (fromIntegral c)
-    CWord32 c -> "0b" ++ bits 32 (fromIntegral c)
-    CWord64 c -> "0b" ++ bits 64 (fromIntegral c)
-    CFloat  c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
-    CDouble c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
-
-  bits :: Int -> Word64 -> String
-  bits 0 _ = ""
-  bits n a = bits (n - 1) (div a 2) ++ show (mod a 2)
-
--- Time 0 to 1 is step 1.
-transition :: [[[Rule]]] -> [UV] -> Int -> String
-transition _ {-schedule-} uvs step = vars uvs step ++ transition
-  where
-  transition = "; transition " ++ show (step - 1) ++ " to " ++ show step ++ "\n"  --XXX
-
-getUV :: [UV] -> Int -> UV
-getUV [] _ = error "Verify.getUV"
-getUV (uv@(UV i _ _):_) j | i == j = uv
-getUV (_:a) i = getUV a i
-
-
-parseVar :: [UV] -> Group -> (Int, UV, String)
-parseVar uvs (G [S "=", S name, value]) = (t, getUV uvs i, parseValue value)
-  where
-  (i', t') = break (== '_') $ tail name
-  i = read i'
-  t = read $ tail t'
-parseVar _ g = error $ "Verify.parseVar: " ++ show g
-
-parseValue :: Group -> String
-parseValue (S ('0':'b':a)) = "b" ++ a ++ " "
-parseValue (S "true")      = "1"
-parseValue (S "false")     = "0"
-parseValue (S v)           = "r" ++ v ++ " "
-parseValue (G [S "/", S n, S d]) = "r" ++ show (fromRational (read n % read d)) ++ " "
-parseValue a               = error $ "Verify.parseValue: " ++ show a
-
-
-data Heirarchy = Variable UV | Module String [Heirarchy]
-
-vcd :: [UV] -> [(Int, UV, String)] -> String
-vcd uvs signals' = header ++ samples ++ end
-  where
-  signals = sortBy (\ (a,_,_) (b,_,_) -> compare a b) signals'
-
-  header = "$timescale\n  1 ms\n$end\n" ++ concatMap decl (heirarchy 0 uvs) ++ "$enddefinitions $end\n"
-  (lastTime, _, _) = last signals
-  end = "#" ++ show (lastTime + 1) ++ "\n"
-
-  decl :: Heirarchy -> String
-  decl (Module name subs) = "$scope module " ++ name ++ " $end\n" ++ concatMap decl subs ++ "$upscope $end\n"
-  decl (Variable uv)      = declVar uv
-
-  declVar :: UV -> String
-  declVar uv@(UV i n _) = case uvType uv of
-    Bool   -> "$var wire 1 "     ++ code ++ " " ++ name ++ " $end\n"
-    Int8   -> "$var integer 8 "  ++ code ++ " " ++ name ++ " $end\n"
-    Int16  -> "$var integer 16 " ++ code ++ " " ++ name ++ " $end\n"
-    Int32  -> "$var integer 32 " ++ code ++ " " ++ name ++ " $end\n"
-    Int64  -> "$var integer 64 " ++ code ++ " " ++ name ++ " $end\n"
-    Word8  -> "$var wire 8 "     ++ code ++ " " ++ name ++ " $end\n"
-    Word16 -> "$var wire 16 "    ++ code ++ " " ++ name ++ " $end\n"
-    Word32 -> "$var wire 32 "    ++ code ++ " " ++ name ++ " $end\n"
-    Word64 -> "$var wire 64 "    ++ code ++ " " ++ name ++ " $end\n"
-    Float  -> "$var real 32 "    ++ code ++ " " ++ name ++ " $end\n"
-    Double -> "$var real 64 "    ++ code ++ " " ++ name ++ " $end\n"
-    where
-    code = vcdCode i
-    name = reverse $ takeWhile (/= '.') $ reverse n
-
-  samples = concatMap sample signals
-
-  sample (t, (UV i _ _), v) = "#" ++ show t ++ "\n" ++ v ++ vcdCode i ++ "\n"
-
-heirarchy :: Int -> [UV] -> [Heirarchy]
-heirarchy _ [] = []
-heirarchy depth uvs = heirarchy' depth notvars ++ map Variable vars
-  where
-  isVar :: UV -> Bool
-  isVar uv = length (path depth uv) == 1
-  (vars, notvars) = partition isVar uvs
-
-heirarchy' :: Int -> [UV] -> [Heirarchy]
-heirarchy' _ [] = []
-heirarchy' depth uvs@(a:_) = Module n (heirarchy (depth + 1) yes) : heirarchy' depth no
-  where
-  n = head $ path depth a
-  isMod uv = n == head (path depth uv)
-  (yes, no) = partition isMod uvs
-
-path :: Int -> UV -> [String]
-path depth (UV _ n _) = drop depth $ words $ map (\ c -> if c == '.' then ' ' else c) n
-
-vcdCode :: Int -> String
-vcdCode i | i < 94 =              [chr (33 + mod i 94)]
-vcdCode i = vcdCode (div i 94) ++ [chr (33 + mod i 94)]
-
-{-
-bitString :: Int -> String
-bitString n = if null bits then "0" else bits
-  where
-  bit :: Int -> Char
-  bit i = if testBit n i then '1' else '0'
-  bits = dropWhile (== '0') $ map bit $ reverse [0..31]
--}
-
--}
-
-
-
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,3 +1,9 @@
+atom 0.1.4    12/16/2009
+
+- Added 'call' function. 
+- Bug fix to float and double variable initialization.
+- Moved Language.Atom.Verification to new project: afv.
+
 atom 0.1.3    12/03/2009
 
 - Added linear lookup (Common). 
diff --git a/atom.cabal b/atom.cabal
--- a/atom.cabal
+++ b/atom.cabal
@@ -1,5 +1,5 @@
 name:    atom
-version: 0.1.3
+version: 0.1.4
 
 category: Language
 
@@ -35,8 +35,7 @@
     build-depends:
         base       >= 4       && < 5,
         mtl        >= 1.1.0.1 && < 1.2,
-        process    >= 1.0.1.1 && < 1.2,
-        yices      >= 0.0.0.4
+        process    >= 1.0.1.1 && < 1.2
 
     exposed-modules:
         Language.Atom
@@ -50,7 +49,6 @@
         Language.Atom.Language
         Language.Atom.Scheduling
         Language.Atom.Unit
-        Language.Atom.Verification
 
     extensions: GADTs