diff --git a/infer/src/IR/Attributes.ml b/infer/src/IR/Attributes.ml
index 1c3769026..88775d11f 100644
--- a/infer/src/IR/Attributes.ml
+++ b/infer/src/IR/Attributes.ml
@@ -6,15 +6,27 @@
  * LICENSE file in the root directory of this source tree. An additional grant
  * of patent rights can be found in the PATENTS file in the same directory.
  *)
+
 open! IStd
+module F = Format
 module L = Logging
 
 type attributes_kind = ProcUndefined | ProcObjCAccessor | ProcDefined [@@deriving compare]
 
-let int64_of_attributes_kind =
-  (* only allocate this once *)
-  let int64_two = Int64.of_int 2 in
-  function ProcUndefined -> Int64.zero | ProcObjCAccessor -> Int64.one | ProcDefined -> int64_two
+let equal_attributes_kind = [%compare.equal : attributes_kind]
+
+let attributes_kind_to_int64 =
+  [(ProcUndefined, Int64.zero); (ProcObjCAccessor, Int64.one); (ProcDefined, Int64.of_int 2)]
+
+
+let int64_of_attributes_kind a =
+  List.Assoc.find_exn ~equal:equal_attributes_kind attributes_kind_to_int64 a
+
+
+let deserialize_attributes_kind =
+  let int64_to_attributes_kind = List.Assoc.inverse attributes_kind_to_int64 in
+  function[@warning "-8"]
+    | Sqlite3.Data.INT n -> List.Assoc.find_exn ~equal:Int64.equal int64_to_attributes_kind n
 
 
 let proc_kind_of_attr (proc_attributes: ProcAttributes.t) =
@@ -134,3 +146,12 @@ let find_file_capturing_procedure pname =
             `Source
       in
       (source_file, origin) )
+
+
+let pp_attributes_kind f = function
+  | ProcUndefined ->
+      F.pp_print_string f "<undefined>"
+  | ProcObjCAccessor ->
+      F.pp_print_string f "<ObjC accessor>"
+  | ProcDefined ->
+      F.pp_print_string f "<defined>"
diff --git a/infer/src/IR/Attributes.mli b/infer/src/IR/Attributes.mli
index 733f28c6b..ac61214d2 100644
--- a/infer/src/IR/Attributes.mli
+++ b/infer/src/IR/Attributes.mli
@@ -11,6 +11,10 @@
 
 open! IStd
 
+type attributes_kind
+
+val deserialize_attributes_kind : Sqlite3.Data.t -> attributes_kind
+
 val store : ProcAttributes.t -> unit
 (** Save .attr file for the procedure into the attributes database. *)
 
@@ -24,3 +28,5 @@ val find_file_capturing_procedure : Typ.Procname.t -> (SourceFile.t * [`Include
 (** Find the file where the procedure was captured, if a cfg for that file exists.
    Return also a boolean indicating whether the procedure is defined in an
    include file. *)
+
+val pp_attributes_kind : Format.formatter -> attributes_kind -> unit
diff --git a/infer/src/IR/PredSymb.ml b/infer/src/IR/PredSymb.ml
index 21cc891b5..fbae0af67 100644
--- a/infer/src/IR/PredSymb.ml
+++ b/infer/src/IR/PredSymb.ml
@@ -18,11 +18,24 @@ type func_attribute =
   | FA_sentinel of int * int  (** __attribute__((sentinel(int, int))) *)
   [@@deriving compare]
 
+let pp_func_attribute fmt = function FA_sentinel (i, j) -> F.fprintf fmt "sentinel(%d,%d)" i j
+
 (** Visibility modifiers. *)
 type access = Default | Public | Private | Protected [@@deriving compare]
 
 let equal_access = [%compare.equal : access]
 
+let string_of_access = function
+  | Default ->
+      "<Default>"
+  | Public ->
+      "<Public>"
+  | Private ->
+      "<Private>"
+  | Protected ->
+      "<Protected>"
+
+
 (** Return the value of the FA_sentinel attribute in [attr_list] if it is found *)
 let get_sentinel_func_attribute_value attr_list =
   match attr_list with
diff --git a/infer/src/IR/PredSymb.mli b/infer/src/IR/PredSymb.mli
index 88f53e773..fe1b565f5 100644
--- a/infer/src/IR/PredSymb.mli
+++ b/infer/src/IR/PredSymb.mli
@@ -18,6 +18,8 @@ module F = Format
 
 type func_attribute = FA_sentinel of int * int [@@deriving compare]
 
+val pp_func_attribute : F.formatter -> func_attribute -> unit
+
 val get_sentinel_func_attribute_value : func_attribute list -> (int * int) option
 (** Return the value of the FA_sentinel attribute in [attr_list] if it is found *)
 
@@ -26,6 +28,8 @@ type access = Default | Public | Private | Protected [@@deriving compare]
 
 val equal_access : access -> access -> bool
 
+val string_of_access : access -> string
+
 type mem_kind =
   | Mmalloc  (** memory allocated with malloc *)
   | Mnew  (** memory allocated with new *)
diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml
index 4325a7c8d..f564b2f73 100644
--- a/infer/src/IR/ProcAttributes.ml
+++ b/infer/src/IR/ProcAttributes.ml
@@ -60,12 +60,32 @@ let kind_of_objc_accessor_type accessor =
   match accessor with Objc_getter _ -> "getter" | Objc_setter _ -> "setter"
 
 
+let pp_objc_accessor_type fmt objc_accessor_type =
+  let fieldname, typ, annots =
+    match objc_accessor_type with Objc_getter field | Objc_setter field -> field
+  in
+  F.fprintf fmt "%s<%a:%a@,[%a]>"
+    (kind_of_objc_accessor_type objc_accessor_type)
+    Typ.Fieldname.pp fieldname (Typ.pp Pp.text) typ
+    (Pp.semicolon_seq (Pp.pair ~fst:Annot.pp ~snd:F.pp_print_bool))
+    annots
+
+
 type var_attribute = Modify_in_block [@@deriving compare]
 
+let string_of_var_attribute = function Modify_in_block -> "<Modify_in_block>"
+
 let var_attribute_equal = [%compare.equal : var_attribute]
 
 type var_data = {name: Mangled.t; typ: Typ.t; attributes: var_attribute list} [@@deriving compare]
 
+let pp_var_data fmt {name; typ; attributes} =
+  F.fprintf fmt "{@[<h>name=@ %a;@,typ=@ %a;@,attributes=@ %a@]}" Mangled.pp name (Typ.pp Pp.text)
+    typ
+    (Pp.semicolon_seq (Pp.to_string ~f:string_of_var_attribute))
+    attributes
+
+
 type t =
   { access: PredSymb.access  (** visibility access *)
   ; captured: (Mangled.t * Typ.t) list  (** name and type of variables captured in blocks *)
@@ -126,6 +146,64 @@ let default proc_name =
   ; source_file_captured= SourceFile.invalid __FILE__ }
 
 
+let pp_parameters = Pp.semicolon_seq (Pp.pair ~fst:Mangled.pp ~snd:(Typ.pp Pp.text))
+
+let pp fmt attributes =
+  let[@warning "+9"] { access
+                     ; captured
+                     ; did_preanalysis
+                     ; err_log
+                     ; exceptions
+                     ; formals
+                     ; const_formals
+                     ; by_vals
+                     ; func_attributes
+                     ; is_abstract
+                     ; is_bridge_method
+                     ; is_defined
+                     ; is_cpp_noexcept_method
+                     ; is_java_synchronized_method
+                     ; is_model
+                     ; is_specialized
+                     ; is_synthetic_method
+                     ; clang_method_kind
+                     ; loc
+                     ; translation_unit
+                     ; locals
+                     ; method_annotation
+                     ; objc_accessor
+                     ; proc_flags
+                     ; proc_name
+                     ; ret_type
+                     ; source_file_captured } =
+    attributes
+  in
+  Format.fprintf fmt
+    "{@[access= %a;@ captured= [@[%a@]];@ did_preanalysis= %b;@ err_log= [@[%a%a@]];@ exceptions= \
+     [@[%a@]];@ formals= [@[%a@]];@ const_formals= [@[%a@]];@ by_vals= [@[%a@]];@ \
+     func_attributes= [@[%a@]];@ is_abstract= %b;@ is_bridge_method= %b;@ is_defined= %b;@ \
+     is_cpp_noexcept_method= %b;@ is_java_synchronized_method= %b;@ is_model= %b;@ \
+     is_specialized= %b;@ is_synthetic_method= %b;@ clang_method_kind= %a;@ loc= %a;@ \
+     translation_unit= %a;@ locals= [@[%a@]];@ method_annotation= %a;@ objc_accessor= %a;@ \
+     proc_flags= [@[%a@]];@ proc_name= %a;@ ret_type= %a;@ source_file_captured=%a@]}"
+    (Pp.to_string ~f:PredSymb.string_of_access)
+    access pp_parameters captured did_preanalysis Errlog.pp_errors err_log Errlog.pp_warnings
+    err_log
+    (Pp.semicolon_seq F.pp_print_string)
+    exceptions pp_parameters formals (Pp.semicolon_seq F.pp_print_int) const_formals
+    (Pp.semicolon_seq F.pp_print_int) by_vals
+    (Pp.semicolon_seq PredSymb.pp_func_attribute)
+    func_attributes is_abstract is_bridge_method is_defined is_cpp_noexcept_method
+    is_java_synchronized_method is_model is_specialized is_synthetic_method
+    (Pp.to_string ~f:string_of_clang_method_kind)
+    clang_method_kind Location.pp loc (Pp.option SourceFile.pp) translation_unit
+    (Pp.semicolon_seq pp_var_data) locals (Annot.Method.pp "") method_annotation
+    (Pp.option pp_objc_accessor_type) objc_accessor
+    (Pp.hashtbl ~key:F.pp_print_string ~value:F.pp_print_string)
+    proc_flags Typ.Procname.pp proc_name (Typ.pp Pp.text) ret_type SourceFile.pp
+    source_file_captured
+
+
 module SQLite = SqliteUtils.MarshalledData (struct
   type nonrec t = t
 end)
diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli
index 2f7a64f80..5f2211f2a 100644
--- a/infer/src/IR/ProcAttributes.mli
+++ b/infer/src/IR/ProcAttributes.mli
@@ -77,4 +77,6 @@ type t =
 val default : Typ.Procname.t -> t
 (** Create a proc_attributes with default values. *)
 
+val pp : Format.formatter -> t -> unit
+
 module SQLite : SqliteUtils.Data with type t = t
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 5002aadd5..125b73dd7 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -1160,6 +1160,11 @@ module Procname = struct
       Base.Hashtbl.find_or_add pname_to_key pname ~default
 
 
+    let deserialize : Sqlite3.Data.t -> t = function[@warning "-8"]
+      | Sqlite3.Data.BLOB b ->
+          Marshal.from_string b 0
+
+
     let clear_cache () = Base.Hashtbl.clear pname_to_key
   end
 
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 0070f3964..ddbfeb2b7 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -464,6 +464,8 @@ module Procname : sig
   module SQLite : sig
     val serialize : t -> Sqlite3.Data.t
 
+    val deserialize : Sqlite3.Data.t -> t
+
     val clear_cache : unit -> unit
   end
 
diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml
index 5cec9f77b..bf962c895 100644
--- a/infer/src/backend/InferPrint.ml
+++ b/infer/src/backend/InferPrint.ml
@@ -593,7 +593,7 @@ module PreconditionStats = struct
     L.result "Procedures with data constraints: %d@." !nr_dataconstraints
 end
 
-(* Wrapper of an issue that compares all parts except the procname *)
+(** Wrapper of an issue that compares all parts except the procname *)
 module Issue = struct
   type err_data_ = Errlog.err_data
 
diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml
new file mode 100644
index 000000000..1c184d9ea
--- /dev/null
+++ b/infer/src/backend/Procedures.ml
@@ -0,0 +1,68 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+
+let select_all_procedures_like_statement =
+  ResultsDatabase.register_statement
+    "SELECT * FROM procedures WHERE proc_name LIKE :pname_like AND source_file LIKE \
+     :source_file_like"
+
+
+let pp_all ?filter ~proc_name ~attr_kind ~source_file ~proc_attributes fmt () =
+  let source_file_like, pname_like =
+    match filter with
+    | None ->
+        let wildcard = Sqlite3.Data.TEXT "%" in
+        (wildcard, wildcard)
+    | Some filter_string ->
+      match String.lsplit2 ~on:':' filter_string with
+      | Some (source_file_like, pname_like) ->
+          (Sqlite3.Data.TEXT source_file_like, Sqlite3.Data.TEXT pname_like)
+      | None ->
+          L.die UserError
+            "Invalid filter for procedures. Please see the documentation for --procedures-filter \
+             in `infer explore --help`."
+  in
+  ResultsDatabase.with_registered_statement select_all_procedures_like_statement ~f:(fun db stmt ->
+      Sqlite3.bind stmt 1 (* :pname_like *) pname_like
+      |> SqliteUtils.check_sqlite_error db ~log:"procedures filter pname bind" ;
+      Sqlite3.bind stmt 2 (* :source_file_like *) source_file_like
+      |> SqliteUtils.check_sqlite_error db ~log:"procedures filter source file bind" ;
+      let pp_if ?(newline= false) condition deserialize pp fmt column =
+        if condition then (
+          if newline then F.fprintf fmt "@\n  " ;
+          F.fprintf fmt "%a@ " pp (Sqlite3.column stmt column |> deserialize) )
+      in
+      let rec aux () =
+        match Sqlite3.step stmt with
+        | Sqlite3.Rc.ROW ->
+            let proc_name_hum =
+              (* same as proc_name for now, will change later *)
+              match[@warning "-8"] Sqlite3.column stmt 0 with Sqlite3.Data.TEXT s -> s
+            in
+            Format.fprintf fmt "@[<h2>%s:@ %a%a%a%a@]@\n" proc_name_hum
+              (pp_if source_file SourceFile.SQLite.deserialize SourceFile.pp)
+              2
+              (pp_if proc_name Typ.Procname.SQLite.deserialize Typ.Procname.pp)
+              0
+              (pp_if attr_kind Attributes.deserialize_attributes_kind Attributes.pp_attributes_kind)
+              1
+              (pp_if ~newline:true proc_attributes ProcAttributes.SQLite.deserialize
+                 ProcAttributes.pp)
+              3 ;
+            aux ()
+        | DONE ->
+            ()
+        | err ->
+            L.die InternalError "procedures_iter: %s (%s)" (Sqlite3.Rc.to_string err)
+              (Sqlite3.errmsg db)
+      in
+      aux () )
diff --git a/infer/src/backend/Procedures.mli b/infer/src/backend/Procedures.mli
new file mode 100644
index 000000000..40716657e
--- /dev/null
+++ b/infer/src/backend/Procedures.mli
@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+val pp_all :
+  ?filter:string -> proc_name:bool -> attr_kind:bool -> source_file:bool -> proc_attributes:bool
+  -> Format.formatter -> unit -> unit
diff --git a/infer/src/base/CommandDoc.ml b/infer/src/base/CommandDoc.ml
index a5fca4980..30cadb8b8 100644
--- a/infer/src/base/CommandDoc.ml
+++ b/infer/src/base/CommandDoc.ml
@@ -126,11 +126,16 @@ let diff =
 let explore =
   mk_command_doc ~title:"Infer Explore"
     ~short_description:"explore the error traces in infer reports"
-    ~synopsis:{|$(b,infer) $(b,explore) $(i,[options])|}
+    ~synopsis:
+      {|$(b,infer) $(b,explore) $(i,[options])
+$(b,infer) $(b,explore) $(b,--procedures) $(i,[options])|}
     ~description:
       [ `P
           "Show the list of bugs on the console and explore symbolic program traces emitted by \
-           infer to explain a report. Can also generate an HTML report from a JSON report." ]
+           infer to explain a report. Can also generate an HTML report from a JSON report."
+      ; `P
+          "If $(b,--procedures) is passed, print information about each procedure captured by \
+           infer." ]
     ~see_also:InferCommand.([Report; Run])
 
 
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 256cd38b4..190e97f4a 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -1667,6 +1667,42 @@ and print_using_diff =
     "Highlight the difference w.r.t. the previous prop when printing symbolic execution debug info"
 
 
+and procedures =
+  CLOpt.mk_bool ~long:"procedures"
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "Print functions and methods discovered by infer"
+
+
+and procedures_attributes =
+  CLOpt.mk_bool ~long:"procedures-attributes"
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "Print the attributes of each procedure in the output of $(b,--procedures)"
+
+
+and procedures_definedness =
+  CLOpt.mk_bool ~long:"procedures-definedness" ~default:true
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "Include procedures definedness in the output of $(b,--procedures), i.e. whether the \
+     procedure definition was found, or only the procedure declaration, or the procedure is an \
+     auto-generated Objective-C accessor"
+
+
+and procedures_filter =
+  CLOpt.mk_string_opt ~long:"procedures-filter" ~meta:"filter"
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "With $(b,--procedures), only print functions and methods (procedures) matching the specified \
+     $(i,filter). A procedure filter is of the form $(i,path_pattern:procedure_name). Patterns \
+     are interpreted by SQLite: use $(b,_) to match any one character and $(b,%) to match any \
+     sequence of characters. For instance, to keep only methods named \"foo\", one can use the \
+     filter \"%:foo\"."
+
+
+and procedures_name =
+  CLOpt.mk_bool ~long:"procedures-name"
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "Include procedures names in the output of $(b,--procedures)"
+
+
 and procedures_per_process =
   CLOpt.mk_int ~long:"procedures-per-process" ~default:1000 ~meta:"int"
     "Specify the number of procedures to analyze per process when using \
@@ -1674,6 +1710,13 @@ and procedures_per_process =
      groups of procedures."
 
 
+and procedures_source_file =
+  CLOpt.mk_bool ~long:"procedures-source-file" ~default:true
+    ~in_help:InferCommand.([(Explore, manual_generic)])
+    "Include the source file in which the procedure definition or declaration was found in the \
+     output of $(b,--procedures)"
+
+
 and procs_csv =
   CLOpt.mk_path_opt ~deprecated:["procs"] ~long:"procs-csv" ~meta:"file"
     "Write statistics for each procedure in CSV format to a file"
@@ -2607,8 +2650,20 @@ and print_types = !print_types
 
 and print_using_diff = !print_using_diff
 
+and procedures = !procedures
+
+and procedures_attributes = !procedures_attributes
+
+and procedures_definedness = !procedures_definedness
+
+and procedures_filter = !procedures_filter
+
+and procedures_name = !procedures_name
+
 and procedures_per_process = !procedures_per_process
 
+and procedures_source_file = !procedures_source_file
+
 and procs_csv = !procs_csv
 
 and project_root = !project_root
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 82b9b2520..4aeab399b 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -181,6 +181,18 @@ val pp_version : Format.formatter -> unit -> unit
 
 val proc_stats_filename : string
 
+val procedures : bool
+
+val procedures_attributes : bool
+
+val procedures_definedness : bool
+
+val procedures_filter : string option
+
+val procedures_name : bool
+
+val procedures_source_file : bool
+
 val property_attributes : string
 
 val report : bool
diff --git a/infer/src/infer.ml b/infer/src/infer.ml
index 1b0b61e81..9b6f366cf 100644
--- a/infer/src/infer.ml
+++ b/infer/src/infer.ml
@@ -145,6 +145,13 @@ let () =
       run (Lazy.force Driver.mode_from_command_line)
   | Diff ->
       Diff.diff (Lazy.force Driver.mode_from_command_line)
+  | Explore when Config.procedures ->
+      L.result "%a"
+        Config.(
+          Procedures.pp_all ?filter:procedures_filter ~proc_name:procedures_name
+            ~attr_kind:procedures_definedness ~source_file:procedures_source_file
+            ~proc_attributes:procedures_attributes)
+        ()
   | Explore ->
       let if_some key opt args =
         match opt with None -> args | Some arg -> key :: string_of_int arg :: args
diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml
index c35896887..c34bcb7a0 100644
--- a/infer/src/istd/Pp.ml
+++ b/infer/src/istd/Pp.ml
@@ -167,3 +167,9 @@ let cli_args fmt args =
   in
   pp_args fmt args ;
   pp_argfile_args String.Set.empty fmt args
+
+
+let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
+
+let hashtbl ~key ~value fmt h =
+  Caml.Hashtbl.iter (fun k v -> F.fprintf fmt "%a@ ->@ %a" key k value v) h
diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli
index b7aa79101..3cf1fbf28 100644
--- a/infer/src/istd/Pp.mli
+++ b/infer/src/istd/Pp.mli
@@ -87,3 +87,11 @@ val current_time : F.formatter -> unit -> unit
 
 val elapsed_time : F.formatter -> unit -> unit
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
+
+val pair :
+  fst:(F.formatter -> 'a -> unit) -> snd:(F.formatter -> 'b -> unit) -> F.formatter -> 'a * 'b
+  -> unit
+
+val hashtbl :
+  key:(F.formatter -> 'a -> unit) -> value:(F.formatter -> 'b -> unit) -> F.formatter
+  -> ('a, 'b) Caml.Hashtbl.t -> unit