diff --git a/verification/cbmc/proofs/Makefile.common b/verification/cbmc/proofs/Makefile.common
index e0897c04d..7658ee5b1 100644
--- a/verification/cbmc/proofs/Makefile.common
+++ b/verification/cbmc/proofs/Makefile.common
@@ -4,7 +4,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5
+CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.11
 
 ################################################################
 # The CBMC Starter Kit depends on the files Makefile.common and
@@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
 
 ifeq ($(strip $(ENABLE_POOLS)),)
   POOL =
+  INIT_POOLS =
 else ifeq ($(strip $(EXPENSIVE)),)
   POOL =
+  INIT_POOLS =
 else
   POOL = --pool expensive
+  INIT_POOLS = --pools expensive:1
 endif
 
 # Similar to the pool feature above. If Litani is new enough, enable
@@ -229,40 +232,45 @@ endif
 #
 # Each variable below controls a specific property checking flag
 # within CBMC. If desired, a property flag can be disabled within
-# a particular proof by nulling the corresponding variable. For
-# instance, the following line:
+# a particular proof by nulling the corresponding variable when CBMC's default
+# is not to perform such checks, or setting to --no-<CHECK>-check when CBMC's
+# default is to perform such checks. For instance, the following lines:
 #
-#     CHECK_FLAG_POINTER_CHECK =
+#     CBMC_FLAG_POINTER_CHECK = --no-pointer-check
+#     CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
 #
-# would disable the --pointer-check CBMC flag within:
+# would disable pointer checks and unsigned overflow checks with CBMC flag
+# within:
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
-CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
-CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable
+CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
-CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
 CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
 CBMC_FLAG_NAN_CHECK ?= --nan-check
-CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable
 CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
-CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
-CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
-CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
-CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
-CBMC_FLAG_UNWIND ?= --unwind 1
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable
+CBMC_DEFAULT_UNWIND ?= --unwind 1
 CBMC_FLAG_FLUSH ?= --flush
 
 # CBMC flags used for property checking and coverage checking
 
-CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH)
+CBMCFLAGS += $(CBMC_FLAG_FLUSH)
+
+# CBMC 6.0.0 enables all standard checks by default, which can make coverage analysis
+# very slow. See https://github.com/diffblue/cbmc/issues/8389
+# For now, we disable these checks when generating coverage info.
+COVERFLAGS ?= --no-standard-checks --malloc-may-fail --malloc-fail-null
 
 # CBMC flags used for property checking
 
-CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
-CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
@@ -274,12 +282,6 @@ CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
-CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)
-
-# CBMC flags used for coverage checking
-
-COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
-COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 
 # Additional CBMC flag to CBMC control verbosity.
 #
@@ -307,10 +309,13 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 NONDET_STATIC ?=
 
 # Flags to pass to goto-cc for compilation and linking
-COMPILE_FLAGS ?= -Wall
-LINK_FLAGS ?= -Wall
+COMPILE_FLAGS ?= -Wall -Werror
+LINK_FLAGS ?= -Wall -Werror
 EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
 
+# During instrumentation, it adds models of C library functions
+ADD_LIBRARY_FLAG := --add-library
+
 # Preprocessor include paths -I...
 INCLUDES ?=
 
@@ -349,9 +354,9 @@ UNWINDSET ?=
 # contracts).  To satisfy this requirement, it may be necessary to
 # unwind some loops before the function contract and loop invariant
 # transformations are applied to the goto program.  This variable
-# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the
-# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint.
-EARLY_UNWINDSET ?=
+# CPROVER_LIBRARY_UNWINDSET is identical to UNWINDSET, and we assume that the
+# loops mentioned in CPROVER_LIBRARY_UNWINDSET and UNWINDSET are disjoint.
+CPROVER_LIBRARY_UNWINDSET ?=
 
 # CBMC function removal (Normally set set in the proof Makefile)
 #
@@ -396,12 +401,28 @@ PROOF_SOURCES ?=
 # report, making the proof run appear to "hang".
 CBMC_TIMEOUT ?= 21600
 
+# CBMC string abstraction
+#
+# Replace all uses of char * by a struct that carries that string,
+# and also the underlying allocation and the C string length.
+STRING_ABSTRACTION ?=
+ifdef STRING_ABSTRACTION
+  ifneq ($(strip $(STRING_ABSTRACTION)),)
+    CBMC_STRING_ABSTRACTION := --string-abstraction
+  endif
+endif
+
+# Optional configuration library flags
+OPT_CONFIG_LIBRARY ?=
+CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION)
+
 # Proof writers could add function contracts in their source code.
 # These contracts are ignored by default, but may be enabled in two distinct
 # contexts using the following two variables:
 # 1. To check whether one or more function contracts are sound with respect to
 #    the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
-#    function names.
+#    function names. Use CHECK_FUNCTION_CONTRACTS_REC to check contracts on
+#    recursive functions.
 # 2. To replace calls to certain functions with their correspondent function
 #    contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
 #    One must check separately whether a function contract is sound before
@@ -409,17 +430,52 @@ CBMC_TIMEOUT ?= 21600
 CHECK_FUNCTION_CONTRACTS ?=
 CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))
 
+CHECK_FUNCTION_CONTRACTS_REC ?=
+CBMC_CHECK_FUNCTION_CONTRACTS_REC := $(patsubst %,--enforce-contract-rec %, $(CHECK_FUNCTION_CONTRACTS_REC))
+
 USE_FUNCTION_CONTRACTS ?=
 CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))
 
+CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LOOP_CONTRACTS)
+
+# Proof writers may also apply function contracts using the Dynamic Frame
+# Condition Checking (DFCC) mode. For more information on DFCC,
+# please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html.
+USE_DYNAMIC_FRAMES ?=
+ifdef USE_DYNAMIC_FRAMES
+  ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
+    CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC)
+  endif
+endif
+
 # Similarly, proof writers could also add loop contracts in their source code
 # to obtain unbounded correctness proofs. Unlike function contracts, loop
 # contracts are not reusable and thus are checked and used simultaneously.
 # These contracts are also ignored by default, but may be enabled by setting
-# the APPLY_LOOP_CONTRACTS variable to 1.
-APPLY_LOOP_CONTRACTS ?= 0
-ifeq ($(APPLY_LOOP_CONTRACTS),1)
-  CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
+# the APPLY_LOOP_CONTRACTS variable.
+APPLY_LOOP_CONTRACTS ?=
+ifdef APPLY_LOOP_CONTRACTS
+  ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
+    CBMC_APPLY_LOOP_CONTRACTS := --apply-loop-contracts
+  endif
+endif
+
+# The default unwind should only be used in DFCC mode without loop contracts.
+# When loop contracts are applied, we only unwind specified loops.
+# If any loops remain after loop contracts have been applied, CBMC might try
+# to unwind the program indefinitely, because we do not pass default unwind
+# (i.e., --unwind 1) to CBMC when in DFCC mode.
+# We must not use a default unwind command in DFCC mode, because contract instrumentation
+# introduces loops encoding write set inclusion checks that must be dynamically unwound during
+# symex.
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
+ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
+else
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
+endif
 endif
 
 # Silence makefile output (eg, long litani commands) unless VERBOSE is set.
@@ -442,7 +498,6 @@ GOTO_CC ?= goto-cc
 GOTO_INSTRUMENT ?= goto-instrument
 CRANGLER ?= crangler
 VIEWER ?= cbmc-viewer
-MAKE_SOURCE ?= make-source
 VIEWER2 ?= cbmc-viewer
 CMAKE ?= cmake
 
@@ -471,19 +526,28 @@ DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
 
 # CI currently assumes cbmc invocation has at most one --unwindset
+
+# UNWINDSET is designed for user code (i.e., proof and project code)
 ifdef UNWINDSET
-  ifneq ($(strip $(UNWINDSET)),"")
+  ifneq ($(strip $(UNWINDSET)),)
     CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
   endif
 endif
-ifdef EARLY_UNWINDSET
-  ifneq ($(strip $(EARLY_UNWINDSET)),"")
-    CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET)))
+
+# CPROVER_LIBRARY_UNWINDSET is designed for CPROVER library functions
+ifdef CPROVER_LIBRARY_UNWINDSET
+  ifneq ($(strip $(CPROVER_LIBRARY_UNWINDSET)),)
+    CBMC_CPROVER_LIBRARY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(CPROVER_LIBRARY_UNWINDSET)))
   endif
 endif
 
 CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
-CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
+
+ifdef RESTRICT_FUNCTION_POINTER
+  ifneq ($(strip $(RESTRICT_FUNCTION_POINTER)),)
+    CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
+  endif
+endif
 
 ################################################################
 # Targets for rewriting source files with crangler
@@ -567,7 +631,7 @@ $(REWRITTEN_SOURCES):
 # Build targets that make the relevant .goto files
 
 # Compile project sources
-$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
+$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -579,7 +643,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	  --description "$(PROOF_UID): building project binary"
 
 # Compile proof sources
-$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
+$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -591,7 +655,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
 	  --description "$(PROOF_UID): building proof binary"
 
 # Remove function bodies from project sources
-$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
@@ -603,7 +667,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
 	  --description "$(PROOF_UID): removing function bodies from project sources"
 
 # Link project and proof sources into the proof harness
-$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
 	$(LITANI) add-job \
 	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
 	  --inputs $^ \
@@ -614,10 +678,10 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
 	  --description "$(PROOF_UID): linking project to proof"
 
 # Restrict function pointers
-$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
+$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
@@ -626,7 +690,17 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
 	  --description "$(PROOF_UID): restricting function pointers in project sources"
 
 # Fill static variable with unconstrained values
-$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
+$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto
+ifneq ($(strip $(CODE_CONTRACTS)),)
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/nondet_static-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not setting static variables to nondet (will do during contract instrumentation)"
+else
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
@@ -636,83 +710,102 @@ $(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
 	  --description "$(PROOF_UID): setting static variables to nondet"
+endif
 
-# Omit unused functions (sharpens coverage calculations)
-$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+# Link CPROVER library if DFCC mode is on
+$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
+	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): dropping unused functions"
+	  --description "$(PROOF_UID): linking CPROVER library"
+else
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not linking CPROVER library"
+endif
 
-# Omit initialization of unused global variables (reduces problem size)
-$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code
+$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): slicing global initializations"
-
-# Replace function calls with function contracts
-# This must be done before enforcing function contracts,
-# since contract enforcement inlines all function calls.
-$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
+	  --description $(UNWIND_0500_DESC)
+else ifneq ($(strip $(CODE_CONTRACTS)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
+		'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/use_function_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): replacing function calls with function contracts"
+	  --description "$(PROOF_UID): unwinding loops in proof and project code"
+else
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not unwinding loops"
+endif
 
-# Unwind loops for loop and function contracts
-$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+# Replace function contracts, check function contracts, instrument for loop contracts
+$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
+	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): unwinding loops"
+	  --description "$(PROOF_UID): checking function contracts"
 
-# Apply loop contracts
-$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
+# Omit initialization of unused global variables (reduces problem size)
+$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): applying loop contracts"
+	  --description "$(PROOF_UID): slicing global initializations"
 
-# Check function contracts
-$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
+# Omit unused functions (sharpens coverage calculations)
+$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): checking function contracts"
+	  --description "$(PROOF_UID): dropping unused functions"
 
 # Final name for proof harness
-$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
+$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto
 	$(LITANI) add-job \
 	  --command 'cp $< $@' \
 	  --inputs $^ \
@@ -724,11 +817,19 @@ $(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
 ################################################################
 # Targets to run the analysis commands
 
-$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+ifdef CBMCFLAGS
+  ifeq ($(strip $(CODE_CONTRACTS)),)
+    CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
+  else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
+    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
+  endif
+endif
+
+$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  $(POOL) \
 	  --command \
-	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --ci-stage test \
@@ -741,11 +842,11 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/result-err-log.txt \
 	  --description "$(PROOF_UID): checking safety properties"
 
-$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  $(POOL) \
 	  --command \
-	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --ci-stage test \
@@ -788,54 +889,19 @@ $(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/coverage-err-log.txt \
 	  --description "$(PROOF_UID): calculating coverage"
 
-define VIEWER_CMD
-  $(VIEWER) \
-    --result $(LOGDIR)/result.txt \
-    --block $(LOGDIR)/coverage.xml \
-    --property $(LOGDIR)/property.xml \
-    --srcdir $(SRCDIR) \
-    --goto $(HARNESS_GOTO).goto \
-    --htmldir $(PROOFDIR)/html
-endef
-export VIEWER_CMD
-
-$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
-	$(LITANI) add-job \
-	  --command "$$VIEWER_CMD" \
-	  --inputs $^ \
-	  --outputs $(PROOFDIR)/html \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage report \
-	  --stdout-file $(LOGDIR)/viewer-log.txt \
-	  --description "$(PROOF_UID): generating report"
-
+COVERAGE ?= $(LOGDIR)/coverage.xml
+VIEWER_COVERAGE_FLAG ?= --coverage $(COVERAGE)
 
-# Caution: run make-source before running property and coverage checking
-# The current make-source script removes the goto binary
-$(LOGDIR)/source.json:
-	mkdir -p $(dir $@)
-	$(RM) -r $(GOTODIR)
-	$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
-	$(RM) -r $(GOTODIR)
-
-define VIEWER2_CMD
-  $(VIEWER2) \
-    --result $(LOGDIR)/result.xml \
-    --coverage $(LOGDIR)/coverage.xml \
-    --property $(LOGDIR)/property.xml \
-    --srcdir $(SRCDIR) \
-    --goto $(HARNESS_GOTO).goto \
-    --reportdir $(PROOFDIR)/report \
-    --config $(PROOFDIR)/cbmc-viewer.json
-endef
-export VIEWER2_CMD
-
-# Omit logs/source.json from report generation until make-sources
-# works correctly with Makefiles that invoke the compiler with
-# mutliple source files at once.
-$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(COVERAGE)
 	$(LITANI) add-job \
-	  --command "$$VIEWER2_CMD" \
+	  --command " $(VIEWER) \
+	    --result $(LOGDIR)/result.xml \
+	    $(VIEWER_COVERAGE_FLAG) \
+	    --property $(LOGDIR)/property.xml \
+	    --srcdir $(SRCDIR) \
+	    --goto $(HARNESS_GOTO).goto \
+	    --reportdir $(PROOFDIR)/report \
+	    --config $(PROOFDIR)/cbmc-viewer.json" \
 	  --inputs $^ \
 	  --outputs $(PROOFDIR)/report \
 	  --pipeline-name "$(PROOF_UID)" \
@@ -858,7 +924,7 @@ litani-path:
 _goto: $(HARNESS_GOTO).goto
 goto:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _goto
 	@ echo Running 'litani build'
@@ -867,7 +933,7 @@ goto:
 _result: $(LOGDIR)/result.txt
 result:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _result
 	@ echo Running 'litani build'
@@ -876,7 +942,7 @@ result:
 _property: $(LOGDIR)/property.xml
 property:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _property
 	@ echo Running 'litani build'
@@ -885,30 +951,26 @@ property:
 _coverage: $(LOGDIR)/coverage.xml
 coverage:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _coverage
 	@ echo Running 'litani build'
 	$(LITANI) run-build
 
-# Choose the invocation of cbmc-viewer depending on which version of
-# cbmc-viewer is installed.  The --version flag is not implemented in
-# version 1 --- it is an "unrecognized argument" --- but it is
-# implemented in version 2.
-_report1: $(PROOFDIR)/html
-_report2: $(PROOFDIR)/report
-_report:
-	(cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \
-		$(MAKE) -B _report1 || $(MAKE) -B _report2
-
-report report1 report2:
+_report: $(PROOFDIR)/report
+report:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _report
 	@ echo Running 'litani build'
 	$(LITANI) run-build
 
+_report_no_coverage:
+	$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG="" _report
+report-no-coverage:
+	$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG=" " report
+
 ################################################################
 # Targets to clean up after ourselves
 clean:
@@ -918,7 +980,7 @@ clean:
 	-$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json)
 
 veryclean: clean
-	-$(RM) -r html report
+	-$(RM) -r report
 	-$(RM) -r $(LOGDIR) $(GOTODIR)
 
 .PHONY: \
@@ -926,15 +988,14 @@ veryclean: clean
   _goto \
   _property \
   _report \
-  _report2 \
-  _result \
+  _report_no_coverage \
   clean \
   coverage \
   goto \
   litani-path \
   property \
   report \
-  report2 \
+  report-no-coverage \
   result \
   setup_dependencies \
   testdeps \
@@ -943,38 +1004,6 @@ veryclean: clean
 
 ################################################################
 
-# Rule for generating cbmc-batch.yaml, used by the CI at
-# https://github.com/awslabs/aws-batch-cbmc/
-
-JOB_OS ?= ubuntu16
-JOB_MEMORY ?= 32000
-
-# Proofs that are expected to fail should set EXPECTED to
-# "FAILED" in their Makefile. Values other than SUCCESSFUL
-# or FAILED will cause a CI error.
-EXPECTED ?= SUCCESSFUL
-
-define yaml_encode_options
-	"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
-endef
-
-CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)
-
-cbmc-batch.yaml:
-	@$(RM) $@
-	@echo 'build_memory: $(JOB_MEMORY)' > $@
-	@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
-	@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
-	@echo 'expected: $(EXPECTED)' >> $@
-	@echo 'goto: $(HARNESS_GOTO).goto' >> $@
-	@echo 'jobos: $(JOB_OS)' >> $@
-	@echo 'property_memory: $(JOB_MEMORY)' >> $@
-	@echo 'report_memory: $(JOB_MEMORY)' >> $@
-
-.PHONY: cbmc-batch.yaml
-
-################################################################
-
 # Run "make echo-proof-uid" to print the proof ID of a proof. This can be
 # used by scripts to ensure that every proof has an ID, that there are
 # no duplicates, etc.