diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6b2d120cf6..aa6117fe69 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,10 +1,19 @@
 cmake_minimum_required(VERSION 3.2)
 
-include(GNUInstallDirs)
-
 set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
 
+include(GNUInstallDirs)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
 add_subdirectory(src)
 
-enable_testing()
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
 add_subdirectory(unit)
+add_subdirectory(regression)
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
new file mode 100644
index 0000000000..245e861124
--- /dev/null
+++ b/regression/CMakeLists.txt
@@ -0,0 +1,36 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile}"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests name cmdline)
+    add_test_pl_profile("${name}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
+endmacro(add_test_pl_tests)
+
+add_subdirectory(ansi-c)
+add_subdirectory(cbmc)
+add_subdirectory(cbmc-java)
+add_subdirectory(cbmc-java-inheritance)
+add_subdirectory(cpp)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
+add_subdirectory(goto-instrument)
+add_subdirectory(goto-instrument-typedef)
+add_subdirectory(invariants)
+add_subdirectory(strings)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(test-script)
diff --git a/regression/ansi-c/CMakeLists.txt b/regression/ansi-c/CMakeLists.txt
new file mode 100644
index 0000000000..027ec188f7
--- /dev/null
+++ b/regression/ansi-c/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "ansi-c"
+    "$<TARGET_FILE:goto-cc>"
+)
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
index 87af55e330..c770b3b3ed 100644
--- a/regression/ansi-c/Makefile
+++ b/regression/ansi-c/Makefile
@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
diff --git a/regression/cbmc-java-inheritance/CMakeLists.txt b/regression/cbmc-java-inheritance/CMakeLists.txt
new file mode 100644
index 0000000000..cf949e080b
--- /dev/null
+++ b/regression/cbmc-java-inheritance/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java-inheritance"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc-java/CMakeLists.txt b/regression/cbmc-java/CMakeLists.txt
new file mode 100644
index 0000000000..37252add85
--- /dev/null
+++ b/regression/cbmc-java/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
new file mode 100644
index 0000000000..ee9f8f2e90
--- /dev/null
+++ b/regression/cbmc/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt
new file mode 100644
index 0000000000..c6eea89555
--- /dev/null
+++ b/regression/cpp/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cpp"
+    "$<TARGET_FILE:goto-cc>"
+)
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
index 87af55e330..c770b3b3ed 100644
--- a/regression/cpp/Makefile
+++ b/regression/cpp/Makefile
@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
diff --git a/regression/goto-analyzer/CMakeLists.txt b/regression/goto-analyzer/CMakeLists.txt
new file mode 100644
index 0000000000..3d5daac5b9
--- /dev/null
+++ b/regression/goto-analyzer/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-analyzer"
+    "$<TARGET_FILE:goto-analyzer>"
+)
diff --git a/regression/goto-diff/CMakeLists.txt b/regression/goto-diff/CMakeLists.txt
new file mode 100644
index 0000000000..9f0957a138
--- /dev/null
+++ b/regression/goto-diff/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-diff"
+    "$<TARGET_FILE:goto-diff>"
+)
diff --git a/regression/goto-instrument-typedef/CMakeLists.txt b/regression/goto-instrument-typedef/CMakeLists.txt
new file mode 100644
index 0000000000..63a842ccec
--- /dev/null
+++ b/regression/goto-instrument-typedef/CMakeLists.txt
@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument-typedef"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)
diff --git a/regression/goto-instrument-typedef/Makefile b/regression/goto-instrument-typedef/Makefile
index 08fe97ae88..56de781ae2 100644
--- a/regression/goto-instrument-typedef/Makefile
+++ b/regression/goto-instrument-typedef/Makefile
@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
diff --git a/regression/goto-instrument-typedef/chain.sh b/regression/goto-instrument-typedef/chain.sh
index 9cef4ffdfa..d53833cccd 100755
--- a/regression/goto-instrument-typedef/chain.sh
+++ b/regression/goto-instrument-typedef/chain.sh
@@ -1,14 +1,21 @@
 #!/bin/bash
 
-SRC=../../../src
+GC=$1
+GI=$2
+is_windows=$3
 
-GC=$SRC/goto-cc/goto-cc
-GI=$SRC/goto-instrument/goto-instrument
+name=${*:$#}
+name=${name%.c}
 
-OPTS=$1
-NAME=${2%.c}
+args=${*:4:$#-4}
 
-rm $NAME.gb
-$GC $NAME.c --function fun -o $NAME.gb
-echo $GI $OPTS $NAME.gb
-$GI $OPTS $NAME.gb
+rm "${name}.gb"
+if [[ "${is_windows}" == "true" ]]; then
+  "$GC" "${name}.c" --function fun
+  mv "${name}.exe" "${name}.gb"
+else
+  "$GC" "${name}.c" --function fun -o "${name}.gb"
+fi
+
+echo "$GI" ${args} "${name}.gb"
+"$GI" ${args} "${name}.gb"
diff --git a/regression/goto-instrument/CMakeLists.txt b/regression/goto-instrument/CMakeLists.txt
new file mode 100644
index 0000000000..088fcab965
--- /dev/null
+++ b/regression/goto-instrument/CMakeLists.txt
@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)
diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile
index 94605814b4..a8d5437028 100644
--- a/regression/goto-instrument/Makefile
+++ b/regression/goto-instrument/Makefile
@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index 68f50b095b..2656ea4488 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -2,26 +2,37 @@
 
 set -e
 
-src=../../../src
-goto_cc=$src/goto-cc/goto-cc
-goto_instrument=$src/goto-instrument/goto-instrument
-cbmc=$src/cbmc/cbmc
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
 
-name=${@:$#}
+name=${*:$#}
 name=${name%.c}
 
-args=${@:1:$#-1}
+args=${*:5:$#-5}
 
-$goto_cc -o $name.gb $name.c
-# $goto_instrument --show-goto-functions $name.gb
-$goto_instrument $args $name.gb ${name}-mod.gb
-if [ ! -e ${name}-mod.gb ] ; then
-  cp $name.gb ${name}-mod.gb
-elif echo "$args" | grep -q -- "--dump-c" ; then
-  mv ${name}-mod.gb ${name}-mod.c
-  $goto_cc ${name}-mod.c -o ${name}-mod.gb
-  rm ${name}-mod.c
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
 fi
-$goto_instrument --show-goto-functions ${name}-mod.gb
-$cbmc ${name}-mod.gb
 
+$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"
diff --git a/regression/invariants/CMakeLists.txt b/regression/invariants/CMakeLists.txt
new file mode 100644
index 0000000000..467e2b1395
--- /dev/null
+++ b/regression/invariants/CMakeLists.txt
@@ -0,0 +1,7 @@
+add_executable(driver driver.cpp)
+target_link_libraries(driver big-int util)
+
+add_test_pl_tests(
+    "invariants"
+    "$<TARGET_FILE:driver>"
+)
diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt
new file mode 100644
index 0000000000..6e8a19a979
--- /dev/null
+++ b/regression/strings-smoke-tests/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "strings-smoke-test"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/strings/CMakeLists.txt b/regression/strings/CMakeLists.txt
new file mode 100644
index 0000000000..846e65ae00
--- /dev/null
+++ b/regression/strings/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "strings"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/test-script/CMakeLists.txt b/regression/test-script/CMakeLists.txt
new file mode 100644
index 0000000000..00ad3a848d
--- /dev/null
+++ b/regression/test-script/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "test-script"
+    "${CMAKE_CURRENT_SOURCE_DIR}/program_runner.sh" 
+)
diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt
index 0f3fd34519..9556873965 100644
--- a/src/ansi-c/CMakeLists.txt
+++ b/src/ansi-c/CMakeLists.txt
@@ -20,6 +20,31 @@ function(make_inc name)
     )
 endfunction(make_inc)
 
+################################################################################
+
+if(MINGW)
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/err.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+else()
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+endif()
+
+file(GLOB library_check_sources "library/*.c")
+list(REMOVE_ITEM library_check_sources ${platform_unavail})
+
+add_custom_target(library_check
+    ${CMAKE_CURRENT_SOURCE_DIR}/check_library.sh ${library_check_sources}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+################################################################################
+
 make_inc(arm_builtin_headers)
 make_inc(clang_builtin_headers)
 make_inc(cw_builtin_headers)
diff --git a/src/ansi-c/check_library.sh b/src/ansi-c/check_library.sh
new file mode 100755
index 0000000000..c02d0c95bf
--- /dev/null
+++ b/src/ansi-c/check_library.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+for var in "$@"; do
+    cp "${var}" __libcheck.c
+    sed -i 's/__builtin_[^v]/s&/' __libcheck.c
+    sed -i 's/__sync_/s&/' __libcheck.c
+    sed -i 's/__noop/s&/' __libcheck.c
+    cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label -Wno-uninitialized
+
+    ec="$?"
+    rm __libcheck.s __libcheck.i __libcheck.c
+    [ "${ec}" -eq 0 ] || exit "${ec}"
+done
diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt
index ad2b50f775..6aa01b6139 100644
--- a/src/goto-cc/CMakeLists.txt
+++ b/src/goto-cc/CMakeLists.txt
@@ -35,3 +35,7 @@ add_if_library(goto-cc-lib jsil)
 # Executable
 add_executable(goto-cc goto_cc_main.cpp)
 target_link_libraries(goto-cc goto-cc-lib)
+
+if(WIN32)
+  set_target_properties(goto-cc PROPERTIES OUTPUT_NAME goto-cl)
+endif()
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 69d0f7b14b..623e57ecb5 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -31,7 +31,12 @@ target_include_directories(unit
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
 target_link_libraries(unit ansi-c solvers java_bytecode)
-add_test(NAME unit COMMAND unit WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
+add_test(
+    NAME unit
+    COMMAND $<TARGET_FILE:unit>
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+set_tests_properties(unit PROPERTIES LABELS CORE)
 
 add_executable(miniBDD miniBDD.cpp)
 target_include_directories(miniBDD
@@ -41,7 +46,8 @@ target_include_directories(miniBDD
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
 target_link_libraries(miniBDD solvers ansi-c)
-add_test(miniBDD miniBDD)
+add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
+set_tests_properties(miniBDD PROPERTIES LABELS CORE)
 
 add_executable(string_utils string_utils.cpp)
 target_include_directories(string_utils
@@ -51,7 +57,8 @@ target_include_directories(string_utils
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
 target_link_libraries(string_utils solvers ansi-c)
-add_test(string_utils string_utils)
+add_test(NAME string_utils COMMAND $<TARGET_FILE:string_utils>)
+set_tests_properties(string_utils PROPERTIES LABELS CORE)
 
 add_executable(sharing_node sharing_node.cpp)
 target_include_directories(sharing_node
@@ -60,6 +67,6 @@ target_include_directories(sharing_node
     ${CBMC_SOURCE_DIR}
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
-add_test(sharing_node sharing_node)
-
-install(TARGETS unit miniBDD string_utils sharing_node DESTINATION bin)
+target_link_libraries(sharing_node util)
+add_test(NAME sharing_node COMMAND $<TARGET_FILE:sharing_node>)
+set_tests_properties(sharing_node PROPERTIES LABELS CORE)