diff --git a/regression/cpp/auto1/test.desc b/regression/cpp/auto1/test.desc
index 0daa9695017..3862862ffd3 100644
--- a/regression/cpp/auto1/test.desc
+++ b/regression/cpp/auto1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -std=c++11
 ^EXIT=0$
diff --git a/regression/cpp/auto2/main.cpp b/regression/cpp/auto2/main.cpp
new file mode 100644
index 00000000000..26c5895984e
--- /dev/null
+++ b/regression/cpp/auto2/main.cpp
@@ -0,0 +1,7 @@
+int main()
+{
+#ifndef _MSC_VER
+  // Visual Studio uses C++14 by default, thus the below would not be valid
+  auto int x = 42;
+#endif
+}
diff --git a/regression/cpp/auto2/test.desc b/regression/cpp/auto2/test.desc
new file mode 100644
index 00000000000..a003b07b93c
--- /dev/null
+++ b/regression/cpp/auto2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cpp/auto3/main.cpp b/regression/cpp/auto3/main.cpp
new file mode 100644
index 00000000000..a3f0c15b9f6
--- /dev/null
+++ b/regression/cpp/auto3/main.cpp
@@ -0,0 +1,11 @@
+int main()
+{
+#ifndef _MSC_VER
+  // should yield a parse error unless in C++11 (or later) mode
+  auto x = 42;
+  const auto y = 42;
+  const auto &z = y;
+#else
+  intentionally invalid
+#endif
+}
diff --git a/regression/cpp/auto3/test.desc b/regression/cpp/auto3/test.desc
new file mode 100644
index 00000000000..b770347575f
--- /dev/null
+++ b/regression/cpp/auto3/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.cpp
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+parse error
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cpp/auto4/main.cpp b/regression/cpp/auto4/main.cpp
new file mode 100644
index 00000000000..d3b8e84a4c2
--- /dev/null
+++ b/regression/cpp/auto4/main.cpp
@@ -0,0 +1,6 @@
+int main()
+{
+  auto x = 42;
+  const auto y = 42;
+  const auto &z = y;
+}
diff --git a/regression/cpp/auto4/test.desc b/regression/cpp/auto4/test.desc
new file mode 100644
index 00000000000..3862862ffd3
--- /dev/null
+++ b/regression/cpp/auto4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+-std=c++11
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index 1b7bab029eb..8586a9ef129 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/src/cpp/cpp_convert_type.cpp
@@ -591,3 +591,19 @@ void cpp_convert_plain_type(typet &type)
     cpp_convert_type.write(type);
   }
 }
+
+void cpp_convert_auto(typet &dest, const typet &src)
+{
+  if(dest.id() != ID_merged_type && dest.has_subtype())
+  {
+    cpp_convert_auto(dest.subtype(), src);
+    return;
+  }
+
+  cpp_convert_typet cpp_convert_type(dest);
+  for(auto &t : cpp_convert_type.other)
+    if(t.id() == ID_auto)
+      t = src;
+
+  cpp_convert_type.write(dest);
+}
diff --git a/src/cpp/cpp_convert_type.h b/src/cpp/cpp_convert_type.h
index 0a14982210b..441db6ee7a3 100644
--- a/src/cpp/cpp_convert_type.h
+++ b/src/cpp/cpp_convert_type.h
@@ -16,4 +16,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 void cpp_convert_plain_type(typet &);
 
+void cpp_convert_auto(typet &dest, const typet &src);
+
 #endif // CPROVER_CPP_CPP_CONVERT_TYPE_H
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index fc1211a2d9d..da13cea78d4 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -68,7 +68,8 @@ symbolt &cpp_declarator_convertert::convert(
     scope=&cpp_typecheck.cpp_scopes.current_scope();
 
     // check the declarator-part of the type, in that scope
-    cpp_typecheck.typecheck_type(final_type);
+    if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
+      cpp_typecheck.typecheck_type(final_type);
   }
 
   is_code=is_code_type(final_type);
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 307a6188fa2..59ca3b35839 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -395,6 +395,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   static bool has_const(const typet &type);
   static bool has_volatile(const typet &type);
+  static bool has_auto(const typet &type);
 
   void typecheck_member_function(
     const irep_idt &compound_identifier,
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index 21d0fe6aae7..0215ae3fb3b 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -366,7 +366,9 @@ void cpp_typecheckt::typecheck_decl(codet &code)
 
   bool is_typedef=declaration.is_typedef();
 
-  typecheck_type(type);
+  if(declaration.declarators().empty() || !has_auto(type))
+    typecheck_type(type);
+
   assert(type.is_not_nil());
 
   if(declaration.declarators().empty() &&
@@ -407,7 +409,10 @@ void cpp_typecheckt::typecheck_decl(codet &code)
        symbol.value.id()!=ID_code)
     {
       decl_statement.copy_to_operands(symbol.value);
-      assert(follow(decl_statement.op1().type())==follow(symbol.type));
+      DATA_INVARIANT(
+        has_auto(symbol.type) ||
+          follow(decl_statement.op1().type()) == follow(symbol.type),
+        "declarator type should match symbol type");
     }
 
     new_code.move_to_operands(decl_statement);
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index f2be6ebe189..82f64089595 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -57,6 +57,22 @@ bool cpp_typecheckt::has_volatile(const typet &type)
     return false;
 }
 
+bool cpp_typecheckt::has_auto(const typet &type)
+{
+  if(type.id() == ID_auto)
+    return true;
+  else if(type.id() == ID_merged_type || type.id() == ID_frontend_pointer)
+  {
+    forall_subtypes(it, type)
+      if(has_auto(*it))
+        return true;
+
+    return false;
+  }
+  else
+    return false;
+}
+
 cpp_scopet &cpp_typecheckt::tag_scope(
   const irep_idt &base_name,
   bool has_body,
diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp
index 16bbd081123..a3d4ff6aa9d 100644
--- a/src/cpp/cpp_typecheck_declaration.cpp
+++ b/src/cpp/cpp_typecheck_declaration.cpp
@@ -122,7 +122,8 @@ void cpp_typecheckt::convert_non_template_declaration(
   declaration.name_anon_struct_union();
 
   // do the type of the declaration
-  typecheck_type(declaration_type);
+  if(declaration.declarators().empty() || !has_auto(declaration_type))
+    typecheck_type(declaration_type);
 
   // Elaborate any class template instance _unless_ we do a typedef.
   // These are only elaborated on usage!
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 871cd972af0..f936f5e5bb6 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
 
+#include "cpp_convert_type.h"
+
 /// Initialize an object with a value
 void cpp_typecheckt::convert_initializer(symbolt &symbol)
 {
@@ -144,6 +146,12 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
       if(symbol.type.find(ID_size).is_nil())
         symbol.type=symbol.value.type();
     }
+    else if(has_auto(symbol.type))
+    {
+      cpp_convert_auto(symbol.type, symbol.value.type());
+      typecheck_type(symbol.type);
+      implicit_typecast(symbol.value, symbol.type);
+    }
     else
       implicit_typecast(symbol.value, symbol.type);
 
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 7246108160f..fce70bcfa72 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -1442,7 +1442,7 @@ bool Parser::rDeclaration(cpp_declarationt &declaration)
               << "\n";
     #endif
 
-    if((cv_q.is_not_nil() || storage_spec.is_auto()) &&
+    if(cv_q.is_not_nil() &&
        ((t==TOK_IDENTIFIER && lex.LookAhead(1)=='=') || t=='*'))
       return rConstDeclaration(declaration, storage_spec, member_spec, cv_q);
     else
@@ -1585,6 +1585,17 @@ bool Parser::rIntegralDeclaration(
     if(!rDeclarators(declaration.declarators(), true))
       return false;
 
+    // handle trailing return type
+    if(
+      declaration.type().id() == ID_auto &&
+      declaration.declarators().size() == 1 &&
+      declaration.declarators().front().type().id() == ID_function_type &&
+      declaration.declarators().front().type().subtype().is_not_nil())
+    {
+      declaration.type() = declaration.declarators().front().type().subtype();
+      declaration.declarators().front().type().subtype().make_nil();
+    }
+
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ')
               << "Parser::rIntegralDeclaration 7\n";
@@ -1961,7 +1972,7 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
 
   if(t==TOK_STATIC ||
      t==TOK_EXTERN ||
-     t==TOK_AUTO ||
+     (t == TOK_AUTO && !ansi_c_parser.cpp11) ||
      t==TOK_REGISTER ||
      t==TOK_MUTABLE ||
      t==TOK_GCC_ASM ||
@@ -2224,6 +2235,7 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
     case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
     case TOK_BOOL: type_id=ID_bool; break;
     case TOK_CPROVER_BOOL: type_id=ID_proper_bool; break;
+    case TOK_AUTO: type_id = ID_auto; break;
     default: type_id=irep_idt();
     }
 
@@ -2912,6 +2924,11 @@ bool Parser::rDeclarator(
         typet return_type;
         if(!rTypeSpecifier(return_type, false))
           return false;
+
+        if(d_outer.subtype().is_not_nil())
+          return false;
+
+        d_outer.subtype().swap(return_type);
       }
 
       if(lex.LookAhead(0)==':')
@@ -7997,7 +8014,7 @@ bool Parser::rDeclarationStatement(codet &statement)
               << "Parser::rDeclarationStatement 3 " << t << "\n";
     #endif
 
-    if((cv_q.is_not_nil() || storage_spec.is_auto()) &&
+    if(cv_q.is_not_nil() &&
        ((t==TOK_IDENTIFIER && lex.LookAhead(1)=='=') || t=='*'))
     {
       #ifdef DEBUG