diff --git a/sys/include/timex.h b/sys/include/timex.h
index 317fdf85b49a4fc8b4055451a371fc78a050009b..897bb7adaddfdc171936c0487d1e3701da65b2b6 100644
--- a/sys/include/timex.h
+++ b/sys/include/timex.h
@@ -22,22 +22,12 @@
 #define __TIMEX_H
 
 #include <stdint.h>
-#include <stdio.h>
 #include <inttypes.h>
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-/**
- * @brief Formater for unsigned 32 bit values
- *
- *        mspgcc bug : PRIxxx macros not defined before mid-2011 versions
- */
-#ifndef PRIu32
-#define PRIu32 "lu"
-#endif
-
 /**
  * @brief The number of microseconds per second
  */
@@ -56,7 +46,14 @@ extern "C" {
 /**
  * @brief The maximum length of the string representation of a timex timestamp
  */
-#define TIMEX_MAX_STR_LEN   (18)
+#define TIMEX_MAX_STR_LEN   (20)
+/* 20 =
+ *  + 10 byte: 2^32-1 for seconds
+ *  + 1 byte: decimal point
+ *  + 6 byte: microseconds (normalized)
+ *  + 2 byte: " s" (unit)
+ *  + 1 byte: '\0'
+ */
 
 /**
  * @brief A timex timestamp
@@ -166,26 +163,16 @@ static inline timex_t timex_from_uint64(const uint64_t timestamp)
 /**
  * @brief Converts a timex timestamp to a string
  *
+ * @pre memory at timestamp >= TIMEX_MAX_STR_LEN
+ *
  * @param[in]  t            The timestamp to convert
  * @param[out] timestamp    The output char buffer for the converted timestamp
  *
  * @note The timestamp will be normalized
- * @note The buffer must have a size of TIMEX_MAX_STR_LEN characters
  *
  * @return A pointer to the string representation of the timestamp
- *
- * @todo replace call to snprintf by something more efficient
  */
-static inline const char *timex_to_str(timex_t t, char *timestamp)
-{
-    timex_normalize(&t);
-    /* 2^32 seconds have maximum 10 digits, microseconds are always < 1000000
-     * in a normalized timestamp, plus two chars for the point and terminator
-     * => 10 + 6 + 2 = 20 */
-    snprintf(timestamp, TIMEX_MAX_STR_LEN, "%" PRIu32 ".%06" PRIu32 " s",
-             t.seconds, t.microseconds);
-    return timestamp;
-}
+const char *timex_to_str(timex_t t, char *timestamp);
 
 #ifdef __cplusplus
 }
diff --git a/sys/shell/commands/sc_ipv6_nc.c b/sys/shell/commands/sc_ipv6_nc.c
index 9f8dc160e8ef2ac4cab6446b0236d67f4240dcf6..cd41b0454026550ce9b783c8aaaefe6e70f01acf 100644
--- a/sys/shell/commands/sc_ipv6_nc.c
+++ b/sys/shell/commands/sc_ipv6_nc.c
@@ -15,6 +15,7 @@
  * @author      Martine Lenders <mlenders@inf.fu-berlin.de>
  */
 
+#include <stdio.h>
 #include <string.h>
 
 #include "kernel_types.h"
diff --git a/sys/timex/timex_to_str.c b/sys/timex/timex_to_str.c
new file mode 100644
index 0000000000000000000000000000000000000000..eb96ef1bb9db9de36cd34b115b17e96d828efb0a
--- /dev/null
+++ b/sys/timex/timex_to_str.c
@@ -0,0 +1,65 @@
+/*
+ * Copyright (C) 2015 Martine Lenders <mlenders@inf.fu-berlin.de>
+ *
+ * This file is subject to the terms and conditions of the GNU Lesser
+ * General Public License v2.1. See the file LICENSE in the top level
+ * directory for more details.
+ */
+
+/**
+ * @{
+ *
+ * @file
+ */
+
+#include <stdint.h>
+
+#include "timex.h"
+
+#define RADIX   (10)
+
+static unsigned int u32_to_str(char *str, uint32_t u32)
+{
+    int len;
+    int i = 0;
+    if (u32 == 0) {
+        str[i] = '0';
+        return 1;
+    }
+    for (; u32 > 0; u32 /= RADIX) {
+        char digit = (char)(u32 % RADIX);
+        str[i++] = '0' + digit;
+    }
+    len = i;
+    i--;    /* go back to last character */
+    for (int j = 0; j < i; j++, i--) {
+        char tmp = str[i];
+        str[i] = str[j];
+        str[j] = tmp;
+    }
+    return len;
+}
+
+const char *timex_to_str(timex_t t, char *timestamp)
+{
+    timex_normalize(&t);
+    char *dec;
+    uint8_t offset = 6;
+    /* get seconds and set terminating '\0' byte */
+    dec = &timestamp[u32_to_str(timestamp, t.seconds)];
+    *(dec++) = '.';                         /* set decimal point */
+    for (uint32_t i = 100000; i > 1; i /= 10) {  /* timex_normalize() ensures that i < 1000000 */
+        if (t.microseconds < i) {           /* pad with 0's */
+            *(dec++) = '0';
+            offset--;
+        }
+    }
+    u32_to_str(dec, t.microseconds);        /* convert microseconds */
+    dec += offset;
+    *(dec++) = ' ';                         /* append unit */
+    *(dec++) = 's';
+    *(dec) = '\0';
+    return timestamp;
+}
+
+/** @} */