diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index d1c4ce05468..2c83f8bc1c9 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -68,12 +68,12 @@ class ai_baset
   }
 
   /// Run abstract interpretation on a whole program
-  void operator()(const goto_modelt &goto_model)
+  void operator()(const abstract_goto_modelt &goto_model)
   {
-    const namespacet ns(goto_model.symbol_table);
-    initialize(goto_model.goto_functions);
-    entry_state(goto_model.goto_functions);
-    fixedpoint(goto_model.goto_functions, ns);
+    const namespacet ns(goto_model.get_symbol_table());
+    initialize(goto_model.get_goto_functions());
+    entry_state(goto_model.get_goto_functions());
+    fixedpoint(goto_model.get_goto_functions(), ns);
     finalize();
   }
 
@@ -374,7 +374,7 @@ class ai_baset
 ///    \ref ai_baset#operator()(const irep_idt&,const goto_programt&, <!--
 ///    --> const namespacet&),
 ///    \ref ai_baset#operator()(const goto_functionst&,const namespacet&)
-///    and \ref ai_baset#operator()(const goto_modelt&)
+///    and \ref ai_baset#operator()(const abstract_goto_modelt&)
 /// 2. Accessing the results of an analysis, by looking up the result
 ///    for a given location \p l using
 ///    \ref ait#operator[](goto_programt::const_targett).
diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt
index 0ad6aadc0de..3ea42354c2a 100644
--- a/src/goto-analyzer/CMakeLists.txt
+++ b/src/goto-analyzer/CMakeLists.txt
@@ -12,6 +12,7 @@ target_link_libraries(goto-analyzer-lib
     cpp
     linking
     big-int
+    goto-checker
     goto-programs
     analyses
     pointer-analysis
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index ad955380c48..a41692727bc 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -13,6 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../pointer-analysis/pointer-analysis$(LIBEXT) \
diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt
index 72778a5e8df..df25ebdf0ed 100644
--- a/src/goto-analyzer/module_dependencies.txt
+++ b/src/goto-analyzer/module_dependencies.txt
@@ -3,6 +3,7 @@ analyses
 assembler
 cpp
 goto-analyzer
+goto-checker
 goto-programs
 java_bytecode # will go away
 langapi # should go away
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
index 2dcaa2a40d5..0d78d556746 100644
--- a/src/goto-analyzer/static_verifier.cpp
+++ b/src/goto-analyzer/static_verifier.cpp
@@ -27,6 +27,49 @@ struct static_verifier_resultt
   irep_idt function_id;
 };
 
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties)
+{
+  const namespacet ns{abstract_goto_model.get_symbol_table()};
+  // this is mutable because we want to change the property status
+  // in this loop
+  for(auto &property : properties)
+  {
+    auto &property_status = property.second.status;
+    const goto_programt::const_targett &property_location = property.second.pc;
+    exprt condition = property_location->get_condition();
+    const std::unique_ptr<ai_baset::statet> predecessor_state_copy =
+      ai.abstract_state_before(property_location);
+    // simplify the condition given the domain information we have
+    // about the state right before the assertion is evaluated
+    predecessor_state_copy->ai_simplify(condition, ns);
+    // if the condition simplifies to true the assertion always succeeds
+    if(condition.is_true())
+    {
+      property_status = property_statust::PASS;
+    }
+    // if the condition simplifies to false the assertion always fails
+    else if(condition.is_false())
+    {
+      property_status = property_statust::FAIL;
+    }
+    // if the domain state is bottom then the assertion is definitely
+    // unreachable
+    else if(predecessor_state_copy->is_bottom())
+    {
+      property_status = property_statust::NOT_REACHABLE;
+    }
+    // if the condition isn't definitely true, false or unreachable
+    // we don't know whether or not it may fail
+    else
+    {
+      property_status = property_statust::UNKNOWN;
+    }
+  }
+}
+
 /// Makes a status message string from a status.
 static const char *message(const static_verifier_resultt::statust &status)
 {
diff --git a/src/goto-analyzer/static_verifier.h b/src/goto-analyzer/static_verifier.h
index 87358a30958..910466fd585 100644
--- a/src/goto-analyzer/static_verifier.h
+++ b/src/goto-analyzer/static_verifier.h
@@ -9,8 +9,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 #define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 
+#include <goto-checker/properties.h>
 #include <iosfwd>
 
+class abstract_goto_modelt;
 class ai_baset;
 class goto_modelt;
 class message_handlert;
@@ -23,4 +25,15 @@ bool static_verifier(
   message_handlert &,
   std::ostream &);
 
+/// Use the information from the abstract interpreter to fill out the statuses
+/// of the passed properties
+/// \param abstract_goto_model The goto program to verify
+/// \param ai The abstract interpreter (should be run to fixpoint
+///           before calling this function)
+/// \param properties The properties to fill out
+void static_verifier(
+  const abstract_goto_modelt &abstract_goto_model,
+  const ai_baset &ai,
+  propertiest &properties);
+
 #endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H