diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 080448dd6..402385e84 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1746,6 +1746,10 @@ INTERNAL OPTIONS
            Activates: Detailed tracing information during prop re-arrangement
            operations (Conversely: --no-trace-rearrange)
 
+       --trace-topl
+           Activates: Detailed tracing information during TOPL analysis
+           (Conversely: --no-trace-topl)
+
        --tracing
            Activates: Report error traces for runtime exceptions (Java only):
            generate preconditions for runtimeexceptions in Java and report
diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml
index 886a6b025..7c7002389 100644
--- a/infer/src/IR/Instrs.ml
+++ b/infer/src/IR/Instrs.ml
@@ -91,6 +91,14 @@ let map_changed =
     if phys_equal instrs instrs' then t else NotReversed instrs'
 
 
+let concat_map_changed ~equal (NotReversed instrs as t) ~f =
+  let instrs' = Array.concat_map ~f instrs in
+  if
+    Int.equal (Array.length instrs) (Array.length instrs')
+    && Array.for_all2_exn ~f:equal instrs instrs'
+  then t
+  else NotReversed instrs'
+
 let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs)
 
 (* Functions on both reversed and non-reversed arrays *)
diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli
index 80cd12c8f..a973d819a 100644
--- a/infer/src/IR/Instrs.mli
+++ b/infer/src/IR/Instrs.mli
@@ -33,6 +33,12 @@ val map_changed :
   -> f:(Sil.instr -> Sil.instr)
   -> not_reversed_t
 
+val concat_map_changed :
+     equal:(Sil.instr -> Sil.instr -> bool)
+  -> not_reversed_t
+  -> f:(Sil.instr -> Sil.instr array)
+  -> not_reversed_t
+
 val reverse_order : not_reversed_t -> reversed t
 
 val is_empty : _ t -> bool
diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml
index b0305bfe2..ffdad67e2 100644
--- a/infer/src/IR/Procdesc.ml
+++ b/infer/src/IR/Procdesc.ml
@@ -228,6 +228,15 @@ module Node = struct
       true )
 
 
+  (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *)
+  let replace_instrs_by node ~f =
+    let instrs' = Instrs.concat_map_changed ~equal:phys_equal node.instrs ~f:(f node) in
+    if phys_equal instrs' node.instrs then false
+    else (
+      node.instrs <- instrs' ;
+      true )
+
+
   let pp_stmt fmt = function
     | AssertionFailure ->
         F.pp_print_string fmt "Assertion failure"
@@ -520,13 +529,22 @@ let find_map_instrs pdesc ~f =
   find_map_nodes ~f:find_map_node pdesc
 
 
-let replace_instrs pdesc ~f =
-  let f updated node =
-    Node.replace_instrs ~f node || (* do not short-circuit [Node.replace_instrs] *) updated
-  in
+let update_nodes pdesc ~(update : Node.t -> bool) : bool =
+  let f acc node = update node || acc in
+  (* do not shortcut call to [update] *)
   fold_nodes pdesc ~init:false ~f
 
 
+let replace_instrs pdesc ~f =
+  let update node = Node.replace_instrs ~f node in
+  update_nodes pdesc ~update
+
+
+let replace_instrs_by pdesc ~f =
+  let update node = Node.replace_instrs_by ~f node in
+  update_nodes pdesc ~update
+
+
 (** fold between two nodes or until we reach a branching structure *)
 let fold_slope_range =
   let rec aux node visited acc ~f =
diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli
index cdf8bea73..fd1fae9d3 100644
--- a/infer/src/IR/Procdesc.mli
+++ b/infer/src/IR/Procdesc.mli
@@ -264,6 +264,10 @@ val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr) -> bool
 (** Map and replace the instructions to be executed.
     Returns true if at least one substitution occured. *)
 
+val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool
+(** Like [replace_instrs], but slower, and each instruction may be replaced                                   
+by 0, 1, or more instructions. *)
+
 val iter_nodes : (Node.t -> unit) -> t -> unit
 (** iterate over all the nodes of a procedure *)
 
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index eda8c2c24..e0b38d589 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -447,6 +447,8 @@ module Name = struct
       let java_lang_object = make ~package:"java.lang" "Object"
 
       let java_lang_string = make ~package:"java.lang" "String"
+
+      let void = make "void"
     end
 
     let from_string name_str = JavaClass (Mangled.from_string name_str)
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 1dda3515e..fb753554d 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -199,6 +199,8 @@ module Name : sig
 
       val java_lang_string : t
 
+      val void : t
+
       val package : t -> string option
 
       val type_name : t -> string
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index ec3610792..df04ecfaf 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -59,8 +59,13 @@ let should_be_analyzed proc_attributes =
   (not (is_active proc_name)) (* avoid infinite loops *) && not (already_analyzed proc_name)
 
 
+let get_proc_attr proc_name =
+  IList.force_until_first_some
+    [lazy (Summary.proc_resolve_attributes proc_name); lazy (Topl.get_proc_attr proc_name)]
+
+
 let procedure_should_be_analyzed proc_name =
-  match Summary.proc_resolve_attributes proc_name with
+  match get_proc_attr proc_name with
   | Some proc_attributes when Config.reactive_capture && not proc_attributes.is_defined ->
       (* try to capture procedure first *)
       let defined_proc_attributes = OndemandCapture.try_capture proc_attributes in
@@ -270,11 +275,10 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc =
 
 (** Find a proc desc for the procedure, perhaps loading it from disk. *)
 let get_proc_desc callee_pname =
-  match Procdesc.load callee_pname with
-  | Some _ as pdesc_opt ->
-      pdesc_opt
-  | None ->
-      Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)
+  IList.force_until_first_some
+    [ lazy (Procdesc.load callee_pname)
+    ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname))
+    ; lazy (Topl.get_proc_desc callee_pname) ]
 
 
 (** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 12998691b..dad5100ea 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -2289,6 +2289,10 @@ and trace_rearrange =
     "Detailed tracing information during prop re-arrangement operations"
 
 
+and trace_topl =
+  CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during TOPL analysis"
+
+
 and tracing =
   CLOpt.mk_bool ~deprecated:["tracing"] ~long:"tracing"
     "Report error traces for runtime exceptions (Java only): generate preconditions for \
@@ -3141,6 +3145,8 @@ and trace_join = !trace_join
 
 and trace_rearrange = !trace_rearrange
 
+and trace_topl = !trace_topl
+
 and tracing = !tracing
 
 and tv_commit = !tv_commit
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 9f3eed0bc..34aa73217 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -690,6 +690,8 @@ val trace_ondemand : bool
 
 val trace_rearrange : bool
 
+val trace_topl : bool
+
 val tracing : bool
 
 val tv_commit : string option
diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml
index 150ad011e..25bd97307 100644
--- a/infer/src/biabduction/interproc.ml
+++ b/infer/src/biabduction/interproc.ml
@@ -1253,7 +1253,7 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t =
 let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
-  if not (List.is_empty Config.topl_properties) then Topl.init () ;
+  if Topl.is_active () then Topl.instrument tenv proc_desc ;
   try analyze_procedure_aux summary exe_env tenv proc_desc
   with exn ->
     IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
diff --git a/infer/src/deadcode/dune.in b/infer/src/deadcode/dune.in
index 05fb2563d..a7fd3335e 100644
--- a/infer/src/deadcode/dune.in
+++ b/infer/src/deadcode/dune.in
@@ -16,7 +16,7 @@ Format.sprintf
  (ocamlopt_flags (%s))
  (libraries %s)
  (modules All_infer_in_one_file)
- (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check))
+ (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
 )
 |}
   (String.concat " " common_cflags)
diff --git a/infer/src/dune.in b/infer/src/dune.in
index dc6b26133..03aac3b64 100644
--- a/infer/src/dune.in
+++ b/infer/src/dune.in
@@ -64,7 +64,7 @@ let stanzas =
  (ocamlopt_flags (%s))
  (libraries %s)
  (modules :standard \ %s infertop)
- (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check))
+ (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
 )
 
 (documentation
@@ -84,7 +84,7 @@ let stanzas =
  (ocamlopt_flags (%s))
  (libraries InferModules)
  (modules %s)
- (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check))
+ (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
 )
 |}
         (String.concat " " infer_binaries)
@@ -98,7 +98,7 @@ let stanzas =
  (flags (%s))
  (libraries utop InferModules)
  (modules Infertop)
- (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check))
+ (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
  (link_flags (-linkall -warn-error -31))
 )
 |}
diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml
index 74ebdb1ff..195bfff71 100644
--- a/infer/src/istd/IList.ml
+++ b/infer/src/istd/IList.ml
@@ -182,6 +182,8 @@ let remove_first =
   fun list ~f -> aux list ~f []
 
 
+let force_until_first_some lazies = List.find_map lazies ~f:Lazy.force
+
 let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf =
   let rec aux n = function
     | [] ->
diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli
index 61d519ac1..17dd0386e 100644
--- a/infer/src/istd/IList.mli
+++ b/infer/src/istd/IList.mli
@@ -46,6 +46,10 @@ val opt_cons : 'a option -> 'a list -> 'a list
 
 val remove_first : 'a list -> f:('a -> bool) -> 'a list option
 
+val force_until_first_some : 'a option lazy_t list -> 'a option
+(** [force_until_first_some xs] forces the computation of each element of [xs] and returns the first
+that matches (Some _); or, if no such element exists, it returns None. *)
+
 val pp_print_list :
      max:int
   -> ?pp_sep:(Format.formatter -> unit -> unit)
diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml
index aaf393b00..fcd06064d 100644
--- a/infer/src/topl/Topl.ml
+++ b/infer/src/topl/Topl.ml
@@ -8,9 +8,7 @@
 open! IStd
 module L = Logging
 
-let initialized = ref false
-
-let properties = ref []
+let tt fmt = L.d_printf "ToplTrace: " ; L.d_printfln fmt
 
 let parse topl_file =
   let f ch =
@@ -25,7 +23,178 @@ let parse topl_file =
   with Sys_error msg -> L.(die UserError) "@[topl:%s: %s@]@\n@?" topl_file msg
 
 
-let init () =
-  if not !initialized then (
-    properties := List.concat_map ~f:parse Config.topl_properties ;
-    initialized := true )
+let properties = lazy (List.concat_map ~f:parse Config.topl_properties)
+
+let automaton = lazy (ToplAutomaton.make (Lazy.force properties))
+
+let is_active () = not (List.is_empty (Lazy.force properties))
+
+let cfg = Cfg.create ()
+
+let sourcefile = SourceFile.create "SynthesizedToplProperty.java"
+
+let sourcefile_location = Location.none sourcefile
+
+(* NOTE: For now, Topl is mostly untyped; that is, everything has type Object. *)
+let type_of_paramtyp (_t : Typ.Procname.Parameter.t) : Typ.t =
+  let classname = Typ.mk (Tstruct Typ.Name.Java.java_lang_object) in
+  Typ.mk (Tptr (classname, Pk_pointer))
+
+
+(** NOTE: Similar to [JTrans.formals_from_signature]. *)
+let formals_of_procname proc_name =
+  let params = Typ.Procname.get_parameters proc_name in
+  let new_arg_name =
+    let n = ref (-1) in
+    fun () -> incr n ; Printf.sprintf "arg%d" !n
+  in
+  let f t =
+    let name = Mangled.from_string (new_arg_name ()) in
+    let typ = type_of_paramtyp t in
+    (name, typ)
+  in
+  List.map ~f params
+
+
+(** The procedure description and its nodes will have location [sourcefile_location]. *)
+let empty_proc_desc proc_name =
+  let attr =
+    let formals = formals_of_procname proc_name in
+    let is_defined = true in
+    let loc = sourcefile_location in
+    {(ProcAttributes.default sourcefile proc_name) with formals; is_defined; loc}
+  in
+  let proc_desc = Cfg.create_proc_desc cfg attr in
+  let start_node =
+    Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Start_node []
+  in
+  let exit_node = Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Exit_node [] in
+  Procdesc.node_set_succs_exn proc_desc start_node [exit_node] [exit_node] ;
+  Procdesc.set_start_node proc_desc start_node ;
+  Procdesc.set_exit_node proc_desc exit_node ;
+  proc_desc
+
+
+let is_synthesized = function
+  | Typ.Procname.Java j ->
+      String.equal "topl.Property" (Typ.Procname.Java.get_class_name j)
+  | _ ->
+      false
+
+
+let get_proc_desc proc_name =
+  if is_synthesized proc_name then Some ((* TODO *) empty_proc_desc proc_name) else None
+
+
+let get_proc_attr proc_name =
+  (* TODO: optimize -- don't generate body just to get attributes  *)
+  Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name)
+
+
+let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton)
+
+(** Checks whether the method name and the number of arguments matches the conditions in a
+transition label. Possible optimization: also evaluate if arguments equal certain constants. *)
+let evaluate_static_guard label (e_fun, arg_ts) =
+  let match_name () =
+    match e_fun with
+    | Exp.Const (Const.Cfun n) ->
+        (* TODO: perhaps handle inheritance *)
+        let name = Typ.Procname.hashable_name n in
+        let re = Str.regexp label.ToplAst.procedure_name in
+        let result = Str.string_match re name 0 in
+        if Config.trace_topl then
+          tt "match name='%s' re='%s' result=%b" name label.ToplAst.procedure_name result ;
+        result
+    | _ ->
+        false
+  in
+  let match_args () =
+    let same_length xs ys = Option.is_some (List.zip xs ys) in
+    Option.value_map label.ToplAst.arguments ~f:(same_length arg_ts) ~default:true
+  in
+  match_name () && match_args ()
+
+
+(** For each transition in the automaton, evaluate its static guard. *)
+let get_active_transitions e_fun arg_ts =
+  let a = Lazy.force automaton in
+  let f i = evaluate_static_guard (ToplAutomaton.transition a i).label (e_fun, arg_ts) in
+  Array.init (ToplAutomaton.tcount a) ~f
+
+
+let topl_class_exp =
+  let class_name = Mangled.from_string "topl.Property" in
+  let var_name = Pvar.mk_global class_name in
+  Exp.Lvar var_name
+
+
+let topl_class_name : Typ.Name.t = Typ.Name.Java.from_string "topl.Property"
+
+let topl_class_typ = Typ.mk (Tstruct topl_class_name)
+
+let transition_field_name i = Typ.Fieldname.Java.from_string (Printf.sprintf "transition%d" i)
+
+let transition_var i = Exp.Lfield (topl_class_exp, transition_field_name i, topl_class_typ)
+
+let set_transitions loc active_transitions =
+  let store i b =
+    let value = if b then Exp.one else Exp.zero in
+    Sil.Store (transition_var i, topl_class_typ, value, loc)
+  in
+  Array.mapi ~f:store active_transitions
+
+
+let topl_fun name n =
+  let ret_typ = Some Typ.Name.Java.Split.void in
+  let args_typ = List.init n ~f:(fun _ -> Typ.Name.Java.Split.java_lang_object) in
+  Exp.Const
+    (Const.Cfun
+       (Typ.Procname.Java
+          (Typ.Procname.Java.make topl_class_name ret_typ name args_typ Typ.Procname.Java.Static)))
+
+
+let call_save_args loc ret_id ret_typ arg_ts =
+  let arg_ts = arg_ts @ [(Exp.Var ret_id, ret_typ)] in
+  let e_fun = topl_fun "saveArgs" (List.length arg_ts) in
+  let ret_id = Ident.create_fresh Ident.knormal in
+  let ret_typ = Typ.mk Tvoid in
+  [|Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, CallFlags.default)|]
+
+
+let call_execute loc =
+  let e_fun = topl_fun "execute" 0 in
+  let ret_id = Ident.create_fresh Ident.knormal in
+  let ret_typ = Typ.mk Tvoid in
+  [|Sil.Call ((ret_id, ret_typ), e_fun, [], loc, CallFlags.default)|]
+
+
+let instrument_instruction = function
+  | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i ->
+      let active_transitions = get_active_transitions e_fun arg_ts in
+      if not (Array.exists ~f:(fun x -> x) active_transitions) then [|i|]
+      else
+        let i1s = set_transitions loc active_transitions in
+        let i2s = call_save_args loc ret_id ret_typ arg_ts in
+        let i3s = call_execute loc in
+        Array.concat [[|i|]; i1s; i2s; i3s]
+  | i ->
+      [|i|]
+
+
+(* PRE: Calling [Tenv.mk_struct tenv <args>] twice is a no-op. *)
+let add_types tenv =
+  let transition_field i = (transition_field_name i, Typ.mk (Tint IBool), []) in
+  let rec transitions n =
+    if Int.equal n 0 then [] else transition_field (n - 1) :: transitions (n - 1)
+  in
+  let statics = transitions (get_transitions_count ()) in
+  let _topl_class = Tenv.mk_struct tenv topl_class_name ~statics in
+  ()
+
+
+let instrument tenv procdesc =
+  add_types tenv ;
+  let f _node = instrument_instruction in
+  let _updated = Procdesc.replace_instrs_by procdesc ~f in
+  ()
diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli
index 324a04f88..550f9a075 100644
--- a/infer/src/topl/Topl.mli
+++ b/infer/src/topl/Topl.mli
@@ -7,5 +7,15 @@
 
 open! IStd
 
-val init : unit -> unit
-(** Parse properties, mentioned by [Config.topl_properties]. Does this only once. *)
+val is_active : unit -> bool
+(** Returns whether the TOPL analysis is active. *)
+
+val get_proc_attr : Typ.Procname.t -> ProcAttributes.t option
+(** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *)
+
+val get_proc_desc : Typ.Procname.t -> Procdesc.t option
+(** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *)
+
+val instrument : Tenv.t -> Procdesc.t -> unit
+(** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility
+to instrument procedures at most once. *)
diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml
index fd9f5a18d..0d236e8ec 100644
--- a/infer/src/topl/ToplAst.ml
+++ b/infer/src/topl/ToplAst.ml
@@ -7,6 +7,8 @@
 
 open! IStd
 
+type property_name = string [@@deriving compare, hash, sexp]
+
 type register_name = string
 
 (** TODO: use Const.t *)
@@ -26,8 +28,9 @@ type label =
   ; procedure_name: procedure_name_pattern
   ; arguments: value_pattern list option }
 
-type vertex = string
+type vertex = string [@@deriving compare, hash, sexp]
 
 type transition = {source: vertex; target: vertex; label: label}
 
-type t = {name: string; message: string option; prefixes: string list; transitions: transition list}
+type t =
+  {name: property_name; message: string option; prefixes: string list; transitions: transition list}
diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml
new file mode 100644
index 000000000..dd883a3cc
--- /dev/null
+++ b/infer/src/topl/ToplAutomaton.ml
@@ -0,0 +1,81 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+module Vname = struct
+  module T = struct
+    type t = ToplAst.property_name * ToplAst.vertex [@@deriving compare, hash, sexp]
+  end
+
+  include T
+  include Hashable.Make (T)
+end
+
+type vname = Vname.t
+
+type vindex = int
+
+type tindex = int
+
+type transition = {source: vindex; target: vindex; label: ToplAst.label}
+
+(** INV1: Array.length states = Array.length outgoing
+    INV2: each index of [transitions] occurs exactly once in one of [outgoing]'s lists *)
+type t =
+  { states: vname array
+  ; transitions: transition array
+  ; outgoing: tindex list array
+  ; vindex: vname -> vindex }
+
+(** [index_in H a x] is the (last) index of [x] in array [a]. *)
+let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) : k -> int =
+  let h = H.create ~size:(2 * Array.length a) () in
+  let f i x = H.set h ~key:x ~data:i in
+  Array.iteri ~f a ;
+  let find x = H.find_exn h x in
+  find
+
+
+let make properties =
+  let states : vname array =
+    let open ToplAst in
+    let f p =
+      let f {source; target; _} = [(p.name, source); (p.name, target)] in
+      List.concat_map ~f p.transitions
+    in
+    Array.of_list (List.concat_map ~f properties)
+  in
+  let vindex = index_in (module Vname.Table) states in
+  let transitions : transition array =
+    let f p =
+      let prefix_pname pname =
+        "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "()$"
+      in
+      let f t =
+        let source = vindex ToplAst.(p.name, t.source) in
+        let target = vindex ToplAst.(p.name, t.target) in
+        let procedure_name = prefix_pname ToplAst.(t.label.procedure_name) in
+        let label = {t.ToplAst.label with procedure_name} in
+        {source; target; label}
+      in
+      List.map ~f p.ToplAst.transitions
+    in
+    Array.of_list (List.concat_map ~f properties)
+  in
+  let outgoing : tindex list array =
+    let vcount = Array.length states in
+    let a = Array.create ~len:vcount [] in
+    let f i t = a.(t.source) <- i :: a.(t.source) in
+    Array.iteri ~f transitions ; a
+  in
+  {states; transitions; outgoing; vindex}
+
+
+let transition a i = a.transitions.(i)
+
+let tcount a = Array.length a.transitions
diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli
new file mode 100644
index 000000000..b73d22043
--- /dev/null
+++ b/infer/src/topl/ToplAutomaton.mli
@@ -0,0 +1,39 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(* An automaton is a different representation for a set of TOPL properties: states and transitions
+   are identified by nonnegative integers; and transitions are grouped by their source. Also, the
+   meaning of transition labels does not depend on context (e.g., prefixes are now included).
+
+   We identify states by integers because biabduction tracks integers well; for example, equality
+   checks on integers are obvious, we don't need to worry about whether we should be using an
+   equals() method.
+
+   We identify transitions by integers because, in the monitor code that we generate, we use a
+   boolean variable transitionN to tell if the static part of a transition guard is satisfied. The N
+   is just some identifier for the transition, and integers are convenient identifiers.
+
+   NOTE: Now, the signature is the minimal needed for code instrumentation, but the implementation
+   does some extra work (such as grouping transitions by their source) that will be useful for
+   code generation. (TODO: remove note once code generation is implemented.)
+*)
+
+type t
+
+type vindex = int
+
+type tindex = int (* from 0 to tcount()-1, inclusive *)
+
+type transition = {source: vindex; target: vindex; label: ToplAst.label}
+
+val make : ToplAst.t list -> t
+
+val transition : t -> tindex -> transition
+
+val tcount : t -> int
diff --git a/infer/tests/codetoanalyze/java/topl/Iterators.java b/infer/tests/codetoanalyze/java/topl/Iterators.java
new file mode 100644
index 000000000..6bb0d3888
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/Iterators.java
@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+import java.util.*;
+
+class Iterators {
+  void hasNextBad_FN(List<Integer> x) {
+    Iterator<Integer> i = x.iterator();
+    i.next();
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile
index ca917b0ff..7f8c2fd69 100644
--- a/infer/tests/codetoanalyze/java/topl/Makefile
+++ b/infer/tests/codetoanalyze/java/topl/Makefile
@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-INFER_OPTIONS = --topl-properties tomcat.topl --biabduction-only
+INFER_OPTIONS = --topl-properties tomcat.topl --topl-properties iterators.topl --biabduction-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)
diff --git a/infer/tests/codetoanalyze/java/topl/iterators.topl b/infer/tests/codetoanalyze/java/topl/iterators.topl
new file mode 100644
index 000000000..92cc32c51
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/iterators.topl
@@ -0,0 +1,29 @@
+property HasNext
+  prefix <java.util.{Collection,Iterator}>
+  start -> start: *
+  start -> invalid: I = iterator(*)
+  invalid -> valid: <true> = hasNext(i) // treat as shorthand for <B> = hasNext if (b)
+  valid -> invalid: next(i)
+  invalid -> error: next(i)
+
+property UnsafeIterator
+  prefix <java.util.{Collection,Iterator}>
+  start -> iterating: I = iterator(C)
+  iterating -> modified: remove(c, *)
+  iterating -> modified: add(c, *)
+  modified -> error: next(i)
+
+property UnsafeMapIterator
+  start -> start: *
+  start -> gotView: View = keySet(M)
+  start -> gotView: View = values(M)
+  gotView -> iterating: I = iterator(view)
+  iterating -> updated: put(m, *)
+  updated -> error: next(i)
+
+property SkipIndexAfterRemove
+  prefix <java.util.ArrayList>
+  start -> start: *
+  start -> removed: remove(Collection, Index)
+  removed -> ok:    get(collection, index)
+  removed -> error: get(collection, J) // TODO: if (j!=index)