diff --git a/regression/cbmc/points-to-sets/main.c b/regression/cbmc/points-to-sets/main.c
new file mode 100644
index 00000000000..70e4856e45a
--- /dev/null
+++ b/regression/cbmc/points-to-sets/main.c
@@ -0,0 +1,9 @@
+int main()
+{
+  unsigned int value;
+  int *p = (int *)value;
+
+  *p = *p + 1;
+  assert(1);
+  return 0;
+}
diff --git a/regression/cbmc/points-to-sets/test.desc b/regression/cbmc/points-to-sets/test.desc
new file mode 100644
index 00000000000..e95a06651d8
--- /dev/null
+++ b/regression/cbmc/points-to-sets/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-points-to-sets
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.
diff --git a/regression/cbmc/points-to-sets/test_json.desc b/regression/cbmc/points-to-sets/test_json.desc
new file mode 100644
index 00000000000..3e62c77d638
--- /dev/null
+++ b/regression/cbmc/points-to-sets/test_json.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-points-to-sets --json-ui
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\}
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.
diff --git a/regression/cbmc/points-to-sets/test_xml.desc b/regression/cbmc/points-to-sets/test_xml.desc
new file mode 100644
index 00000000000..d4bf269cbb3
--- /dev/null
+++ b/regression/cbmc/points-to-sets/test_xml.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-points-to-sets --xml-ui
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 7b561f1cacf..624c9d5070f 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -122,6 +122,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
   options.set_option("show-goto-symex-steps", false);
+  options.set_option("show-points-to-sets", false);
 
   // Other default
   options.set_option("arrays-uf", "auto");
@@ -520,6 +521,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-goto-symex-steps"))
     options.set_option("show-goto-symex-steps", true);
 
+  if(cmdline.isset("show-points-to-sets"))
+    options.set_option("show-points-to-sets", true);
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
@@ -562,6 +566,17 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
+  if(cmdline.isset("show-points-to-sets"))
+  {
+    if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
+    {
+      log.error() << "--show-points-to-sets supports only"
+                     " json output. Use --json-ui."
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   register_languages();
 
   // configure gcc, if required
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index a3e87ebcdf5..f12c07f72b6 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -177,6 +177,7 @@ void run_property_decider(
   "(show-loops)" \
   "(show-vcc)" \
   "(show-goto-symex-steps)" \
+  "(show-points-to-sets)" \
   "(slice-formula)" \
   "(unwinding-assertions)" \
   "(no-unwinding-assertions)" \
@@ -203,6 +204,8 @@ void run_property_decider(
   " --show-symex-strategies      list strategies for use with --paths\n" \
   " --show-goto-symex-steps      show which steps symex travels, includes " \
   "                              diagnostic information\n" \
+  " --show-points-to-sets        show points-to sets for\n" \
+  "                              pointer dereference. Requires --json-ui.\n" \
   " --program-only               only show program expression\n" \
   " --show-byte-ops              show all byte extracts and updates\n" \
   " --show-loops                 show the loops in the program\n" \
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 9aaa72921f7..49899889f5d 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -134,9 +134,9 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   symex_dereference_statet symex_dereference_state(state, ns);
 
   value_set_dereferencet dereference(
-    ns, state.symbol_table, symex_dereference_state, language_mode, false);
+    ns, state.symbol_table, symex_dereference_state, language_mode, false, log);
 
-  expr = dereference.dereference(expr);
+  expr = dereference.dereference(expr, symex_config.show_points_to_sets);
   lift_lets(state, expr);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);
diff --git a/src/goto-symex/symex_config.h b/src/goto-symex/symex_config.h
index 086b1b091b5..b7bd52e83f6 100644
--- a/src/goto-symex/symex_config.h
+++ b/src/goto-symex/symex_config.h
@@ -46,6 +46,7 @@ struct symex_configt final
   /// \brief Prints out the path that symex is actively taking during execution,
   /// includes diagnostic information about call stack and guard size.
   bool show_symex_steps;
+  bool show_points_to_sets;
 
   /// Maximum sizes for which field sensitivity will be applied to array cells
   std::size_t max_field_sensitivity_array_size;
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index af6c8a36c7b..65068e9025d 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -264,10 +264,12 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
       state.symbol_table,
       symex_dereference_state,
       language_mode,
-      expr_is_not_null);
+      expr_is_not_null,
+      log);
 
     // std::cout << "**** " << format(tmp1) << '\n';
-    exprt tmp2 = dereference.dereference(tmp1);
+    exprt tmp2 =
+      dereference.dereference(tmp1, symex_config.show_points_to_sets);
     // std::cout << "**** " << format(tmp2) << '\n';
 
     expr.swap(tmp2);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 68fd360586b..8f6c3db9ee5 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -47,6 +47,7 @@ symex_configt::symex_configt(const optionst &options)
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
+    show_points_to_sets(options.get_bool_option("show-points-to-sets")),
     max_field_sensitivity_array_size(
       options.is_set("no-array-field-sensitivity")
         ? 0
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index 53a35f85f02..a26a374dc7b 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -28,15 +28,24 @@ class goto_program_dereferencet:protected dereference_callbackt
   // for the final argument to value_set_dereferencet.
   // This means that language-inappropriate values such as
   // (struct A*)some_integer_value in Java, may be returned.
+  // Note: value_set_dereferencet requires a messaget instance
+  // as on of its arguments to display the points-to set
+  // during symex. Display is not done during goto-program
+  // conversion. To ensure this the display_points_to_sets
+  // parameter in value_set_dereferencet::dereference()
+  // is set to false by default and is not changed by the
+  // goto program conversion modules. Similarly, here we set
+  // _log to be a default messaget instance.
   goto_program_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    value_setst &_value_sets)
+    value_setst &_value_sets,
+    const messaget &_log = messaget())
     : options(_options),
       ns(_ns),
       value_sets(_value_sets),
-      dereference(_ns, _new_symbol_table, *this, ID_nil, false)
+      dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log)
   {
   }
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 6c15e53593d..404fb0e1580 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
 #endif
 
 #include <util/arith_tools.h>
@@ -24,8 +23,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/format_expr.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
+#include <util/json_irep.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -60,7 +61,9 @@ static bool should_use_local_definition_for(const exprt &expr)
   return false;
 }
 
-exprt value_set_dereferencet::dereference(const exprt &pointer)
+exprt value_set_dereferencet::dereference(
+  const exprt &pointer,
+  bool display_points_to_sets)
 {
   if(pointer.type().id()!=ID_pointer)
     throw "dereference expected pointer type, but got "+
@@ -70,8 +73,9 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
-    exprt true_case = dereference(if_expr.true_case());
-    exprt false_case = dereference(if_expr.false_case());
+    exprt true_case = dereference(if_expr.true_case(), display_points_to_sets);
+    exprt false_case =
+      dereference(if_expr.false_case(), display_points_to_sets);
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
   else if(pointer.id() == ID_typecast)
@@ -90,14 +94,26 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
       const auto &if_expr = to_if_expr(*underlying);
       return if_exprt(
         if_expr.cond(),
-        dereference(typecast_exprt(if_expr.true_case(), pointer.type())),
-        dereference(typecast_exprt(if_expr.false_case(), pointer.type())));
+        dereference(
+          typecast_exprt(if_expr.true_case(), pointer.type()),
+          display_points_to_sets),
+        dereference(
+          typecast_exprt(if_expr.false_case(), pointer.type()),
+          display_points_to_sets));
     }
   }
 
   // type of the object
   const typet &type=pointer.type().subtype();
 
+  json_objectt json_result;
+  if(display_points_to_sets)
+  {
+    std::stringstream ss;
+    ss << format(pointer);
+    json_result["Pointer"] = json_stringt(ss.str());
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference pointer=" << format(pointer)
             << '\n';
@@ -107,6 +123,22 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   const std::vector<exprt> points_to_set =
     dereference_callback.get_value_set(pointer);
 
+  if(display_points_to_sets)
+  {
+    json_result["PointsToSetSize"] =
+      json_numbert(std::to_string(points_to_set.size()));
+
+    json_arrayt points_to_set_json;
+    for(auto p : points_to_set)
+    {
+      std::stringstream ss;
+      ss << format(p);
+      points_to_set_json.push_back(json_stringt(ss.str()));
+    }
+
+    json_result["PointsToSet"] = points_to_set_json;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference points_to_set={";
   for(auto p : points_to_set)
@@ -135,6 +167,22 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     compare_against_pointer = fresh_binder.symbol_expr();
   }
 
+  if(display_points_to_sets)
+  {
+    json_result["RetainedValuesSetSize"] =
+      json_numbert(std::to_string(points_to_set.size()));
+
+    json_arrayt retained_values_set_json;
+    for(auto &value : retained_values)
+    {
+      std::stringstream ss;
+      ss << format(value);
+      retained_values_set_json.push_back(json_stringt(ss.str()));
+    }
+
+    json_result["RetainedValuesSet"] = retained_values_set_json;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference retained_values={";
   for(const auto &value : retained_values)
@@ -224,6 +272,15 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   if(compare_against_pointer != pointer)
     value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value);
 
+  if(display_points_to_sets)
+  {
+    std::stringstream ss;
+    ss << format(value);
+    json_result["Value"] = json_stringt(ss.str());
+
+    log.status() << json_result;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_derefencet::dereference value=" << format(value)
             << '\n'
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index 4889a7cb362..d3ed72f724d 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <unordered_set>
 
+#include <util/message.h>
 #include <util/std_expr.h>
 
 #include "dereference_callback.h"
@@ -34,17 +35,20 @@ class value_set_dereferencet final
   ///   dereference failure
   /// \param _exclude_null_derefs: Ignore value-set entries that indicate a
   //    given dereference may follow a null pointer
+  /// \param _log: Messaget object for displaying points-to set
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     dereference_callbackt &_dereference_callback,
     const irep_idt _language_mode,
-    bool _exclude_null_derefs):
-    ns(_ns),
-    new_symbol_table(_new_symbol_table),
-    dereference_callback(_dereference_callback),
-    language_mode(_language_mode),
-    exclude_null_derefs(_exclude_null_derefs)
+    bool _exclude_null_derefs,
+    const messaget &_log)
+    : ns(_ns),
+      new_symbol_table(_new_symbol_table),
+      dereference_callback(_dereference_callback),
+      language_mode(_language_mode),
+      exclude_null_derefs(_exclude_null_derefs),
+      log(_log)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -52,7 +56,8 @@ class value_set_dereferencet final
   /// Dereference the given pointer-expression. Any errors are
   /// reported to the callback method given in the constructor.
   /// \param pointer: A pointer-typed expression, to be dereferenced.
-  exprt dereference(const exprt &pointer);
+  /// \param display_points_to_sets: Display size and contents of points to sets
+  exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
 
   /// Return value for `build_reference_to`; see that method for documentation.
   class valuet
@@ -105,6 +110,7 @@ class value_set_dereferencet final
   /// Flag indicating whether `value_set_dereferencet::dereference` should
   /// disregard an apparent attempt to dereference NULL
   const bool exclude_null_derefs;
+  const messaget &log;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H