diff --git a/regression/smv/process/process1.desc b/regression/smv/process/process1.desc
index 55a48b851..268f47784 100644
--- a/regression/smv/process/process1.desc
+++ b/regression/smv/process/process1.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 process1.smv
 
-^EXIT=0$
+^file .* line 8: no support for asynchronous processes$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This does not parse.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 47e9b6b0b..00ef781cc 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -39,6 +39,7 @@ IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
 IREP_ID_ONE(smv_sizeof)
 IREP_ID_ONE(smv_module_instance)
+IREP_ID_ONE(smv_process_module_instance)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index a45ee3f9f..8ca018db4 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -1060,7 +1060,7 @@ std::string type2smv(const typet &type, const namespacet &ns)
   }
   else if(type.id() == ID_smv_module_instance)
   {
-    auto code = id2string(to_smv_module_instance_type(type).identifier());
+    auto code = id2string(to_smv_module_instance_type(type).base_name());
     const exprt &e=(exprt &)type;
     if(e.has_operands())
     {
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index f7745c8b5..272b02fac 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -145,11 +145,11 @@ Function: new_module
 static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_name)
 {
   auto base_name = stack_expr(module_name).id_string();
-  const std::string identifier=smv_module_symbol(base_name);
+  const auto identifier=smv_module_symbol(base_name);
   PARSER.parse_tree.module_list.push_back(smv_parse_treet::modulet{});
   auto &module=PARSER.parse_tree.module_list.back();
-  PARSER.parse_tree.module_map[identifier] = --PARSER.parse_tree.module_list.end();
-  module.name = identifier;
+  PARSER.parse_tree.module_map[base_name] = --PARSER.parse_tree.module_list.end();
+  module.identifier = identifier;
   module.base_name = base_name;
   module.source_location = stack_expr(location).source_location();
   PARSER.module = &module;
@@ -598,18 +598,26 @@ simple_type_specifier:
            ;
 
 module_type_specifier:
-             module_name
+             module_name parameter_list_paren_opt
            {
              init($$, ID_smv_module_instance);
-             to_smv_module_instance_type(stack_type($$)).identifier(
-                           smv_module_symbol(stack_expr($1).id_string()));
+             to_smv_module_instance_type(stack_type($$)).base_name(stack_expr($1).id());
+             stack_expr($$).operands().swap(stack_expr($2).operands());
            }
-           | module_name '(' parameter_list ')'
+           | process_Token module_name parameter_list_paren_opt
            {
-             init($$, ID_smv_module_instance);
-             to_smv_module_instance_type(stack_type($$)).identifier(
-                           smv_module_symbol(stack_expr($1).id_string()));
-             stack_expr($$).operands().swap(stack_expr($3).operands());
+             init($$, ID_smv_process_module_instance);
+           }
+           ;
+
+parameter_list_paren_opt:
+             /* optional */
+           {
+             init($$);
+           }
+           | '(' parameter_list ')'
+           {
+             $$ = $2;
            }
            ;
 
diff --git a/src/smvlang/smv_ebmc_language.cpp b/src/smvlang/smv_ebmc_language.cpp
index 77a576e7a..b929aa8cb 100644
--- a/src/smvlang/smv_ebmc_language.cpp
+++ b/src/smvlang/smv_ebmc_language.cpp
@@ -80,7 +80,7 @@ std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
 
     for(const auto &module : parse_tree.module_list)
       show_modules.modules.emplace_back(
-        module.name, module.base_name, "SMV", module.source_location);
+        module.identifier, module.base_name, "SMV", module.source_location);
 
     auto filename = cmdline.value_opt("outfile").value_or("-");
     output_filet output_file{filename};
diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp
index 4ba5f722f..6b16e824f 100644
--- a/src/smvlang/smv_language.cpp
+++ b/src/smvlang/smv_language.cpp
@@ -62,7 +62,7 @@ void smv_languaget::dependencies(
   const std::string &module, 
   std::set<std::string> &module_set)
 {
-  auto m_it = smv_parse_tree.module_map.find(module);
+  auto m_it = smv_parse_tree.module_map.find(smv_module_base_name(module));
 
   if(m_it == smv_parse_tree.module_map.end())
     return;
@@ -71,8 +71,11 @@ void smv_languaget::dependencies(
 
   for(auto &element : smv_module.elements)
     if(element.is_var() && element.expr.type().id() == ID_smv_module_instance)
-      module_set.insert(id2string(
-        to_smv_module_instance_type(element.expr.type()).identifier()));
+    {
+      auto base_name =
+        to_smv_module_instance_type(element.expr.type()).base_name();
+      module_set.insert(id2string(smv_module_symbol(base_name)));
+    }
 }
 
 /*******************************************************************\
@@ -90,7 +93,7 @@ Function: smv_languaget::modules_provided
 void smv_languaget::modules_provided(std::set<std::string> &module_set)
 {
   for(const auto &module : smv_parse_tree.module_list)
-    module_set.insert(id2string(module.name));
+    module_set.insert(id2string(module.identifier));
 }
 
 /*******************************************************************\
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index f5d211e36..3c4502d24 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -30,7 +30,7 @@ class smv_parse_treet
   struct modulet
   {
     source_locationt source_location;
-    irep_idt name, base_name;
+    irep_idt identifier, base_name;
     std::vector<irep_idt> parameters;
 
     struct elementt
@@ -315,6 +315,7 @@ class smv_parse_treet
   using module_listt = std::list<modulet>;
   module_listt module_list;
 
+  // map from module base names into the module list
   using module_mapt =
     std::unordered_map<irep_idt, module_listt::iterator, irep_id_hash>;
   module_mapt module_map;
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 92f3c7cfe..4ed0b3da2 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/mathematical_expr.h>
 #include <util/namespace.h>
+#include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/typecheck.h>
 
@@ -32,13 +33,13 @@ class smv_typecheckt:public typecheckt
   smv_typecheckt(
     smv_parse_treet &_smv_parse_tree,
     symbol_table_baset &_symbol_table,
-    const std::string &_module,
+    const std::string &_module_identifier,
     bool _do_spec,
     message_handlert &_message_handler)
     : typecheckt(_message_handler),
       smv_parse_tree(_smv_parse_tree),
       symbol_table(_symbol_table),
-      module(_module),
+      module_identifier(_module_identifier),
       do_spec(_do_spec)
   {
     nondet_count=0;
@@ -80,7 +81,7 @@ class smv_typecheckt:public typecheckt
 protected:
   smv_parse_treet &smv_parse_tree;
   symbol_table_baset &symbol_table;
-  const std::string &module;
+  const std::string &module_identifier;
   bool do_spec;
 
   void check_type(typet &);
@@ -104,7 +105,7 @@ class smv_typecheckt:public typecheckt
 
   void instantiate(
     smv_parse_treet::modulet &,
-    const irep_idt &identifier,
+    const irep_idt &module_base_name,
     const irep_idt &instance,
     const exprt::operandst &arguments,
     const source_locationt &);
@@ -216,7 +217,7 @@ void smv_typecheckt::convert_ports(
     ports.push_back(exprt(ID_symbol));
     ports.back().set(
       ID_identifier,
-      id2string(smv_module.name) + "::var::" + id2string(port_name));
+      id2string(smv_module.identifier) + "::var::" + id2string(port_name));
   }
 }
 
@@ -249,16 +250,25 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
       for(auto &argument : instance.arguments())
         convert(argument);
 
+      // the base name of the instance, not the module
       auto instance_base_name =
         to_smv_identifier_expr(element.expr).identifier();
 
       instantiate(
         smv_module,
-        instance.identifier(),
+        instance.base_name(),
         instance_base_name,
         instance.arguments(),
         instance.source_location());
     }
+
+    if(
+      element.is_var() &&
+      element.expr.type().id() == ID_smv_process_module_instance)
+    {
+      throw errort().with_location(element.expr.source_location())
+        << "no support for asynchronous processes";
+    }
   }
 }
 
@@ -276,18 +286,18 @@ Function: smv_typecheckt::instantiate
 
 void smv_typecheckt::instantiate(
   smv_parse_treet::modulet &smv_module,
-  const irep_idt &identifier,
+  const irep_idt &module_base_name,
   const irep_idt &instance,
   const exprt::operandst &arguments,
   const source_locationt &location)
 {
   // Find the module
-  auto module_it = smv_parse_tree.module_map.find(identifier);
+  auto module_it = smv_parse_tree.module_map.find(module_base_name);
 
   if(module_it == smv_parse_tree.module_map.end())
   {
     throw errort().with_location(location)
-      << "submodule `" << identifier << "' not found";
+      << "submodule `" << module_base_name << "' not found";
   }
 
   const auto &instantiated_module = *module_it->second;
@@ -297,7 +307,7 @@ void smv_typecheckt::instantiate(
   if(parameters.size() != arguments.size())
   {
     throw errort().with_location(location)
-      << "submodule `" << identifier << "' has wrong number of arguments";
+      << "submodule `" << module_base_name << "' has wrong number of arguments";
   }
 
   rename_mapt parameter_map;
@@ -676,7 +686,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
 
     if(mode == INIT || next)
     {
-      if(symbol.module==module)
+      if(symbol.module == module_identifier)
       {
         symbol.is_input=false;
         symbol.is_state_var=true;
@@ -1665,7 +1675,7 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &dest_type)
       // sets can be assigned to scalars, which yields a nondeterministic
       // choice
       std::string identifier =
-        module + "::var::" + std::to_string(nondet_count++);
+        module_identifier + "::var::" + std::to_string(nondet_count++);
 
       expr.set(ID_identifier, identifier);
       expr.set("#smv_nondet_choice", true);
@@ -1826,7 +1836,7 @@ void smv_typecheckt::convert(exprt &expr)
     if(
       smv_parse_tree.enum_set.find(identifier) == smv_parse_tree.enum_set.end())
     {
-      std::string id = module + "::var::" + identifier;
+      std::string id = module_identifier + "::var::" + identifier;
 
       expr.set(ID_identifier, id);
       expr.id(ID_symbol);
@@ -1876,8 +1886,8 @@ void smv_typecheckt::convert(exprt &expr)
         << "expected operand here";
     }
 
-    std::string identifier=
-      module+"::var::"+std::to_string(nondet_count++);
+    std::string identifier =
+      module_identifier + "::var::" + std::to_string(nondet_count++);
 
     expr.set(ID_identifier, identifier);
     expr.set("#smv_nondet_choice", true);
@@ -2198,7 +2208,8 @@ void smv_typecheckt::create_var_symbols(
     {
       irep_idt base_name = merge_complex_identifier(element.expr);
       auto location = element.expr.source_location();
-      irep_idt identifier = module + "::var::" + id2string(base_name);
+      irep_idt identifier =
+        module_identifier + "::var::" + id2string(base_name);
 
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
@@ -2215,16 +2226,20 @@ void smv_typecheckt::create_var_symbols(
 
       symbolt symbol{identifier, std::move(type), mode};
 
-      symbol.module = modulep->name;
+      symbol.module = modulep->identifier;
       symbol.base_name = base_name;
 
-      if(module == "smv::main")
+      if(module_identifier == "smv::main")
         symbol.pretty_name = symbol.base_name;
       else
         symbol.pretty_name = strip_smv_prefix(symbol.name);
 
-      if(symbol.type.id() == ID_smv_module_instance)
+      if(
+        symbol.type.id() == ID_smv_module_instance ||
+        symbol.type.id() == ID_smv_process_module_instance)
+      {
         symbol.is_input = false;
+      }
       else
         symbol.is_input = true;
 
@@ -2238,7 +2253,8 @@ void smv_typecheckt::create_var_symbols(
     {
       irep_idt base_name = merge_complex_identifier(element.lhs());
       auto location = to_equal_expr(element.expr).lhs().source_location();
-      irep_idt identifier = module + "::var::" + id2string(base_name);
+      irep_idt identifier =
+        module_identifier + "::var::" + id2string(base_name);
 
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
@@ -2254,10 +2270,10 @@ void smv_typecheckt::create_var_symbols(
       symbolt symbol{identifier, std::move(type), mode};
 
       symbol.mode = mode;
-      symbol.module = modulep->name;
+      symbol.module = modulep->identifier;
       symbol.base_name = base_name;
 
-      if(module == "smv::main")
+      if(module_identifier == "smv::main")
         symbol.pretty_name = symbol.base_name;
       else
         symbol.pretty_name = strip_smv_prefix(symbol.name);
@@ -2272,7 +2288,8 @@ void smv_typecheckt::create_var_symbols(
     else if(element.is_enum())
     {
       irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
-      irep_idt identifier = module + "::var::" + id2string(base_name);
+      irep_idt identifier =
+        module_identifier + "::var::" + id2string(base_name);
 
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
@@ -2486,7 +2503,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
     module_symbol.base_name=smv_module.base_name;
     module_symbol.pretty_name=smv_module.base_name;
-    module_symbol.name=smv_module.name;
+    module_symbol.name = smv_module.identifier;
     module_symbol.module=module_symbol.name;
     module_symbol.type=typet(ID_module);
     module_symbol.mode="SMV";
@@ -2558,9 +2575,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         else
           spec_symbol.base_name = "spec" + std::to_string(nr++);
 
-        spec_symbol.name =
-          id2string(smv_module.name) + "::" + id2string(spec_symbol.base_name);
-        spec_symbol.module = smv_module.name;
+        spec_symbol.name = id2string(smv_module.identifier) +
+                           "::" + id2string(spec_symbol.base_name);
+        spec_symbol.module = smv_module.identifier;
         spec_symbol.type = bool_typet();
         spec_symbol.is_property = true;
         spec_symbol.mode = "SMV";
@@ -2568,7 +2585,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         spec_symbol.location = element.location;
         spec_symbol.location.set_comment(to_string(element.expr));
 
-        if(smv_module.name == "smv::main")
+        if(smv_module.identifier == "smv::main")
           spec_symbol.pretty_name = spec_symbol.base_name;
         else
           spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
@@ -2581,8 +2598,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
   }
 
   // lowering
-  for(auto v_it = symbol_table.symbol_module_map.lower_bound(smv_module.name);
-      v_it != symbol_table.symbol_module_map.upper_bound(smv_module.name);
+  for(auto v_it =
+        symbol_table.symbol_module_map.lower_bound(smv_module.identifier);
+      v_it != symbol_table.symbol_module_map.upper_bound(smv_module.identifier);
       v_it++)
   {
     auto &symbol = symbol_table.get_writeable_ref(v_it->second);
@@ -2605,18 +2623,19 @@ Function: smv_typecheckt::typecheck
 
 void smv_typecheckt::typecheck()
 {
-  if(module != "smv::main")
+  if(module_identifier != "smv::main")
     return;
 
   // check all modules for duplicate identifiers
   for(auto &module : smv_parse_tree.module_list)
     variable_checks(module);
 
-  auto it = smv_parse_tree.module_map.find(module);
+  auto module_base_name = smv_module_base_name(module_identifier);
+  auto it = smv_parse_tree.module_map.find(module_base_name);
 
   if(it == smv_parse_tree.module_map.end())
   {
-    throw errort() << "failed to find module " << module;
+    throw errort() << "failed to find module " << module_base_name;
   }
 
   convert(*it->second);
@@ -2637,12 +2656,12 @@ Function: smv_typecheck
 bool smv_typecheck(
   smv_parse_treet &smv_parse_tree,
   symbol_table_baset &symbol_table,
-  const std::string &module,
+  const std::string &module_identifier,
   message_handlert &message_handler,
   bool do_spec)
 {
   smv_typecheckt smv_typecheck(
-    smv_parse_tree, symbol_table, module, do_spec, message_handler);
+    smv_parse_tree, symbol_table, module_identifier, do_spec, message_handler);
   return smv_typecheck.typecheck_main();
 }
 
@@ -2658,7 +2677,25 @@ Function: smv_module_symbol
 
 \*******************************************************************/
 
-std::string smv_module_symbol(const std::string &module)
+irep_idt smv_module_symbol(const irep_idt &base_name)
+{
+  return "smv::" + id2string(base_name);
+}
+
+/*******************************************************************\
+
+Function: smv_module_base_name
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+irep_idt smv_module_base_name(const irep_idt &identifier)
 {
-  return "smv::"+module;
+  PRECONDITION(has_prefix(id2string(identifier), "smv::"));
+  return id2string(identifier).substr(5, std::string::npos);
 }
diff --git a/src/smvlang/smv_typecheck.h b/src/smvlang/smv_typecheck.h
index 984933e5c..5fa9b95ac 100644
--- a/src/smvlang/smv_typecheck.h
+++ b/src/smvlang/smv_typecheck.h
@@ -17,10 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com
 bool smv_typecheck(
   smv_parse_treet &smv_parse_tree,
   symbol_table_baset &,
-  const std::string &module,
+  const std::string &module_identifier,
   message_handlert &message_handler,
   bool do_spec = true);
 
-std::string smv_module_symbol(const std::string &module);
+/// returns the identifier for the module with given base name
+irep_idt smv_module_symbol(const irep_idt &module_base_name);
+
+/// returns the base_name for the module with given identifier
+irep_idt smv_module_base_name(const irep_idt &module_identifier);
 
 #endif
diff --git a/src/smvlang/smv_types.h b/src/smvlang/smv_types.h
index 868b80c12..f3f6786de 100644
--- a/src/smvlang/smv_types.h
+++ b/src/smvlang/smv_types.h
@@ -76,20 +76,21 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
 class smv_module_instance_typet : public typet
 {
 public:
-  explicit smv_module_instance_typet(irep_idt _identifier)
+  explicit smv_module_instance_typet(irep_idt _base_name)
     : typet{ID_smv_module_instance}
   {
-    identifier(_identifier);
+    base_name(_base_name);
   }
 
-  irep_idt identifier() const
+  // the base name of the module that is instantiated
+  irep_idt base_name() const
   {
-    return get(ID_identifier);
+    return get(ID_base_name);
   }
 
-  void identifier(irep_idt _identifier)
+  void base_name(irep_idt _base_name)
   {
-    set(ID_identifier, _identifier);
+    set(ID_base_name, _base_name);
   }
 
   const exprt::operandst &arguments() const