diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
deleted file mode 100644
index adfae72..0000000
--- a/.github/workflows/release.yml
+++ /dev/null
@@ -1,19 +0,0 @@
-on:
-  push:
-    types: [created]
-name: Handle Push
-jobs:
-  generate:
-    name: Create nigtly artifacts
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout the repository
-        uses: actions/checkout@master
-      - name: Generate the artifacts
-        uses: skx/github-action-build@master
-      - name: Upload the artifacts
-        uses: skx/github-action-publish-binaries@master
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        with:
-          args: 'example-*'
diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
index 1165887..314257b 100644
--- a/.github/workflows/scala.yml
+++ b/.github/workflows/scala.yml
@@ -1,4 +1,4 @@
-name: Scala CI
+name: Check, Build, Test, Publish Nightly
 
 on:
   push:
@@ -6,7 +6,7 @@ on:
 
 jobs:
   check-headers:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-16.04
     steps:
       - name: Checkout ViperServer repo
         uses: actions/checkout@v2
@@ -17,54 +17,88 @@ jobs:
           config: ./.github/license-check/config.json
           strict: true
 
-  build:
-    runs-on: ubuntu-latest
+  test:
+    runs-on: ubuntu-16.04
     steps:
-    - name: Checkout ViperServer
-      uses: actions/checkout@v2
-      with:
-        path: viperServer
-    - name: Checkout Silver
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/silver
-        path: silver
-    - name: Checkout Silicon
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/silicon
-        path: silicon
-    - name: Checkout Carbon
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/carbon
-        path: carbon
-    
-    - name: Symbolically link Silver to Carbon
-      run: cd carbon; ln --symbolic ../silver
-    - name: Symbolically link Silver to Silicon
-      run: cd silicon; ln --symbolic ../silver
-    - name: Symbolically link Silver to ViperServer
-      run: cd viperServer; ln --symbolic ../silver
-    - name: Symbolically link Carbon to ViperServer
-      run: cd viperServer; ln --symbolic ../carbon
-    - name: Symbolically link Silicon to ViperServer
-      run: cd viperServer; ln --symbolic ../silicon
-    
-    - name: Install Z3
-      run: sudo apt-get update -y; sudo apt-get install -y z3
+      - name: Get Current Date
+        id: date
+        run: echo "::set-output name=DATE::$(date +'%Y-%m-%d')"
+
+      - name: Checkout ViperServer
+        uses: actions/checkout@v2
+        with:
+          path: viperServer
+      - name: Checkout Silver
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/silver
+          path: silver
+      - name: Checkout Silicon
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/silicon
+          path: silicon
+      - name: Checkout Carbon
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/carbon
+          path: carbon
     
-    - name: Set up JDK 1.8
-      uses: actions/setup-java@v1
-      with:
-        java-version: 1.11
+      - name: Symbolically link Silver to Carbon
+        run: cd carbon; ln --symbolic ../silver
+      - name: Symbolically link Silver to Silicon
+        run: cd silicon; ln --symbolic ../silver
+      - name: Symbolically link Silver to ViperServer
+        run: cd viperServer; ln --symbolic ../silver
+      - name: Symbolically link Carbon to ViperServer
+        run: cd viperServer; ln --symbolic ../carbon
+      - name: Symbolically link Silicon to ViperServer
+        run: cd viperServer; ln --symbolic ../silicon
+
+      - name: Install Z3
+        env: 
+          Z3_VERSION: 4.8.9
+          Z3_PLATFORM: x64
+          Z3_OS: ubuntu-16.04
+        run: |
+          export Z3=z3-$Z3_VERSION-$Z3_PLATFORM-$Z3_OS; 
+          curl -J -L https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/$Z3.zip > z3.zip; 
+          unzip z3.zip; 
+          sudo ln -s $(pwd)/$Z3/bin/z3 /usr/bin/z3
 
-    - name: Install SBT
-      run: echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list; curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo apt-key add; sudo apt-get update; sudo apt-get install sbt
+      - name: Set up JDK 15
+        uses: actions/setup-java@v1
+        with:
+          java-version: '15.0.1'
+          architecture: x64
+
+      - name: Install SBT
+        run: |
+          echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list; 
+          curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo apt-key add; 
+          sudo apt-get update; sudo apt-get install sbt
+    
+      - name: test project
+        run: |
+          cd viperServer; 
+          export Z3_EXE="/usr/bin/z3"; 
+          env > print_dir.txt; 
+          sbt test
 
-    - name: Assemble project
-      run: cd viperServer; sbt assembly
-        
-    - name: test project
-      run: cd viperServer; export Z3_EXE="/usr/bin/z3"; env > print_dir.txt; sbt test
+      - name: Assemble the fat JAR file
+        run: |
+          cd viperServer; 
+          sbt assembly
       
+      - name: Publish Nightly Artifact
+        env:
+          FILE: viperServer/target/scala-2.13/viper.jar
+          NIGHTLY_RELEASE_ID: 36021300
+          ARTIFACT_NAME: viper-nightly-${{ steps.date.outputs.DATE }}.jar
+        run: |
+          echo Publishing $FILE as $ARTIFACT_NAME ...;
+          curl -H "Accept: application/vnd.github.v3+json" \
+               -H "Content-Type: $(file -b --mime-type $FILE)" \
+               -H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}" \
+               --data-binary @$FILE \
+               "https://uploads.github.com/repos/${{ github.repository }}/releases/$NIGHTLY_RELEASE_ID/assets?name=$ARTIFACT_NAME"
diff --git a/README.md b/README.md
index cfd143d..31af071 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,7 @@
 
 This is ViperServer, an HTTP server that manages verification requests to different tools from the Viper tool stack.
 
-The main two tools currently are:
+The main two Viper tools (a.k.a verification backends) currently are: 
 
 - [Carbon](https://bitbucket.org/viperproject/carbon), a verification condition generation (VCG) backend for the Viper language.
 - [Silicon](https://bitbucket.org/viperproject/silicon), a symbolic execution verification backend.
@@ -14,13 +14,16 @@ The main two tools currently are:
 
 1. Viper IDE: integration of Viper into Visual Studio Code (VS Code). Viper IDE provides the best user experience for Viper.
    More details here: http://viper.ethz.ch/downloads/
-2. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g.,
+1. Facilitate the development of verification IDEs for Viper frontends, such as: 
+    - [Gobra](https://github.com/viperproject/gobra), the Viper-based verifier for the Go language
+    - [Prusti](https://github.com/viperproject/prusti-dev/), the Viper-based verifier for the Rust language
+1. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g.,
    [Nailgun](https://github.com/facebook/nailgun).
-3. Develop Viper encodings more efficiently with caching.
-4. Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is
+1. Develop Viper encodings more efficiently with caching.
+1. Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is
    available via [viper_client](https://bitbucket.org/viperproject/viper_client).
 
-For more details, please visit: http://viper.ethz.ch/downloads/
+For more details about using Viper, please visit: http://viper.ethz.ch/downloads/
 
 
 ### Installation Instructions ###
diff --git a/build.sbt b/build.sbt
index 208b153..dca31a3 100644
--- a/build.sbt
+++ b/build.sbt
@@ -9,11 +9,15 @@ lazy val silver = project in file("silver")
 lazy val silicon = project in file("silicon")
 lazy val carbon = project in file("carbon")
 
+lazy val common = (project in file("common"))
+
 // Viper Server specific project settings
 lazy val server = (project in file("."))
     .dependsOn(silver % "compile->compile;test->test")
     .dependsOn(silicon % "compile->compile;test->test")
     .dependsOn(carbon % "compile->compile;test->test")
+    .dependsOn(common)
+    .aggregate(common)
     .enablePlugins(JavaAppPackaging)
     .settings(
         // General settings
@@ -31,11 +35,12 @@ lazy val server = (project in file("."))
         libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.6.10",
         libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test,
         libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test,
+        libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.8.1", // Java implementation of language server protocol
 
         // Run settings
         run / javaOptions += "-Xss128m",
 
-        // Test settings.
+        // Test settings
         Test / parallelExecution := false,
 
         // Assembly settings
diff --git a/project/plugins.sbt b/project/plugins.sbt
index 3938178..d60a712 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -2,5 +2,5 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.15.0")
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.10.0")
 addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.7.6")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.10.0")
diff --git a/src/main/scala/viper/server/LanguageServerRunner.scala b/src/main/scala/viper/server/LanguageServerRunner.scala
new file mode 100644
index 0000000..4bff53e
--- /dev/null
+++ b/src/main/scala/viper/server/LanguageServerRunner.scala
@@ -0,0 +1,50 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+import java.io.IOException
+import java.net.Socket
+
+import org.eclipse.lsp4j.jsonrpc.Launcher
+import viper.server.ViperConfig
+import viper.server.frontends.lsp.{Coordinator, CustomReceiver, IdeLanguageClient}
+
+
+object LanguageServerRunner {
+
+  private var _config: ViperConfig = _
+
+  def main(args: Array[String]): Unit = {
+    _config = new ViperConfig(args)
+    _config.verify()
+    val port = _config.port.getOrElse(0)
+    runServer(port)
+  }
+
+  def runServer(port: Int): Unit = {
+    // start listening on port
+    try {
+      val socket = new Socket("localhost", port)
+      val localAddress = socket.getLocalAddress.getHostAddress
+
+      Coordinator.port = socket.getPort
+      Coordinator.url = localAddress
+
+      println(s"preparing to listen on ${Coordinator.url}:${Coordinator.port}")
+
+      val server: CustomReceiver = new CustomReceiver()
+      val launcher = Launcher.createLauncher(server, classOf[IdeLanguageClient], socket.getInputStream, socket.getOutputStream)
+      server.connect(launcher.getRemoteProxy)
+
+      // start listening on input stream in a new thread:
+      val fut = launcher.startListening()
+      // wait until stream is closed again
+      fut.get()
+    } catch {
+      case e: IOException => println(s"IOException occurred: ${e.toString}")
+    }
+  }
+}
+
diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala
index 676b6e5..6271fdc 100644
--- a/src/main/scala/viper/server/ViperConfig.scala
+++ b/src/main/scala/viper/server/ViperConfig.scala
@@ -9,8 +9,8 @@ package viper.server
 import java.io.File
 
 import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter}
+import viper.server.utility.Helpers.{canonizedFile, validatePath}
 import viper.server.utility.ibm
-import viper.server.utility.ibm.Socket
 
 class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
@@ -31,24 +31,12 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
       val temp: File = java.io.File.createTempFile("viperserver_journal_" + System.currentTimeMillis(), ".log")
       Some(temp.getAbsolutePath)
     },
-    validate = (path: String) => {
-      val f = canonizedLogFile(path)
-      (f.isFile || f.isDirectory) && f.canWrite || f.getParentFile.canWrite
-    },
+    validate = validatePath,
     noshort = true,
     hidden = false)
 
-  private def canonizedLogFile(some_file_path: String): File = {
-    val f = new File(some_file_path)
-    if (f.isAbsolute) {
-      f
-    } else {
-      java.nio.file.Paths.get(System.getProperty("user.dir"), some_file_path).toFile
-    }
-  }
-
   def getLogFileWithGuarantee: String = {
-    val cf: File = canonizedLogFile(logFile())
+    val cf: File = canonizedFile(logFile())
     if ( cf.isDirectory ) {
       val log: File = java.io.File.createTempFile("viperserver_journal_" + System.currentTimeMillis(), ".log", cf)
       log.toString
@@ -66,9 +54,8 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
   val port: ScallopOption[Int] = opt[Int]("port", 'p',
     descr = ("Specifies the port on which ViperServer will be started."
-      + s"The port must be an integer in range [${Socket.MIN_PORT_NUMBER}-${ibm.Socket.MAX_PORT_NUMBER}]"
+      + s"The port must be an integer in range [${ibm.Socket.MIN_PORT_NUMBER}-${ibm.Socket.MAX_PORT_NUMBER}]"
       + "If the option is omitted, an available port will be selected automatically."),
-    default = Some(ibm.Socket.findFreePort),
     validate = p => try {
       ibm.Socket.available(p)
     } catch {
diff --git a/src/main/scala/viper/server/ViperServer.scala b/src/main/scala/viper/server/ViperServerRunner.scala
similarity index 75%
rename from src/main/scala/viper/server/ViperServer.scala
rename to src/main/scala/viper/server/ViperServerRunner.scala
index 7f26776..9a284e5 100644
--- a/src/main/scala/viper/server/ViperServer.scala
+++ b/src/main/scala/viper/server/ViperServerRunner.scala
@@ -1,26 +1,24 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2020 ETH Zurich.
-
-package viper.server
-
-import viper.server.frontends.http.ViperHttpServer
-
-object ViperServerRunner {
-
-  var viperServerHTTP: ViperHttpServer = _
-
-  /** Start VCS in HTTP mode.
-    * */
-  def startHttpServer(args: Array[String]): Unit = {
-
-    viperServerHTTP = new ViperHttpServer(args)
-    viperServerHTTP.start()
-  }
-
-  def main(args: Array[String]): Unit = {
-    startHttpServer(args)
-  } // method main
-}
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server
+
+import viper.server.frontends.http.ViperHttpServer
+
+object ViperServerRunner {
+  var viperServerHttp: ViperHttpServer = _
+
+  /** Start VCS in HTTP mode.
+    * */
+  def startHttpServer(args: Array[String]): Unit = {
+    viperServerHttp = new ViperHttpServer(args)
+    viperServerHttp.start()
+  }
+
+  def main(args: Array[String]): Unit = {
+    startHttpServer(args)
+  }
+}
diff --git a/src/main/scala/viper/server/core/AstWorker.scala b/src/main/scala/viper/server/core/AstWorker.scala
new file mode 100644
index 0000000..7f8f942
--- /dev/null
+++ b/src/main/scala/viper/server/core/AstWorker.scala
@@ -0,0 +1,81 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.core
+
+import ch.qos.logback.classic.Logger
+import viper.server.utility.AstGenerator
+import viper.server.vsi.AstConstructionException
+import viper.silver.ast.Program
+import viper.silver.reporter.ExceptionReport
+
+
+object ViperFileNotFoundException extends AstConstructionException
+object AstConstructionInterrupted extends AstConstructionException
+object InvalidArgumentsException extends AstConstructionException
+object AstConstructionFailureException extends AstConstructionException
+object OutOfResourcesException extends AstConstructionException
+
+case class ServerCrashException(e: Throwable) extends Exception(e)
+
+
+import scala.concurrent.{ExecutionContext, Future, Promise}
+
+class AstWorker(val arg_list: List[String],
+                val logger: Logger)(implicit val ec: ExecutionContext) extends MessageReportingTask {
+
+  private val _artifact_pro: Promise[Program] = Promise()
+  override def artifact: Option[Future[Program]] = Some(_artifact_pro.future)
+
+  private def constructAst(): Future[Program] = Future {
+
+    //println(">>> AstWorker.constructAst()")
+
+    val file: String = arg_list.last
+
+    val reporter = new ActorReporter("AstGenerationReporter")
+    val astGen = new AstGenerator(logger, reporter)
+
+    val ast_option: Option[Program] = try {
+      astGen.generateViperAst(file)
+    } catch {
+      case _: java.nio.file.NoSuchFileException =>
+        println("The file for which verification has been requested was not found.")
+        registerTaskEnd(false)
+        throw ViperFileNotFoundException
+      case e: InterruptedException =>
+        logger.info(s"AstWorker has been interrupted: $e")
+        registerTaskEnd(false)
+        throw AstConstructionInterrupted
+      case e: java.nio.channels.ClosedByInterruptException =>
+        logger.info(s"AstWorker has been interrupted: $e")
+        registerTaskEnd(false)
+        throw AstConstructionInterrupted
+      case e: Throwable =>
+        reporter report ExceptionReport(e)
+        logger.trace(s"Creation/Execution of an AstGenerator instance resulted in an exception.", e)
+        registerTaskEnd(false)
+        throw ServerCrashException(e)
+    }
+
+    ast_option match {
+      case Some(ast) =>
+        registerTaskEnd(true)
+        ast
+      case None =>
+        logger.info("The file for which verification has been requested contained syntax errors, type errors, " +
+          "or is simply inconsistent.")
+        registerTaskEnd(false)
+        throw AstConstructionFailureException
+    }
+  }
+
+  override def run(): Unit = {
+    //println(">>> AstWorker.run()")
+    _artifact_pro.completeWith(constructAst())
+  }
+
+}
diff --git a/src/main/scala/viper/server/core/MessageReportingTask.scala b/src/main/scala/viper/server/core/MessageReportingTask.scala
new file mode 100644
index 0000000..5171327
--- /dev/null
+++ b/src/main/scala/viper/server/core/MessageReportingTask.scala
@@ -0,0 +1,38 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.core
+
+import viper.server.vsi.MessageStreamingTask
+import viper.silver.ast.Program
+import viper.silver.reporter.{EntityFailureMessage, EntitySuccessMessage, Message, Reporter}
+
+trait MessageReportingTask extends MessageStreamingTask[Program] with ViperPost {
+
+  protected def enqueueMessage(msg: Message): Unit = {
+    super.enqueueMessage(pack(msg))
+  }
+
+  // Implementation of the Reporter interface used by the backend.
+  class ActorReporter(tag: String) extends Reporter {
+    val name = s"ViperServer_$tag"
+
+    def report(msg: Message): Unit = {
+      //TODO use logger
+      //println(s">>> ActorReporter.report($msg)")
+      msg match {
+        case m: EntityFailureMessage if m.concerning.info.isCached =>
+        case m: EntitySuccessMessage if m.concerning.info.isCached =>
+          // Do not re-send messages about AST nodes that have been cached;
+          // the information about these nodes is going to be reported anyway.
+
+        case m =>
+          enqueueMessage(m)
+      }
+    }
+  }
+
+}
diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index 33fcc67..926f327 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -8,8 +8,7 @@ package viper.server.core
 
 import ch.qos.logback.classic.Logger
 import viper.carbon.CarbonFrontend
-import viper.server.ViperConfig
-import viper.server.vsi.{Envelope, VerificationTask}
+import viper.server.vsi.Envelope
 import viper.silicon.SiliconFrontend
 import viper.silver.ast._
 import viper.silver.frontend.{DefaultStates, SilFrontend}
@@ -17,7 +16,7 @@ import viper.silver.reporter.{Reporter, _}
 import viper.silver.verifier.{AbstractVerificationError, VerificationResult, _}
 
 import scala.collection.mutable.ListBuffer
-import scala.concurrent.ExecutionContext
+import scala.concurrent.{ExecutionContext, Future}
 import scala.language.postfixOps
 
 class ViperServerException extends Exception
@@ -28,13 +27,14 @@ case class ViperServerBackendNotFoundException(name: String) extends ViperServer
   override def toString: String = s"Verification backend (<: SilFrontend) `$name` could not be found."
 }
 
-case class SilverEnvelope(m: Message) extends Envelope
+case class ViperEnvelope(m: Message) extends Envelope
 
-class VerificationWorker(private val viper_config: ViperConfig,
-                         private val logger: Logger,
+class VerificationWorker(private val logger: Logger,
                          private val command: List[String],
-                         private val program: Program)(implicit val ec: ExecutionContext) extends VerificationTask {
+                         private val program: Program)(implicit val ec: ExecutionContext)
+  extends MessageReportingTask {
 
+  override def artifact: Option[Future[Nothing]] = None
   private var backend: ViperBackend = _
 
   private def resolveCustomBackend(clazzName: String, rep: Reporter): Option[SilFrontend] = {
@@ -56,15 +56,6 @@ class VerificationWorker(private val viper_config: ViperConfig,
     }
   }
 
-  // Implementation of the Reporter interface used by the backend.
-  class ActorReporter(val tag: String) extends Reporter {
-    val name = s"ViperServer_$tag"
-
-    def report(msg: Message): Unit = {
-      enqueueMessages(msg)
-    }
-  }
-
   def run(): Unit = {
     try {
       command match {
@@ -88,8 +79,9 @@ class VerificationWorker(private val viper_config: ViperConfig,
       case _: InterruptedException =>
       case _: java.nio.channels.ClosedByInterruptException =>
       case e: Throwable =>
-        enqueueMessages(ExceptionReport(e))
-        logger.trace(s"Creation/Execution of the verification backend ${if (backend == null) "<null>" else backend.toString} resulted in exception.", e)
+        enqueueMessage(ExceptionReport(e))
+        logger.trace(s"Creation/Execution of the verification backend " +
+          s"${if (backend == null) "<null>" else backend.toString} resulted in an exception.", e)
     } finally {
       try {
         backend.stop()
@@ -106,12 +98,6 @@ class VerificationWorker(private val viper_config: ViperConfig,
       registerTaskEnd(false)
     }
   }
-
-  override type A = Message
-
-  override def pack(m: A): Envelope = {
-    SilverEnvelope(m)
-  }
 }
 
 class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program) {
@@ -126,116 +112,9 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
       s"ViperBackend( ${_frontend.verifier.name} )"
   }
 
-  private def collectDefinitions(program: Program): List[Definition] = {
-    (program.members.collect {
-      case t: Method =>
-        (Definition(t.name, "Method", t.pos) +: (t.pos match {
-          case p: AbstractSourcePosition =>
-            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) } ++
-              t.formalReturns.map { arg => Definition(arg.name, "Return", arg.pos, Some(p)) }
-          case _ => Seq()
-        })) ++ t.deepCollectInBody {
-          case scope: Scope with Positioned =>
-            scope.pos match {
-              case p: AbstractSourcePosition =>
-                scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
-              case _ => Seq()
-            }
-        }.flatten
-
-      case t: Function =>
-        (Definition(t.name, "Function", t.pos) +: (t.pos match {
-          case p: AbstractSourcePosition =>
-            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) }
-          case _ => Seq()
-        })) ++ (t.body match {
-          case Some(exp) =>
-            exp.deepCollect {
-              case scope:Scope with Positioned =>
-                scope.pos match {
-                  case p: AbstractSourcePosition =>
-                    scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
-                  case _ => Seq()
-                }
-            } flatten
-          case _ => Seq()
-        })
-
-      case t: Predicate =>
-        (Definition(t.name, "Predicate", t.pos) +: (t.pos match {
-          case p: AbstractSourcePosition =>
-            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) }
-          case _ => Seq()
-        })) ++ (t.body match {
-          case Some(exp) =>
-            exp.deepCollect {
-              case scope:Scope with Positioned =>
-                scope.pos match {
-                  case p: AbstractSourcePosition =>
-                    scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
-                  case _ => Seq()
-                }
-            } flatten
-          case _ => Seq()
-        })
-
-      case t: Domain =>
-        (Definition(t.name, "Domain", t.pos) +: (t.pos match {
-          case p: AbstractSourcePosition =>
-            t.functions.flatMap { func =>
-              Definition(func.name, "Function", func.pos, Some(p)) +: (func.pos match {
-                case func_p: AbstractSourcePosition =>
-                  func.formalArgs.map { arg => Definition(if (arg.isInstanceOf[LocalVarDecl]) arg.asInstanceOf[LocalVarDecl].name else "unnamed parameter", "Argument", arg.pos, Some(func_p)) }
-                case _ => Seq()
-              })
-            } ++ t.axioms.flatMap { ax =>
-              Definition(if (ax.isInstanceOf[NamedDomainAxiom]) ax.asInstanceOf[NamedDomainAxiom].name else "", "Axiom", ax.pos, Some(p)) +: (ax.pos match {
-                case ax_p: AbstractSourcePosition =>
-                  ax.exp.deepCollect {
-                    case scope:Scope with Positioned =>
-                      scope.pos match {
-                        case p: AbstractSourcePosition =>
-                          scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
-                        case _ => Seq()
-                      }
-                  } flatten
-                case _ => Seq()
-              }) }
-          case _ => Seq()
-        })) ++ Seq()
-
-      case t: Field =>
-        Seq(Definition(t.name, "Field", t.pos))
-
-    } flatten) toList
-  }
-
-  private def countInstances(p: Program): Map[String, Int] = p.members.groupBy({
-    case m: Method => "method"
-    case fu: Function => "function"
-    case p: Predicate => "predicate"
-    case d: Domain => "domain"
-    case fi: Field => "field"
-    case _ => "other"
-  }).view.mapValues(_.size).toMap
-
-  private def reportProgramStats(prog: Program): Unit = {
-    val stats = countInstances(prog)
-
-    _frontend.reporter.report(ProgramOutlineReport(prog.members.toList))
-    _frontend.reporter.report(StatisticsReport(
-      stats.getOrElse("method", 0),
-      stats.getOrElse("function", 0),
-      stats.getOrElse("predicate", 0),
-      stats.getOrElse("domain", 0),
-      stats.getOrElse("field", 0)
-    ))
-    _frontend.reporter.report(ProgramDefinitionsReport(collectDefinitions(prog)))
-  }
-
   /** Run the backend verification functionality
     * */
-  def execute(args: Seq[String]){
+  def execute(args: Seq[String]): Unit = {
     val (head, tail) = args.splitAt(args.length-1)
     val fileless_args = head ++ Seq("--ignoreFile") ++ tail
     _frontend.setStartTime()
@@ -244,8 +123,6 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
     if (!_frontend.prepare(fileless_args)) return
     _frontend.init( _frontend.verifier )
 
-    reportProgramStats(_ast)
-
     val temp_result: Option[VerificationResult] = if (_frontend.config.disableCaching()) {
       _frontend.logger.info("Verification with caching disabled")
       Some(_frontend.verifier.verify(_ast))
@@ -269,7 +146,7 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
     _frontend.verifier.stop()
   }
 
-  private def doCachedVerification(real_program: Program) = {
+  private def doCachedVerification(real_program: Program): Unit = {
     /** Top level branch is here for the same reason as in
       * {{{viper.silver.frontend.DefaultFrontend.verification()}}} */
 
@@ -278,47 +155,80 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
 
     // collect and report errors
     val all_cached_errors: collection.mutable.ListBuffer[VerificationError] = ListBuffer()
-    cached_results.foreach (result => {
+    cached_results.foreach((result: CacheResult) => {
       val cached_errors = result.verification_errors
-      if(cached_errors.isEmpty){
-        _frontend.reporter.report(CachedEntityMessage(_frontend.getVerifierName,result.method, Success))
+      if (cached_errors.isEmpty) {
+        _frontend.reporter report
+          CachedEntityMessage(_frontend.getVerifierName, result.method, Success)
       } else {
         all_cached_errors ++= cached_errors
-        _frontend.reporter.report(CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(all_cached_errors.toSeq)))
+        _frontend.reporter report
+          CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(cached_errors))
       }
     })
 
+    val methodsToVerify: Seq[Method] = transformed_prog.methods.filter(_.body.isDefined)
+
     _frontend.logger.debug(
       s"Retrieved data from cache..." +
         s" cachedErrors: ${all_cached_errors.map(_.loggableMessage)};" +
-        s" methodsToVerify: ${cached_results.map(_.method.name)}.")
+        s" cachedMethods: ${cached_results.map(_.method.name)};" +
+        s" methodsToVerify: ${methodsToVerify.map(_.name)}.")
     _frontend.logger.trace(s"The cached program is equivalent to: \n${transformed_prog.toString()}")
 
-    _frontend.setVerificationResult(_frontend.verifier.verify(transformed_prog))
+    val ver_result: VerificationResult = _frontend.verifier.verify(transformed_prog)
+    _frontend.setVerificationResult(ver_result)
     _frontend.setState(DefaultStates.Verification)
 
-    // update cache
-    val methodsToVerify = transformed_prog.methods.filter(_.body.isDefined)
-    methodsToVerify.foreach(m => {
+    _frontend.logger.debug(s"Latest verification result: $ver_result")
+
+    val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]])] = methodsToVerify.map((m: Method) => {
       // Results come back irrespective of program Member.
-      val cachable_errors =
-        for {
-          verRes <- _frontend.getVerificationResult
-          cache_errs <- verRes match {
-            case Failure(errs) => getMethodSpecificErrors(m, errs)
-            case Success => Some(Nil)
+      val cacheable_errors: Option[List[AbstractVerificationError]] = for {
+        verRes <- _frontend.getVerificationResult
+        cache_errs <- verRes match {
+          case Failure(errs) =>
+            val r = getMethodSpecificErrors(m, errs)
+            _frontend.logger.debug(s"getMethodSpecificErrors returned $r")
+            r
+          case Success =>
+            Some(Nil)
+        }
+      } yield cache_errs
+
+      (m, cacheable_errors)
+    })
+
+    // Check that the mapping from errors to methods is not messed up
+    // (otherwise it is unsafe to cache the results)
+    val update_cache_criterion: Boolean = {
+      val all_errors_in_file = meth_to_err_map.flatMap(_._2).flatten
+      _frontend.getVerificationResult.get match {
+        case Success =>
+          all_errors_in_file.isEmpty
+        case Failure(errors) =>
+          // FIXME find a better sorting criterion
+          errors.sortBy(ae => ae.hashCode()) == all_errors_in_file.sortBy(ae => ae.hashCode())
+      }
+    }
+
+    if (update_cache_criterion) {
+      // update cache
+      meth_to_err_map.foreach { case (m: Method, cacheable_errors: Option[List[AbstractVerificationError]]) =>
+        _frontend.logger.debug(s"Obtained cacheable errors: $cacheable_errors")
+
+        if (cacheable_errors.isDefined) {
+          ViperCache.update(backendName, file, m, transformed_prog, cacheable_errors.get) match {
+            case e :: es =>
+              _frontend.logger.trace(s"Storing new entry in cache for method (${m.name}): $e. Other entries for this method: ($es)")
+            case Nil =>
+              _frontend.logger.trace(s"Storing new entry in cache for method (${m.name}) FAILED.")
           }
-        } yield cache_errs
-
-      if(cachable_errors.isDefined){
-        ViperCache.update(backendName, file, m, transformed_prog, cachable_errors.get) match {
-          case e :: es =>
-            _frontend.logger.trace(s"Storing new entry in cache for method (${m.name}): $e. Other entries for this method: ($es)")
-          case Nil =>
-            _frontend.logger.trace(s"Storing new entry in cache for method (${m.name}) FAILED.")
         }
       }
-    })
+    } else {
+      _frontend.logger.debug(s"Inconsistent error splitting; no cache update for this verification attempt in $file.")
+    }
 
     // combine errors:
     if (all_cached_errors.nonEmpty) {
@@ -340,11 +250,13 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
     * if the error belongs to the method and return None.
     */
   private def getMethodSpecificErrors(m: Method, errors: Seq[AbstractError]): Option[List[AbstractVerificationError]] = {
-    val methodPos = m.pos match {
-      case sp: SourcePosition => Some(sp.start.line, sp.end.get.line)
-      case _ => {
+    val methodPos: Option[(Int, Int)] = m.pos match {
+      case sp: SourcePosition =>
+        /** Only the line component matters (not the column) since,
+          * in Viper, each method must be declared on a new line. */
+        Some(sp.start.line, sp.end.get.line)
+      case _ =>
         None
-      }
     }
     val result = scala.collection.mutable.ListBuffer[AbstractVerificationError]()
 
@@ -356,12 +268,13 @@ class ViperBackend(private val _frontend: SilFrontend, private val _ast: Program
         e.pos match {
           case pos: HasLineColumn =>
             val errorPos = pos.line
-            if (methodPos.isEmpty)
-            {
+            if (methodPos.isEmpty) {
               return None
             }
             // The position of the error is used to determine to which Method it belongs.
-            if (errorPos >= methodPos.get._1 && errorPos <= methodPos.get._2) result += e
+            if (methodPos.get._1 <= errorPos && errorPos <= methodPos.get._2) {
+              result += e
+            }
           case _ =>
             return None
         }
diff --git a/src/main/scala/viper/server/core/ViperBackendConfig.scala b/src/main/scala/viper/server/core/ViperBackendConfig.scala
index c357edc..b30bb8d 100644
--- a/src/main/scala/viper/server/core/ViperBackendConfig.scala
+++ b/src/main/scala/viper/server/core/ViperBackendConfig.scala
@@ -6,14 +6,40 @@
 
 package viper.server.core
 
+
+import viper.server.utility.Helpers.getArgListFromArgString
+
+
 trait ViperBackendConfig {
+  val backend_name: String
   val partialCommandLine: List[String]
+
+  def toList: List[String] = this match {
+    case _ : SiliconConfig => "silicon" :: partialCommandLine
+    case _ : CarbonConfig => "carbon" :: partialCommandLine
+    case _ : CustomConfig => "custom" :: partialCommandLine
+  }
 }
 
-object ViperBackendConfigs {
-  object EmptyConfig extends ViperBackendConfig {val partialCommandLine: List[String] = Nil}
+case class SiliconConfig(partialCommandLine: List[String]) extends ViperBackendConfig {
+  override val backend_name = "silicon"
+}
+
+case class CarbonConfig(partialCommandLine: List[String]) extends ViperBackendConfig {
+  override val backend_name = "carbon"
+}
+
+case class CustomConfig(partialCommandLine: List[String], backend_name: String) extends ViperBackendConfig
+
+object ViperBackendConfig {
 
-  case class SiliconConfig(partialCommandLine: List[String]) extends ViperBackendConfig
-  case class CarbonConfig(partialCommandLine: List[String]) extends ViperBackendConfig
-  case class CustomConfig(partialCommandLine: List[String]) extends ViperBackendConfig
+  def apply(args: List[String]): ViperBackendConfig = args match {
+    //    case Nil => EmptyConfig
+    case "silicon" :: args =>  SiliconConfig(args)
+    case "carbon" :: args => CarbonConfig(args)
+    case custom :: args => CustomConfig(args, custom)
+    case invalid => throw new IllegalArgumentException(s"cannot build ViperConfig from string `$invalid`")
+  }
+  
+  def apply(input: String): ViperBackendConfig = apply(getArgListFromArgString(input))
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala
index 858ada7..7241e1f 100644
--- a/src/main/scala/viper/server/core/ViperCache.scala
+++ b/src/main/scala/viper/server/core/ViperCache.scala
@@ -6,6 +6,7 @@
 
 package viper.server.core
 
+import scala.language.postfixOps
 import ch.qos.logback.classic.Logger
 import viper.server.core.ViperCache.logger
 import viper.server.vsi._
@@ -14,6 +15,7 @@ import viper.silver.utility.CacheHelper
 import viper.silver.verifier.errors._
 import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors}
 
+import scala.annotation.tailrec
 import scala.collection.mutable.{Map => MutableMap}
 
 // ===== CACHE OBJECT ==================================================================
@@ -291,9 +293,9 @@ object ViperCache extends Cache {
 
 object ViperCacheHelper {
   private val _node_hash_memo = MutableMap.empty[String, MutableMap[Node, String]]
-  def node_hash_memo = _node_hash_memo
+  def node_hash_memo: MutableMap[String, MutableMap[Node, String]] = _node_hash_memo
 
-  protected def hex(h: String) = h.hashCode.toHexString
+  protected def hex(h: String): String = h.hashCode.toHexString
 
   /**
     * This method is used for computing unique-ish hashes of AST nodes.
@@ -312,8 +314,10 @@ object ViperCacheHelper {
     *
     * The second argument list is used for specifying external keys as (backend, file).
     *  This is needed for removing separate parts of the hash table.
+    *
     *  @see [[forgetFile]].
     */
+  @tailrec
   private def getHashForNode(node: Node)(implicit key: String): String = node match {
     case m: Method => removeBody(m).entityHash
     case hn: Hashable => hn.entityHash
@@ -467,14 +471,20 @@ class AccessPath(val accessPath: List[Number]) {
 
 case class ViperAst(p: Program) extends Ast {
 
-  def compose(cs: List[CacheableMember]): Ast = {
-    val new_methods: List[Method] = cs.map(_.asInstanceOf[ViperMethod].m)
-    val new_program = Program(p.domains, p.fields, p.functions, p.predicates, new_methods, p.extensions)(p.pos, p.info, p.errT)
+  override def compose(cs: List[CacheableMember]): Ast = {
+    // FIXME Use polymorphic types instead of casts!
+    val new_methods: List[Method] = cs filter { _.isInstanceOf[ViperMethod] } map { vm => vm.asInstanceOf[ViperMethod].m }
+    val new_predicates: List[Predicate] = cs filter { _.isInstanceOf[ViperPredicate] } map { vp => vp.asInstanceOf[ViperPredicate].p }
+    val new_functions: List[Function] = cs filter { _.isInstanceOf[ViperFunction] } map { vf => vf.asInstanceOf[ViperFunction].f }
+    val new_program = Program(p.domains, p.fields,
+      new_functions, new_predicates, new_methods, p.extensions)(p.pos, p.info, p.errT)
     ViperAst(new_program)
   }
 
-  def decompose(): List[CacheableMember] = {
-    p.methods.map(m => ViperMethod(m)).toList
+  override def decompose(): List[CacheableMember] = {
+    p.methods.map(m => ViperMethod(m)) ++
+      p.predicates.map(p => ViperPredicate(p)) ++
+      p.functions.map(f => ViperFunction(f)) toList
   }
 
   override def equals(other: Ast): Boolean = {
@@ -505,4 +515,34 @@ case class ViperMethod(m: Method) extends CacheableMember {
     val p = ast.asInstanceOf[ViperAst].p
     p.getDependencies(p, m).map(h => ViperMember(h))
   }
+}
+
+case class ViperPredicate(p: Predicate) extends CacheableMember {
+  def hash(): String = {
+    p.entityHash
+  }
+
+  def transform: CacheableMember = {
+    ViperPredicate(p.copy()(p.pos, ConsInfo(p.info, Cached), p.errT))
+  }
+
+  def getDependencies(ast: Ast): List[Member] = {
+    val p = ast.asInstanceOf[ViperAst].p
+    p.members filter (_.entityHash != hash()) map (h => ViperMember(h)) toList
+  }
+}
+
+case class ViperFunction(f: Function) extends CacheableMember {
+  def hash(): String = {
+    f.entityHash
+  }
+
+  def transform: CacheableMember = {
+    ViperFunction(f.copy()(f.pos, ConsInfo(f.info, Cached), f.errT))
+  }
+
+  def getDependencies(ast: Ast): List[Member] = {
+    val p = ast.asInstanceOf[ViperAst].p
+    p.members filter (_.entityHash != hash()) map (h => ViperMember(h)) toList
+  }
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 7af69b3..646a636 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -6,18 +6,19 @@
 
 package viper.server.core
 
+import akka.Done
 import akka.actor.ActorRef
 import viper.server.ViperConfig
-import viper.server.core.ViperBackendConfigs._
-import viper.server.vsi.{Envelope, JobID, VerificationServer}
+import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
 import viper.silver.ast.Program
 import viper.silver.logger.ViperLogger
-import viper.silver.reporter.Message
 
 import scala.concurrent.Future
 import scala.language.postfixOps
 
-class ViperCoreServer(val _args: Array[String]) extends VerificationServer {
+class ViperCoreServer(val _args: Array[String]) extends VerificationServer with ViperPost {
+
+  override type AST = Program
 
   // --- VCS : Configuration ---
   protected var _config: ViperConfig = _
@@ -42,33 +43,76 @@ class ViperCoreServer(val _args: Array[String]) extends VerificationServer {
     ViperCache.initialize(logger.get, config.backendSpecificCache())
 
     super.start(config.maximumActiveJobs())
-    println(s"ViperCoreServer started.")
+    println(s"ViperCoreServer has started.")
+  }
+
+  def requestAst(arg_list: List[String]): AstJobId = {
+    require(config != null)
+
+    val task_backend = new AstWorker(arg_list, logger.get)
+    val ast_id = initializeAstConstruction(task_backend)
+
+    if (ast_id.id >= 0) {
+      logger.get.info(s"Verification process #${ast_id.id} has successfully started.")
+    } else {
+      logger.get.error(s"Could not start verification process. " +
+        s"The maximum number of active verification jobs are currently running (${ver_jobs.MAX_ACTIVE_JOBS}).")
+    }
+    ast_id
+  }
+
+  def verify(ast_id: AstJobId, backend_config: ViperBackendConfig): VerJobId = {
+
+    if (!isRunning) throw new IllegalStateException("Instance of VerificationServer already stopped")
+    require(backend_config != null)
+
+    val programId = s"ViperAst#${ast_id.id}"
+    val args: List[String] = backend_config.toList
+
+    ast_jobs.lookupJob(ast_id) match {
+      case Some(handle_future) =>
+        val task_backend_fut =
+          handle_future.map((handle: AstHandle[Program]) => {
+            val art: Future[Program] = handle.artifact
+            art.map(program => {
+              new VerificationWorker(logger.get, args :+ programId, program)
+            }).recover({
+              case e: Throwable =>
+                println(s"### As exception has occurred while constructing Viper AST: $e")
+                throw e
+            })
+
+          }).flatten
+
+        initializeVerificationProcess(task_backend_fut, Some(ast_id))
+
+      case None =>
+        logger.get.error(s"Could not start verification process for non-existent $ast_id")
+        VerJobId(-1)
+    }
   }
 
   /** Verifies a Viper AST using the specified backend.
     *
     * Expects a non-null backend config and Viper AST.
     * */
-  def verify(programID: String, backend_config: ViperBackendConfig, program: Program): JobID = {
+  def verify(programId: String, backend_config: ViperBackendConfig, program: Program): VerJobId = {
     require(program != null && backend_config != null)
 
-    val args: List[String] = backend_config match {
-      case _ : SiliconConfig => "silicon" :: backend_config.partialCommandLine
-      case _ : CarbonConfig => "carbon" :: backend_config.partialCommandLine
-      case _ : CustomConfig => "custom" :: backend_config.partialCommandLine
-    }
-    val task_backend = new VerificationWorker(_config, logger.get, args :+ programID, program)
-    val jid = initializeVerificationProcess(task_backend)
-    if(jid.id >= 0) {
-      logger.get.info(s"Verification process #${jid.id} has successfully started.")
+    val args: List[String] = backend_config.toList
+    val task_backend = new VerificationWorker(logger.get, args :+ programId, program)
+    val ver_id = initializeVerificationProcess(Future.successful(task_backend), None)
+
+    if (ver_id.id >= 0) {
+      logger.get.info(s"Verification process #${ver_id.id} has successfully started.")
     } else {
       logger.get.error(s"Could not start verification process. " +
-        s"The maximum number of active verification jobs are currently running (${jobs.MAX_ACTIVE_JOBS}).")
+        s"The maximum number of active verification jobs are currently running (${ver_jobs.MAX_ACTIVE_JOBS}).")
     }
-    jid
+    ver_id
   }
 
-  override def streamMessages(jid: JobID, clientActor: ActorRef): Option[Future[Unit]] = {
+  override def streamMessages(jid: VerJobId, clientActor: ActorRef): Option[Future[Done]] = {
     logger.get.info(s"Streaming results for job #${jid.id}.")
     super.streamMessages(jid, clientActor)
   }
@@ -86,10 +130,5 @@ class ViperCoreServer(val _args: Array[String]) extends VerificationServer {
     super.stop()
   }
 
-  override type A = Message
-  override def unpack(e: Envelope): A = {
-    e match {
-      case SilverEnvelope(m) => m
-    }
-  }
+
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/server/core/ViperCoreServerUtils.scala b/src/main/scala/viper/server/core/ViperCoreServerUtils.scala
index f547c29..2199c3f 100644
--- a/src/main/scala/viper/server/core/ViperCoreServerUtils.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServerUtils.scala
@@ -9,15 +9,15 @@ package viper.server.core
 import akka.actor.{Actor, ActorSystem, Props}
 import akka.pattern.ask
 import akka.util.Timeout
-import viper.server.vsi.{JobID, JobNotFoundException}
+import viper.server.vsi.{JobNotFoundException, VerJobId}
 import viper.silver.reporter.{EntityFailureMessage, Message}
 import viper.silver.verifier.{AbstractError, VerificationResult, Failure => VerificationFailure, Success => VerificationSuccess}
 
 import scala.concurrent.duration._
-import scala.concurrent.{ExecutionContext, Future}
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor, Future}
 
 object ViperCoreServerUtils {
-  implicit private val executionContext = ExecutionContext.global
+  implicit private val executionContext: ExecutionContextExecutor = ExecutionContext.global
 
   private object SeqActor {
     case object Result
@@ -43,18 +43,14 @@ object ViperCoreServerUtils {
     *
     * Deletes the jobHandle on completion.
     */
-  def getMessagesFuture(core: ViperCoreServer, jid: JobID)(implicit actor_system: ActorSystem): Future[List[Message]] = {
+  def getMessagesFuture(core: ViperCoreServer, jid: VerJobId)(implicit actor_system: ActorSystem): Future[List[Message]] = {
     import scala.language.postfixOps
 
     val actor = actor_system.actorOf(SeqActor.props())
-    val complete_future = core.streamMessages(jid, actor).getOrElse(return Future.failed(JobNotFoundException()))
+    val complete_future = core.streamMessages(jid, actor).getOrElse(return Future.failed(JobNotFoundException))
     val res: Future[List[Message]] = complete_future.flatMap(_ => {
       implicit val askTimeout: Timeout = Timeout(core.config.actorCommunicationTimeout() milliseconds)
-      val answer: Future[Any] = actor ? SeqActor.Result
-      //recover result type from "Any"
-      answer.map({
-        case res: List[Message] => res
-      })
+      (actor ? SeqActor.Result).mapTo[List[Message]]
     })
     res
   }
@@ -66,7 +62,7 @@ object ViperCoreServerUtils {
     *
     * Deletes the jobHandle on completion.
     */
-  def getResultsFuture(core: ViperCoreServer, jid: JobID)(implicit actor_system: ActorSystem): Future[VerificationResult] = {
+  def getResultsFuture(core: ViperCoreServer, jid: VerJobId)(implicit actor_system: ActorSystem): Future[VerificationResult] = {
     val messages_future = getMessagesFuture(core, jid)
     val result_future: Future[VerificationResult] = messages_future.map(msgs => {
 
diff --git a/src/main/scala/viper/server/core/ViperPost.scala b/src/main/scala/viper/server/core/ViperPost.scala
new file mode 100644
index 0000000..9a9b612
--- /dev/null
+++ b/src/main/scala/viper/server/core/ViperPost.scala
@@ -0,0 +1,22 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.core
+
+import viper.server.vsi.{Envelope, Post}
+import viper.silver.reporter.Message
+
+trait ViperPost extends Post {
+  override type A = Message
+
+  override def unpack(e: Envelope): Message = {
+    e match {
+      case ViperEnvelope(m) => m
+    }
+  }
+
+  override def pack(m: Message): Envelope = ViperEnvelope(m)
+}
diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala
index 34ab114..7a750d3 100644
--- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala
+++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala
@@ -15,22 +15,21 @@ import akka.stream.scaladsl.Source
 import edu.mit.csail.sdg.alloy4.A4Reporter
 import edu.mit.csail.sdg.parser.CompUtil
 import edu.mit.csail.sdg.translator.{A4Options, TranslateAlloyToKodkod}
-import spray.json.DefaultJsonProtocol
+import spray.json.{DefaultJsonProtocol, RootJsonFormat}
 import viper.server.ViperConfig
-import viper.server.core.ViperBackendConfigs.{CarbonConfig, CustomConfig, SiliconConfig}
-import viper.server.core.{ViperCache, ViperCoreServer}
+import viper.server.core.{AstConstructionFailureException, ViperBackendConfig, ViperCache, ViperCoreServer}
 import viper.server.frontends.http.jsonWriters.ViperIDEProtocol.{AlloyGenerationRequestComplete, AlloyGenerationRequestReject, CacheFlushAccept, CacheFlushReject, JobDiscardAccept, JobDiscardReject, ServerStopConfirmed, VerificationRequestAccept, VerificationRequestReject}
-import viper.server.utility.AstGenerator
+import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile}
+import viper.server.utility.ibm
 import viper.server.vsi.Requests.CacheResetRequest
 import viper.server.vsi._
-import viper.silver.ast.Program
 import viper.silver.logger.ViperLogger
 import viper.silver.reporter.Message
 
 import scala.util.{Failure, Success, Try}
 
 class ViperHttpServer(_args: Array[String])
-  extends ViperCoreServer(_args) with VerificationServerHTTP {
+  extends ViperCoreServer(_args) with VerificationServerHttp {
 
   override def start(): Unit = {
     _config = new ViperConfig(_args.toIndexedSeq)
@@ -41,9 +40,9 @@ class ViperHttpServer(_args: Array[String])
 
     ViperCache.initialize(logger.get, config.backendSpecificCache())
 
-    port = config.port()
+    port = config.port.getOrElse(ibm.Socket.findFreePort)
     super.start(config.maximumActiveJobs())
-    println(s"ViperServer online at http://localhost:${config.port()}")
+    println(s"ViperServer online at http://localhost:$port}")
   }
 
   def setRoutes(): Route = {
@@ -63,43 +62,27 @@ class ViperHttpServer(_args: Array[String])
   }
 
   override def onVerifyPost(vr: Requests.VerificationRequest): ToResponseMarshallable = {
-    // Extract file name from args list
     val arg_list = getArgListFromArgString(vr.arg)
-    val file: String = arg_list.last
-    val arg_list_partial = arg_list.dropRight(1)
-
-    // Parse file
-    val astGen = new AstGenerator(_logger)
-    var ast_option: Option[Program] = None
-    try {
-      ast_option = astGen.generateViperAst(file)
-    } catch {
-      case _: java.nio.file.NoSuchFileException =>
-        return VerificationRequestReject("The file for which verification has been requested was not found.")
+
+    if (!validateViperFile(arg_list.last)) {
+      return VerificationRequestReject("File not found")
     }
-    val ast = ast_option.getOrElse(return VerificationRequestReject("The file for which verification has been requested contained syntax errors."))
-
-    // prepare backend config
-    val backend = arg_list_partial match {
-      case "silicon" :: args => SiliconConfig(args)
-      case "carbon" :: args => CarbonConfig(args)
-      case "custom" :: args => CustomConfig(args)
-      case args =>
-        logger.get.error(s"Invalid arguments: ${args.toString} " +
+
+    val ast_id = requestAst(arg_list)
+
+    val arg_list_partial: List[String] = arg_list.dropRight(1)
+    val backend = try {
+      ViperBackendConfig(arg_list_partial)
+    } catch {
+      case _: IllegalArgumentException =>
+        logger.get.error(s"Invalid arguments: ${vr.arg} " +
           s"You need to specify the verification backend, e.g., `silicon [args]`")
         return VerificationRequestReject("Invalid arguments for backend.")
     }
 
-    val jid: JobID = verify(file, backend, ast)
+    val ver_id = verify(ast_id, backend)
 
-    if (jid.id >= 0) {
-      logger.get.info(s"Verification process #${jid.id} has successfully started.")
-      VerificationRequestAccept(jid.id)
-    } else {
-      logger.get.error(s"Could not start verification process. " +
-        s"The maximum number of active verification jobs are currently running (${jobs.MAX_ACTIVE_JOBS}).")
-      VerificationRequestReject(s"the maximum number of active verification jobs are currently running (${jobs.MAX_ACTIVE_JOBS}).")
-    }
+    VerificationRequestAccept(ast_id, ver_id)
   }
 
   override def unpackMessages(s: Source[Envelope, NotUsed]): ToResponseMarshallable = {
@@ -110,9 +93,12 @@ class ViperHttpServer(_args: Array[String])
 
   override def verificationRequestRejection(jid: Int, e: Throwable): ToResponseMarshallable = {
     e match {
-      case JobNotFoundException() =>
+      case JobNotFoundException =>
         logger.get.error(s"The verification job #$jid does not exist.")
         VerificationRequestReject(s"The verification job #$jid does not exist.")
+      case AstConstructionFailureException =>
+        logger.get.error(s"The verification job #$jid could not be created since the AST is inconsistent.")
+        VerificationRequestReject(s"The verification job #$jid could not be created since the AST is inconsistent.")
       case _ =>
         logger.get.error(s"The verification job #$jid resulted in a terrible error: $e")
         VerificationRequestReject(s"The verification job #$jid resulted in a terrible error: $e")
@@ -172,7 +158,7 @@ class ViperHttpServer(_args: Array[String])
       post {
         object AlloyRequest extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol {
           case class AlloyGenerationRequest(arg: String, solver: String)
-          implicit val generateStuff = jsonFormat2(AlloyGenerationRequest.apply)
+          implicit val generateStuff: RootJsonFormat[AlloyRequest.AlloyGenerationRequest] = jsonFormat2(AlloyGenerationRequest.apply)
         }
 
         entity(as[AlloyRequest.AlloyGenerationRequest]) { r =>
@@ -210,13 +196,4 @@ class ViperHttpServer(_args: Array[String])
       }
     }
   }
-
-  private def getArgListFromArgString(arg_str: String): List[String] = {
-    val possibly_quoted_string = raw"""[^\s"']+|"[^"]*"|'[^']*'""".r
-    val quoted_string = """^["'](.*)["']$""".r
-    possibly_quoted_string.findAllIn(arg_str).toList.map {
-      case quoted_string(noqt_a) => noqt_a
-      case a => a
-    }
-  }
 }
diff --git a/src/main/scala/viper/server/frontends/http/ViperRequests.scala b/src/main/scala/viper/server/frontends/http/ViperRequests.scala
index 1a4d128..1825ac5 100644
--- a/src/main/scala/viper/server/frontends/http/ViperRequests.scala
+++ b/src/main/scala/viper/server/frontends/http/ViperRequests.scala
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
 package viper.server.frontends.http
 
 import spray.json.{DefaultJsonProtocol, RootJsonFormat}
diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/AlloySolutionWriter.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/AlloySolutionWriter.scala
index dce03e9..b46a5ff 100644
--- a/src/main/scala/viper/server/frontends/http/jsonWriters/AlloySolutionWriter.scala
+++ b/src/main/scala/viper/server/frontends/http/jsonWriters/AlloySolutionWriter.scala
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
 package viper.server.frontends.http.jsonWriters
 
 import edu.mit.csail.sdg.ast.Sig.Field
diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/SymbExLogReportWriter.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/SymbExLogReportWriter.scala
index 5546984..d5de61a 100644
--- a/src/main/scala/viper/server/frontends/http/jsonWriters/SymbExLogReportWriter.scala
+++ b/src/main/scala/viper/server/frontends/http/jsonWriters/SymbExLogReportWriter.scala
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
 package viper.server.frontends.http.jsonWriters
 
 import spray.json.{JsArray, JsField, JsNull, JsObject, JsString, JsValue}
diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/TermWriter.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/TermWriter.scala
index 194821a..b474740 100644
--- a/src/main/scala/viper/server/frontends/http/jsonWriters/TermWriter.scala
+++ b/src/main/scala/viper/server/frontends/http/jsonWriters/TermWriter.scala
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
 package viper.server.frontends.http.jsonWriters
 
 import spray.json.{JsArray, JsNull, JsObject, JsString, JsValue}
diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala
index ec46b4e..0892f9f 100644
--- a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala
+++ b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
 package viper.server.frontends.http.jsonWriters
 
 import akka.NotUsed
@@ -6,16 +12,17 @@ import akka.stream.scaladsl.Flow
 import akka.util.ByteString
 import edu.mit.csail.sdg.translator.A4Solution
 import spray.json.DefaultJsonProtocol
+import viper.server.vsi.{AstJobId, VerJobId}
 import viper.silicon.SymbLog
 import viper.silicon.state.terms.Term
 import viper.silver.reporter._
-import viper.silver.verifier._
+import viper.silver.verifier.{ValueEntry, _}
 
 object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol {
 
   import spray.json._
 
-  final case class VerificationRequestAccept(id: Int)
+  final case class VerificationRequestAccept(ast_id: AstJobId, ver_id: VerJobId)
   final case class VerificationRequestReject(msg: String)
   final case class ServerStopConfirmed(msg: String)
   final case class JobDiscardAccept(msg: String)
@@ -26,7 +33,12 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
   final case class AlloyGenerationRequestComplete(solution: A4Solution)
 
 
-  implicit val verReqAccept_format: RootJsonFormat[VerificationRequestAccept] = jsonFormat1(VerificationRequestAccept.apply)
+  implicit val verReqAccept_writer: RootJsonFormat[VerificationRequestAccept] = lift(new RootJsonWriter[VerificationRequestAccept] {
+    override def write(obj: VerificationRequestAccept): JsValue = JsObject(
+      "ast_id" -> JsNumber(obj.ast_id.id),
+      "id" -> JsNumber(obj.ver_id.id)
+    )
+  })
   implicit val verReqReject_format: RootJsonFormat[VerificationRequestReject] = jsonFormat1(VerificationRequestReject.apply)
   implicit val serverStopConfirmed_format: RootJsonFormat[ServerStopConfirmed] = jsonFormat1(ServerStopConfirmed.apply)
   implicit val jobDiscardAccept_format: RootJsonFormat[JobDiscardAccept] = jsonFormat1(JobDiscardAccept.apply)
@@ -90,18 +102,90 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
     }
   })
 
+  implicit val constantEntry_writer: RootJsonFormat[ConstantEntry] = lift(new RootJsonWriter[ConstantEntry] {
+    override def write(obj: ConstantEntry): JsValue = JsString(obj.value)
+  })
+
+  implicit val applicationEntry_writer: RootJsonFormat[ApplicationEntry] = lift(new RootJsonWriter[ApplicationEntry] {
+    override def write(obj: ApplicationEntry): JsValue = JsObject(
+      "name" -> JsString(obj.name),
+      "args" -> JsArray(obj.arguments.map(_.toJson).toVector)
+    )
+  })
+
+  implicit val modelValue_writer: RootJsonFormat[ValueEntry] = lift(new RootJsonWriter[ValueEntry] {
+    override def write(obj: ValueEntry): JsValue = obj match {
+      case c: ConstantEntry =>
+        JsObject(
+          "type" -> JsString("constant_entry"),
+          "value" -> c.toJson
+        )
+      case a: ApplicationEntry =>
+        JsObject(
+          "type" -> JsString("application_entry"),
+          "value" -> a.toJson
+        )
+    }
+  })
+
+  implicit val mapEntry_writer: RootJsonFormat[MapEntry] = lift(new RootJsonWriter[MapEntry] {
+    override def write(obj: MapEntry): JsValue = JsObject(
+      "type" -> JsString("map_entry"),
+      "cases" -> JsArray(obj.options.map {
+        case (args: Seq[ValueEntry], res: ValueEntry) =>
+          JsObject("args" -> JsArray(args.map(_.toJson).toVector),
+                   "value" -> res.toJson)
+      }.toVector),
+      "default" -> obj.default.toJson
+    )
+  })
+
+  implicit val modelEntry_writer: RootJsonFormat[ModelEntry] = lift(new RootJsonWriter[ModelEntry] {
+    override def write(obj: ModelEntry): JsValue = obj match {
+      case ve: ValueEntry =>
+        ve.toJson
+      case me: MapEntry =>
+        me.toJson
+    }
+  })
+
+  implicit val model_writer: RootJsonFormat[Model] = lift(new RootJsonWriter[Model] {
+    override def write(obj: Model): JsValue =
+      JsObject(obj.entries.map { case (k: String, v: ModelEntry) => (k, v.toJson) })
+  })
+
+  implicit val counterexample_writer: RootJsonFormat[Counterexample] = lift(new RootJsonWriter[Counterexample] {
+    override def write(obj: Counterexample): JsValue = JsObject("model" -> obj.model.toJson)
+  })
+
   implicit val abstractError_writer: RootJsonFormat[AbstractError] = lift(new RootJsonWriter[AbstractError] {
-    override def write(obj: AbstractError) = JsObject(
-      "tag" -> JsString(obj.fullId),
-      "text" -> JsString(obj.readableMessage),
-      "position" -> (obj.pos match {
-        case src_pos: Position => src_pos.toJson
-        case no_pos => JsString(no_pos.toString)
-      }))
+    override def write(obj: AbstractError): JsValue = {
+      obj match {
+        case e: VerificationError if e.counterexample.isDefined =>
+          JsObject(
+            "tag" -> JsString(obj.fullId),
+            "text" -> JsString(obj.readableMessage),
+            "position" -> (obj.pos match {
+              case src_pos: Position => src_pos.toJson
+              case no_pos => JsString(no_pos.toString)
+            }),
+            "cached" -> JsBoolean(obj.cached),
+            "counterexample" -> e.counterexample.get.toJson)
+        case _ =>
+          JsObject(
+            "tag" -> JsString(obj.fullId),
+            "text" -> JsString(obj.readableMessage),
+            "position" -> (obj.pos match {
+              case src_pos: Position => src_pos.toJson
+              case no_pos => JsString(no_pos.toString)
+            }),
+            "cached" -> JsBoolean(obj.cached))
+      }
+    }
   })
 
   implicit val failure_writer: RootJsonFormat[Failure] = lift(new RootJsonWriter[Failure] {
-    override def write(obj: Failure) =
+    override def write(obj: Failure): JsObject =
       JsObject(
         "type" -> JsString("error"),
         "errors" -> JsArray(obj.errors.map(_.toJson).toVector))
@@ -124,11 +208,36 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
       "cached" -> obj.cached.toJson)
   })
 
+  implicit val astConstructionMessage_writer = lift(new RootJsonWriter[AstConstructionResultMessage] {
+    override def write(obj: AstConstructionResultMessage): JsValue = JsObject(
+      "status" -> (obj match {
+        case _: AstConstructionSuccessMessage =>
+          JsString("success")
+        case _: AstConstructionFailureMessage =>
+          JsString("failure")
+      }),
+      "details" -> (obj match {
+        case succ: AstConstructionSuccessMessage =>
+          succ.toJson
+        case fail: AstConstructionFailureMessage =>
+          fail.toJson
+      }))
+  })
+
+  implicit val astConstructionSuccess_writer: RootJsonFormat[AstConstructionSuccessMessage] = lift(new RootJsonWriter[AstConstructionSuccessMessage] {
+    override def write(obj: AstConstructionSuccessMessage): JsValue = JsObject(
+      "time" -> obj.astConstructionTime.toJson)
+  })
+
+  implicit val astConstructionFailure_writer: RootJsonFormat[AstConstructionFailureMessage] = lift(new RootJsonWriter[AstConstructionFailureMessage] {
+    override def write(obj: AstConstructionFailureMessage): JsValue = JsObject(
+      "time" -> obj.astConstructionTime.toJson,
+      "result" -> obj.result.toJson)
+  })
+
   implicit val overallSuccessMessage_writer: RootJsonFormat[OverallSuccessMessage] = lift(new RootJsonWriter[OverallSuccessMessage] {
-    override def write(obj: OverallSuccessMessage): JsObject = {
-      JsObject(
-        "time" -> obj.verificationTime.toJson)
-    }
+    override def write(obj: OverallSuccessMessage): JsObject = JsObject(
+      "time" -> obj.verificationTime.toJson)
   })
 
   implicit val overallFailureMessage_writer: RootJsonFormat[OverallFailureMessage] = lift(new RootJsonWriter[OverallFailureMessage] {
@@ -208,7 +317,8 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
   })
 
   implicit val programDefinitionsReport_writer: RootJsonFormat[ProgramDefinitionsReport] = lift(new RootJsonWriter[ProgramDefinitionsReport] {
-    override def write(obj: ProgramDefinitionsReport) = JsObject("definitions" -> JsArray(obj.definitions.map(_.toJson).toVector))
+    override def write(obj: ProgramDefinitionsReport) = JsObject(
+      "definitions" -> JsArray(obj.definitions.map(_.toJson).toVector))
   })
 
   implicit val symbExLogReport_writer: RootJsonFormat[ExecutionTraceReport] = lift(new RootJsonWriter[ExecutionTraceReport] {
@@ -282,6 +392,7 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
     override def write(obj: Message): JsValue = JsObject(
       "msg_type" -> JsString(obj.name),
       "msg_body" -> (obj match {
+        case p: AstConstructionResultMessage => p.toJson
         case a: VerificationResultMessage => a.toJson
         case s: StatisticsReport => s.toJson
         case o: ProgramOutlineReport => o.toJson
diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
new file mode 100644
index 0000000..adb4a72
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
@@ -0,0 +1,54 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+/** This file contains custom LSP commands.
+  *
+  * There exists a similar file in the Viper IDE client, called 'ViperProtocol.ts', that should
+  * contain the same set of commands. The set of commands in both files should be kept in sync.
+  * */
+
+object C2S_Commands {
+  final val RequestBackendNames = "RequestBackendNames"
+  final val Dispose = "Dispose"
+  final val Verify = "Verify"
+  final val StopVerification = "StopVerification"
+  final val ShowHeap = "ShowHeap"
+  final val StartBackend = "StartBackend"
+  final val StopBackend = "StopBackend"
+  final val SwapBackend = "SwapBackend"
+  final val GetExecutionTrace = "GetExecutionTrace"
+  final val RemoveDiagnostics = "RemoveDiagnostics"
+  final val UpdateViperTools = "UpdateViperTools"
+  final val GetViperFileEndings = "GetViperFileEndings"
+  final val ViperUpdateComplete = "ViperUpdateComplete"
+  final val FlushCache = "FlushCache"
+  final val GetIdentifier = "GetIdentifier"
+
+}
+
+object S2C_Commands {
+  final val BackendChange = "BackendChange"
+  final val CheckIfSettingsVersionsSpecified = "CheckIfSettingsVersionsSpecified"
+  final val SettingsChecked = "SettingsChecked"
+  final val RequestRequiredVersion = "RequestRequiredVersion"
+  final val StateChange = "StateChange"
+  final val Log = "Log"
+  final val Error = "Error"
+  final val ToLogFile = "ToLogFile"
+  final val Hint = "Hint"
+  final val Progress = "Progress"
+  final val FileOpened = "FileOpened"
+  final val FileClosed = "FileClosed"
+  final val VerificationNotStarted = "VerificationNotStarted"
+  final val StopDebugging = "StopDebugging"
+  final val BackendReady = "BackendReady"
+  final val StepsAsDecorationOptions = "StepsAsDecorationOptions"
+  final val HeapGraph = "HeapGraph"
+  final val UnhandledViperServerMessageType = "UnhandledViperServerMessageType"
+  final val BackendStarted = "BackendStarted"
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/Common.scala b/src/main/scala/viper/server/frontends/lsp/Common.scala
new file mode 100644
index 0000000..02f88e3
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/Common.scala
@@ -0,0 +1,72 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import java.net.URI
+import java.nio.file.{Path, Paths}
+import java.util.concurrent.CompletableFuture
+
+import org.eclipse.lsp4j.Position
+
+
+object Common {
+  var viperFileEndings: Array[String] = Array("vpr", "sil")
+
+  def uriFromString(uri: String): URI = {
+    URI.create(uri)
+  }
+
+  def uriToPath(uri: URI): Path = {
+    Paths.get(uri)
+  }
+
+  def filenameFromUri(uri: String): String = {
+    Paths.get(uri).getFileName.toString
+  }
+
+  def refreshEndings(): CompletableFuture[Void] = {
+    Coordinator.client.requestVprFileEndings().thenAccept((s: Array[String]) => {
+      viperFileEndings = s
+    }).exceptionally(e => {
+      Log.debug(s"GetViperFileEndings request was rejected by the client: $e")
+      null
+    })
+  }
+
+  def isViperSourceFile(uri: String): CompletableFuture[Boolean] = {
+    def areEndingsDefined: Boolean = viperFileEndings != null && viperFileEndings.nonEmpty
+    if (areEndingsDefined) {
+      val endingMatches = viperFileEndings.exists(ending => uri.endsWith(ending))
+      CompletableFuture.completedFuture(endingMatches)
+    } else { // need to refresh endings and then compare
+      Log.debug("Refreshing the viper file endings.")
+      refreshEndings().thenApply(a => {
+        if (areEndingsDefined) {
+          println("Endings are defined!")
+          viperFileEndings.foreach(s => s.drop(1))
+          viperFileEndings.exists(ending => uri.endsWith(ending))
+        } else {
+          println("Endings not are defined!")
+          false
+        }
+      })
+    }
+  }
+
+  def comparePosition(a: Position, b: Position): Int = {
+    if (a == null && b == null) return 0
+    if (a != null) return -1
+    if (b != null) return 1
+    if (a.getLine < b.getLine || (a.getLine == b.getLine && a.getCharacter < b.getCharacter)) {
+      -1
+    } else if (a.getLine == b.getLine && a.getCharacter == b.getCharacter) {
+      0
+    } else {
+      1
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/Coordinator.scala b/src/main/scala/viper/server/frontends/lsp/Coordinator.scala
new file mode 100644
index 0000000..faa517d
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/Coordinator.scala
@@ -0,0 +1,70 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import java.util.concurrent.CompletableFuture
+
+import scala.collection.mutable
+
+object Coordinator {
+  var port: Int = _
+  var url: String = _
+  var client: IdeLanguageClient = _
+
+  var files = mutable.Map.empty[String, FileManager]    //Each file is managed individually.
+  var verifier: ViperServerService = null   // verification enginge. Set once on start.
+  var backend: BackendProperties = null     // Backend the engine uses. Can be swapped throughout
+
+  def getAddress: String = url + ":" + port
+
+  /** Checks if verification can be started for a given file.
+    *
+    * Informs client differently depending on whether or not verification attempt was triggered manually
+    * */
+  def canVerificationBeStarted(uri: String, manuallyTriggered: Boolean): Boolean = {
+    //check if there is already a verification task for that file
+    if(files.get(uri).isEmpty){
+      Log.debug("No verification task found for file: " + uri)
+      false
+    } else if (!verifier.is_ready) {
+      if (manuallyTriggered) {
+        Log.hint("The verification backend is not ready yet")
+      }
+      Log.debug("The verification backend is not ready yet")
+      false
+    } else {
+      true
+    }
+  }
+
+  /** Stops all running verifications.
+    *
+    * Returns a CF that is successfully completed if all running verifications were stopped
+    * successfully. Otherwise, a failed CF is returned
+    * */
+  def stopAllRunningVerifications(): CompletableFuture[Void] = {
+    if (files.nonEmpty) {
+      val promises = files.values.map(task => task.abortVerification()).toSeq
+      CompletableFuture.allOf(promises:_*)
+    } else {
+      CompletableFuture.completedFuture(null)
+    }
+  }
+
+  /** Notifies the client about a state change
+    *
+    * If state change is related to a particular file, its manager's state is also updated.
+    * */
+  def sendStateChangeNotification(params: StateChangeParams, task: Option[FileManager]): Unit = {
+    if (task.isDefined) task.get.state = VerificationState.apply(params.newState)
+    try {
+      client.notifyStateChanged(params)
+    } catch {
+      case e: Throwable => Log.debug("Error while changing state: ", e)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
new file mode 100644
index 0000000..7bfb4f9
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -0,0 +1,219 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import org.eclipse.lsp4j.{Diagnostic, Position, Range}
+
+object VerificationSuccess extends Enumeration {
+  type VerificationSuccess = Value
+
+  val NA, Success, ParsingFailed, TypecheckingFailed = Value
+  val VerificationFailed = Value  // Manually aborted verification
+  val Aborted = Value             // Caused by internal error
+  val Error = Value               // Caused by verification taking too long
+  val Timeout = Value
+}
+import viper.server.frontends.lsp.VerificationSuccess._
+
+object VerificationState extends Enumeration {
+  type VerificationState = Value
+
+  val Stopped, Starting = Value
+  val VerificationRunning, VerificationPrintingHelp, VerificationReporting = Value
+  val PostProcessing = Value
+  val Ready = Value
+  val Stopping = Value
+  val Stage = Value
+}
+
+object SettingsErrorType extends Enumeration {
+  type SettingsErrorType = Value
+
+  val Error, Warning = Value
+}
+import viper.server.frontends.lsp.SettingsErrorType._
+
+object LogLevel extends Enumeration {
+  type LogLevel = Value
+
+  val None = Value // No output
+  val Default = Value // Only verification specific output
+  val Info = Value // Some info about internal state, critical errors
+  val Verbose = Value // More info about internal state
+  val Debug = Value // Detailed information about internal state, non critical errors
+  val LowLevelDebug = Value // all output of used tools is written to logFile, some of it also to the console
+}
+
+object BackendOutputType {
+  val Start = "Start"
+  val End = "End"
+  val VerificationStart = "VerificationStart"
+  val MethodVerified = "MethodVerified"
+  val FunctionVerified = "FunctionVerified"
+  val PredicateVerified = "PredicateVerified"
+  val Error = "Error"
+  val Outline = "Outline"
+  val Definitions = "Definitions"
+  val Success = "Success"
+  val Stopped = "Stopped"
+}
+
+case class ProgressReport (
+              domain: String,
+              current: Double,
+              total: Double,
+              progress: Double,
+              postfix: Double)
+
+case class BackendProperties(
+              name: String,
+              backend_type: String,
+              paths: Array[String] = null,
+              engine: String = "Viper",
+              timeout: Int = 5000,
+              stages: Array[Stage] = null,
+              stoppingTimeout: Int = 5000,
+              version: String = null)
+
+case class VerifyRequest (
+              uri: String,                  // file to verify
+              manuallyTriggered: Boolean,   // was the verification triggered manually
+              workspace: String)            // the path to the open workspace folder
+
+case class SettingsError (errorType: SettingsErrorType, msg: String)
+
+case class Stage(
+              name: String,      //The per backend unique name of this stage
+              isVerification: Boolean,       //Enable if this stage is describing a verification
+              mainMethod: String,      //The method to invoke when staring the stage
+              customArguments: String,       //the commandline arguments for the java engine
+              onParsingError: String,      //The name of the stage to start in case of a parsing error
+              onTypeCheckingError: String,       //The name of the stage to start in case of a type checking error
+              onVerificationError: String,       //The name of the stage to start in case of a verification error
+              onSuccess: String)       //The name of the stage to start in case of a success
+
+case class PlatformDependentPath (
+              windows: Option[String],
+              mac: Option[String],
+              linux: Option[String])
+
+case class PlatformDependentURL (
+              windows: Option[String],
+              mac: Option[String],
+              linux: Option[String])
+
+// scope == null means global scope
+case class Definition(definition_type: String, name: String, code_location: Position, scope: Range)
+
+case class BackendOutput(
+              typ: String,
+              name: String = null,
+              backendType: String = null,
+              nofMethods: Int = -1,
+              nofPredicates: Int = -1,
+              nofFunctions: Int = -1,  //for End
+              time: Long = -1,  //for Error
+              file: String = null,
+              errors: Array[Error] = null,  //for Outline
+              definitions: Array[Definition] = null)
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//////              SETTINGS                                                                 ///////
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+case class Hint(msg: String, showButton1: Boolean, showButton2: Boolean)
+
+case class BackendReadyParams(
+              name: String,  //name of the backend ready to use
+              restarted: Boolean,
+              isViperServer: Boolean)
+
+case class BackendStartedParams(
+              name: String,
+              forceRestart: Boolean = false,
+              isViperServer: Boolean = true)
+
+case class StateChangeParams(
+              newState: Int,
+              progress: Double = -1,
+              success: Int = NA.id,
+              verificationCompleted: Double = -1,
+              manuallyTriggered: Double = -1,
+              filename: String = null,
+              backendName: String = null,
+              time: Double = -1,
+              nofErrors: Double = -1,
+              verificationNeeded: Double = -1,
+              uri: String = null,
+              stage: String = null,
+              error: String = null,
+              diagnostics: Array[Diagnostic] = null)
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//////              SETTINGS                                                                 ///////
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+case class ViperServerSettings(
+                                serverJars: Array[String],     // Locator to the ViperServer jars
+                                customArguments: String,       // custom commandLine arguments
+                                backendSpecificCache: Boolean, // it set to false, cached errors are reused across backends
+                                disableCaching: Boolean,    // disable the caching mechanism
+                                timeout: Int,               // After timeout ms the startup of the viperServer is expected to have failed and thus aborted
+                                viperServerPolicy: String,  // Specifies whether ViperServer should be started by the IDE or whether the IDE should attach to an existing instance of ViperServer. Possible values: "attach", "create".
+                                viperServerAddress: String, // Specifies the address part of the URL that ViperServer is running on.
+                                viperServerPort: Int,       // Specifies the port part of the URL that ViperServer is running on. Only needed if viperServerPolicy is set to 'attach'.
+                                version: String ) extends VersionedSettings
+
+case class Versions(
+                     viperServerSettingsVersion: String,
+                     backendSettingsVersion: String,
+                     pathSettingsVersion: String,
+                     userPreferencesVersion: String,
+                     javaSettingsVersion: String,
+                     advancedFeaturesVersion: String,
+                     defaultSettings: AnyRef,
+                     extensionVersion: String)
+
+case class ViperSettings(
+                          viperServerSettings: ViperServerSettings, // All viperServer related settings
+                          verificationBackends: Array[BackendProperties], // Description of backends
+                          paths: PathSettings, // Used paths
+                          preferences: UserPreferences, // General user preferences
+                          javaSettings: JavaSettings, // Java settings
+                          advancedFeatures: AdvancedFeatureSettings) // Settings for AdvancedFeatures
+
+trait VersionedSettings {
+  val version: String
+}
+
+case class PathSettings(
+                         viperToolsPath: Either[String, PlatformDependentPath],    // Path to the folder containing all the ViperTools
+                         z3Executable: Either[String, PlatformDependentPath],      // The path to the z3 executable
+                         boogieExecutable: Either[String, PlatformDependentPath],  // The path to the boogie executable
+                         version: String) extends VersionedSettings
+
+case class UserPreferences (
+                             autoSave: Boolean,        //Enable automatically saving modified viper files
+                             logLevel: Int,            //Verbosity of the output, all output is written to the logFile, regardless of the logLevel
+                             autoVerifyAfterBackendChange: Boolean,      //Reverify the open viper file upon backend change.
+                             showProgress: Boolean,   //Display the verification progress in the status bar. Only useful if the backend supports progress reporting.
+                             viperToolsProvider: Either[String, PlatformDependentURL], //The URL for downloading the ViperTools from
+                             version: String) extends VersionedSettings
+
+//The arguments used for all java invocations
+case class JavaSettings(customArguments: String, version: String) extends VersionedSettings
+
+case class AdvancedFeatureSettings(
+                                    enabled: Boolean,         //Enable heap visualization, stepwise debugging and execution path visualization
+                                    showSymbolicState: Boolean,     //Show the symbolic values in the heap visualization. If disabled, the symbolic values are only shown in the error states.
+                                    darkGraphs: Boolean,      //To get the best visual heap representation, this setting should match with the active theme.
+                                    simpleMode: Boolean,      //Useful for verifying programs. Disable when developing the backend
+                                    showOldState: Boolean,    //Visualize also the oldHeap in the heap preview
+                                    showPartialExecutionTree: Boolean,    //Show the part of the execution tree around the current state in the state visualization
+                                    verificationBufferSize: Int,          //Maximal buffer size for verification in KB
+                                    compareStates: Boolean,
+                                    version: String) extends VersionedSettings
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
new file mode 100644
index 0000000..4bae2f5
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -0,0 +1,327 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import java.net.URI
+import java.nio.file.{Path, Paths}
+import java.util.concurrent.{CompletableFuture => CFuture}
+
+import akka.actor.{Actor, Props}
+import org.eclipse.lsp4j.{Diagnostic, DiagnosticSeverity, Location, Position, PublishDiagnosticsParams, Range, SymbolInformation, SymbolKind}
+import viper.server.frontends.lsp
+import viper.server.frontends.lsp.VerificationState._
+import viper.server.frontends.lsp.VerificationSuccess._
+import viper.server.vsi.VerJobId
+import viper.silver.ast.{Domain, Field, Function, Method, Predicate, SourcePosition}
+import viper.silver.reporter._
+
+import scala.collection.JavaConverters._
+import scala.collection.mutable.ArrayBuffer
+
+class FileManager(file_uri: String) {
+  // File information
+  var uri: URI = URI.create(file_uri)
+  var path: Path = Paths.get(uri)
+  var filename: String = path.getFileName.toString
+  var lastSuccess: VerificationSuccess = NA
+  var internalErrorMessage: String = ""
+
+  //state specific to one verification
+  var is_aborting: Boolean = false
+  var is_verifying: Boolean = false
+  var global_failure: Boolean = false
+  var state: VerificationState = Stopped
+  var manuallyTriggered: Boolean = _
+
+  //verification results
+  var jid: Int = -1
+  var time: Long = 0
+  var diagnostics: ArrayBuffer[Diagnostic] = _
+  var parsingCompleted: Boolean = false
+  var typeCheckingCompleted: Boolean = false
+  var backendType: String = _
+  var progress: Progress = _
+  var symbolInformation: ArrayBuffer[SymbolInformation] = ArrayBuffer()
+  var definitions: ArrayBuffer[lsp.Definition] = ArrayBuffer()
+
+  private var lines: Array[String] = Array()
+  private var wrongFormat: Boolean = false
+  private var partialData: String = ""
+
+  def resetDiagnostics(): Unit = {
+    diagnostics = ArrayBuffer()
+    val diagnosticParams = new PublishDiagnosticsParams()
+    diagnosticParams.setUri(file_uri)
+    diagnosticParams.setDiagnostics(diagnostics.asJava)
+    Coordinator.client.publishDiagnostics(diagnosticParams)
+  }
+
+  def resetLastSuccess(): Unit = {
+    lastSuccess = NA
+  }
+
+  def prepareVerification(): Unit = {
+    is_verifying = true
+    is_aborting = false
+    state = Stopped
+    lines = Array()
+    wrongFormat = false
+    if (partialData.length > 0) {
+      Log.debug("Some unparsed output was detected:\n" + partialData)
+      partialData = ""
+    }
+    time = 0
+    resetDiagnostics()
+    parsingCompleted = true
+    typeCheckingCompleted = true
+    internalErrorMessage = ""
+  }
+
+  def abortVerification(): CFuture[Void] = {
+    if (!is_verifying) {
+      return CFuture.completedFuture(null)
+    }
+    Log.info("Aborting running verification.")
+    is_aborting = true
+    Coordinator.verifier.stopVerification(VerJobId(jid)).thenAccept(_ => {
+      is_verifying = false
+      lastSuccess = Aborted
+    }).exceptionally(e => {
+      Log.debug("Error aborting verification of " + filename + ": " + e)
+      null
+    })
+  }
+
+
+  def getVerificationCommand(fileToVerify: String): Option[String] = {
+    try {
+      val args: String = getViperBackendClassName() + s" $fileToVerify"
+      Log.debug(args)
+      Some(args)
+    } catch {
+      case e: Throwable =>
+        Log.debug("Error finding backend: ", e)
+        None
+    }
+  }
+
+  def getViperBackendClassName(): String = {
+    Coordinator.backend.backend_type match {
+      case "Silicon" => "silicon"
+      case "Carbon" => "carbon"
+      case _ => throw new Error(s"Invalid verification backend value. " +
+        s"Possible values are [silicon | carbon | other] " +
+        s"but found ${Coordinator.backend}")
+    }
+  }
+
+  def startVerification(manuallyTriggered: Boolean): Boolean = {
+    prepareVerification()
+    this.manuallyTriggered = manuallyTriggered
+
+    Log.info(s"verify $filename")
+    Log.info(s"${Coordinator.backend.name} verification started")
+
+    val params = StateChangeParams(VerificationRunning.id, filename = filename)
+    println("state change params created")
+    Coordinator.sendStateChangeNotification(params, Some(this))
+    println("state change params sent")
+
+    val command = getVerificationCommand(path.toString).getOrElse(return false)
+    Log.info(s"Successfully generated command: $command")
+    val handle = Coordinator.verifier.verify(command)
+    jid = handle.id
+    if (jid >= 0) {
+      Coordinator.verifier.startStreaming(handle, RelayActor.props(this))
+      true
+    } else {
+      false
+    }
+  }
+
+  object RelayActor {
+    def props(task: FileManager): Props = Props(new RelayActor(task))
+  }
+
+  class RelayActor(task: FileManager) extends Actor {
+
+    override def receive: PartialFunction[Any, Unit] = {
+      case ProgramOutlineReport(members) =>
+        symbolInformation = ArrayBuffer()
+        members.foreach(m => {
+          val member_start = m.pos.asInstanceOf[SourcePosition].start
+          val member_end = m.pos.asInstanceOf[SourcePosition].end.getOrElse(member_start)
+          val range_start = new Position(member_start.line - 1, member_start.column - 1)
+          val range_end = new Position(member_end.line - 1, member_end.column - 1)
+          val range = new Range(range_start, range_end)
+          val location: Location = new Location(file_uri, range)
+
+          val kind = m match {
+            case _: Method => SymbolKind.Method
+            case _: Function => SymbolKind.Function
+            case _: Predicate => SymbolKind.Interface
+            case _: Field => SymbolKind.Field
+            case _: Domain => SymbolKind.Class
+            case _ => SymbolKind.Enum
+          }
+          val info: SymbolInformation = new SymbolInformation(m.name, kind, location)
+          symbolInformation.append(info)
+        })
+      case ProgramDefinitionsReport(defs) =>
+        definitions = ArrayBuffer()
+        defs.foreach(d => {
+          val start = d.scope match {
+            case Some(s) => new Position(s.start.line - 1, s.start.column - 1)
+            case None => null
+          }
+          val end = d.scope match {
+            case Some(s) if s.end.isDefined => new Position(s.end.get.line - 1, s.end.get.column - 1)
+            case None => null
+          }
+          val range: Range = if(start != null && end != null) {
+            new Range(start, end)
+          } else {
+            null
+          }
+          val sourcePos = d.location.asInstanceOf[viper.silver.ast.SourcePosition]
+          val location: Position = new Position(sourcePos.start.line - 1, sourcePos.start.column - 1)
+          val definition: lsp.Definition = lsp.Definition(d.typ, d.name, location, range)
+          definitions.append(definition)
+        })
+    case StatisticsReport(m, f, p, _, _) =>
+      progress = new Progress(p, f, m)
+      val params = StateChangeParams(VerificationRunning.id, progress = 0, filename = filename)
+      Coordinator.sendStateChangeNotification(params, Some(task))
+    case EntitySuccessMessage(_, concerning, _, _) =>
+      if (progress == null) {
+        Log.debug("The backend must send a VerificationStart message before the ...Verified message.")
+      } else {
+        val output = BackendOutput(BackendOutputType.FunctionVerified, name = concerning.name)
+        progress.updateProgress(output)
+        val progressPercentage = progress.toPercent
+        val params = StateChangeParams(VerificationRunning.id, progress = progressPercentage, filename = filename)
+        Coordinator.sendStateChangeNotification(params, Some(task))
+      }
+    case EntityFailureMessage(_, _, _, res, _) =>
+      res.errors.foreach(err => {
+        if (err.fullId != null && err.fullId == "typechecker.error") {
+          typeCheckingCompleted = false
+        }
+        else if (err.fullId != null && err.fullId == "parser.error") {
+          parsingCompleted = false
+          typeCheckingCompleted = false
+        }
+        val err_start = err.pos.asInstanceOf[SourcePosition].start
+        val err_end = err.pos.asInstanceOf[SourcePosition].end
+        val start_pos = new Position(err_start.line - 1, err_start.column - 1)
+        val end_pos = if(err_end.isDefined) {
+          new Position(err_end.get.line - 1, err_end.get.column - 1)
+        } else {
+          null
+        }
+        val range = new Range(start_pos, end_pos)
+        Log.toLogFile(s"Error: [${Coordinator.backend.name}] " +
+          s"${if(err.fullId != null) "[" + err.fullId + "] " else ""}" +
+          s"${range.getStart.getLine + 1}:${range.getStart.getCharacter + 1} ${err.readableMessage}s")
+
+
+        val cachFlag: String = if(err.cached) "(cached)" else ""
+        val diag = new Diagnostic(range, err.readableMessage + cachFlag, DiagnosticSeverity.Error, "")
+        diagnostics.append(diag)
+
+        val params = StateChangeParams(
+                      VerificationRunning.id, filename = filename, nofErrors = diagnostics.length,
+                      uri = file_uri, diagnostics = diagnostics.toArray)
+        Coordinator.sendStateChangeNotification(params, Some(task))
+      })
+    case OverallSuccessMessage(_, verificationTime) =>
+      state = VerificationReporting
+      time = verificationTime
+      completionHandler(0)
+    case OverallFailureMessage(_, verificationTime, _) =>
+      state = VerificationReporting
+      time = verificationTime
+      completionHandler(0)
+    case m: Message => Coordinator.client.notifyUnhandledViperServerMessage(m.toString, 2)
+    case e: Throwable =>
+    }
+  }
+
+  private def determineSuccess(code: Int): VerificationSuccess = {
+    if (diagnostics.isEmpty && code == 0) {
+      VerificationSuccess.Success
+    } else if (diagnostics.nonEmpty) {
+      //use tag and backend trace as indicators for completed parsing
+      if (!parsingCompleted) {
+        ParsingFailed
+      } else if (parsingCompleted && !typeCheckingCompleted) {
+        TypecheckingFailed
+      } else {
+        VerificationFailed
+      }
+    } else if (is_aborting) {
+      Aborted
+    } else {
+      Error
+    }
+  }
+
+  private def completionHandler(code: Int) {
+    try {
+      Log.debug(s"completionHandler is called with code ${code}")
+      if (is_aborting) {
+        is_verifying = false
+        return
+      }
+      var params: StateChangeParams = null
+      var success = NA
+
+      val isVerifyingStage = true
+
+      //do we need to start a followUp Stage?
+      if (isVerifyingStage) {
+        if (partialData != null && partialData.length > 0) {
+          Log.debug("Some unparsed output was detected:\n" + partialData)
+          partialData = ""
+        }
+
+        //inform client about postProcessing
+        success = determineSuccess(code)
+        params = StateChangeParams(PostProcessing.id, filename = filename)
+        Coordinator.sendStateChangeNotification(params, Some(this));
+
+        //notify client about outcome of verification
+        val mt = if(this.manuallyTriggered) 1 else 0
+        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+          filename = filename, nofErrors = diagnostics.length, time = time.toDouble,
+          verificationCompleted = 1, uri = file_uri, error = internalErrorMessage)
+        Coordinator.sendStateChangeNotification(params, Some(this))
+
+        if (code != 0 && code != 1 && code != 899) {
+          Log.debug("Verification Backend Terminated Abnormally: with code " + code)
+        }
+      } else {
+        success = Success
+        val mt = if(this.manuallyTriggered) 1 else 0
+        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+          filename = filename, nofErrors = 0, time = time.toDouble,
+          verificationCompleted = 0, uri = file_uri, error = internalErrorMessage)
+        Coordinator.sendStateChangeNotification(params, Some(this))
+      }
+
+      //reset for next verification
+      lastSuccess = success
+      time = 0
+      is_verifying = false
+    } catch {
+      case e: Throwable =>
+        is_verifying = false
+        Coordinator.client.notifyVerificationNotStarted(file_uri)
+        Log.debug("Error handling verification completion: ", e)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala
new file mode 100644
index 0000000..ff3fc9f
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala
@@ -0,0 +1,55 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import java.util.concurrent.CompletableFuture
+
+import org.eclipse.lsp4j.Position
+import org.eclipse.lsp4j.jsonrpc.services._
+import org.eclipse.lsp4j.services.LanguageClient
+
+
+trait IdeLanguageClient extends LanguageClient {
+  @JsonNotification(S2C_Commands.FileOpened)
+  def notifyFileOpened(uri: String): Unit
+
+  @JsonNotification(S2C_Commands.FileClosed)
+  def notifyFileClosed(uri: String): Unit
+
+  @JsonRequest(C2S_Commands.GetIdentifier)
+  def requestIdentifier(pos: Position): CompletableFuture[String]
+
+  @JsonRequest(C2S_Commands.GetViperFileEndings)
+  def requestVprFileEndings(): CompletableFuture[Array[String]]
+
+  @JsonNotification(S2C_Commands.BackendReady)
+  def notifyBackendReady(param: BackendReadyParams): Unit
+
+  @JsonNotification(S2C_Commands.BackendStarted)
+  def notifyBackendStarted(params: BackendStartedParams): Unit
+
+  @JsonNotification(S2C_Commands.BackendChange)
+  def notifyBackendChanged(name: String): Unit
+
+  @JsonNotification(S2C_Commands.Progress)
+  def notifyProgress(progress: ProgressReport, logLevel: Int): Unit
+
+  @JsonNotification(S2C_Commands.Log)
+  def notifyLog(msg: String, logLevel: Int): Unit
+
+  @JsonNotification(S2C_Commands.Hint)
+  def notifyHint(msg: String, hint: Hint): Unit
+
+  @JsonNotification(S2C_Commands.UnhandledViperServerMessageType)
+  def notifyUnhandledViperServerMessage(msg: String, logLevel: Int): Unit
+
+  @JsonNotification(S2C_Commands.VerificationNotStarted)
+  def notifyVerificationNotStarted(uri: String): Unit
+
+  @JsonNotification(S2C_Commands.StateChange)
+  def notifyStateChanged(params: StateChangeParams): Unit
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLog.scala b/src/main/scala/viper/server/frontends/lsp/IdeLog.scala
new file mode 100644
index 0000000..1fdbf3e
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/IdeLog.scala
@@ -0,0 +1,54 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import viper.server.frontends.lsp.LogLevel._
+
+object Log {
+
+  def log(message: String, logLevel: LogLevel) = {
+    require(message != null && logLevel != null)
+    Coordinator.client.notifyLog(message, logLevel.id)
+  }
+
+  def toLogFile(message: String) = log(message, Default)
+
+  def debug(message: String) = log(message, Debug)
+
+  def debug(message: String, error: Throwable) = log(s"$message $error", Debug)
+
+  def info(message: String) = log(message, Info)
+
+  def lowLevel(message: String) = log(message, LowLevelDebug)
+
+  private var lastProgress: Double = _
+
+  def startProgress() = {
+    lastProgress = 0
+  }
+
+  def progress(domain: String, cur: Double, len: Double, logLevel: LogLevel) = {
+    val progress = 100.0 * cur / len
+    if (Math.floor(progress) > lastProgress) {
+      lastProgress = progress
+      val data = ProgressReport(domain, cur, len, progress, Double.NaN)
+      Coordinator.client.notifyProgress(data, logLevel.id)
+    }
+  }
+
+  def logWithOrigin(origin: String, message: String, logLevel: LogLevel) = {
+    if (message != null) {
+      val indicator: String = if (logLevel >= Debug) "[" + origin + "]: " else ""
+      val msg_with_origin: String = indicator + message
+      log(msg_with_origin, logLevel)
+    }
+  }
+
+  def hint(message: String, showSettingsButton: Boolean = false, showViperToolsUpdateButton: Boolean = false) = {
+    Coordinator.client.notifyHint(S2C_Commands.Hint, Hint(message, showSettingsButton, showViperToolsUpdateButton ))
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/Progress.scala b/src/main/scala/viper/server/frontends/lsp/Progress.scala
new file mode 100644
index 0000000..b0a1466
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/Progress.scala
@@ -0,0 +1,32 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+class Progress(val nofPredicates: Int, val nofFunctions: Int, val nofMethods: Int) {
+
+  var currentFunctions = 0;
+  var currentMethods = 0;
+  var currentPredicates = 0;
+
+  def updateProgress(output: BackendOutput) = {
+    try {
+      output.typ match {
+        case BackendOutputType.MethodVerified => currentMethods += 1
+        case BackendOutputType.FunctionVerified => currentFunctions += 1
+        case BackendOutputType.PredicateVerified => currentPredicates += 1
+      }
+    } catch {
+      case e: Throwable => Log.debug("Error updating progress: ", e);
+    }
+  }
+
+  def toPercent: Double = {
+    val total = nofFunctions + nofMethods + nofPredicates
+    val current = currentFunctions + currentMethods + currentPredicates
+    100 * current / total
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
new file mode 100644
index 0000000..52f4dc0
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -0,0 +1,282 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import java.util.concurrent.{CompletableFuture => CFuture}
+
+import org.eclipse.lsp4j.jsonrpc.services.{JsonNotification, JsonRequest}
+import org.eclipse.lsp4j.services.{LanguageClient, LanguageClientAware}
+import org.eclipse.lsp4j.{DidChangeConfigurationParams, DidChangeTextDocumentParams, DidCloseTextDocumentParams, DidOpenTextDocumentParams, DocumentSymbolParams, InitializeParams, InitializeResult, InitializedParams, Location, Range, ServerCapabilities, SymbolInformation, TextDocumentPositionParams, TextDocumentSyncKind}
+import viper.server.frontends.lsp.LogLevel._
+import viper.server.frontends.lsp.VerificationState._
+
+import scala.collection.mutable.ArrayBuffer
+
+
+
+abstract class StandardReceiver extends LanguageClientAware {
+  var received_shutdown = false
+
+  @JsonRequest("initialize")
+  def onInitialize(params: InitializeParams): CFuture[InitializeResult] = {
+    Log.info("initialize")
+    val capabilities = new ServerCapabilities()
+
+    capabilities.setTextDocumentSync(TextDocumentSyncKind.Full)
+    capabilities.setDefinitionProvider(true)
+    capabilities.setDocumentSymbolProvider(true)
+    CFuture.completedFuture(new InitializeResult(capabilities))
+  }
+
+  @JsonNotification("initialized")
+  def onInitialized(params: InitializedParams): Unit = {
+    Log.info("initialized")
+  }
+
+  @JsonNotification("textDocument/didOpen")
+  def onDidOpenDocument(params: DidOpenTextDocumentParams): Unit = {
+    Log.info("On opening document")
+    try {
+      val uri: String = params.getTextDocument.getUri
+      Common.isViperSourceFile(uri).thenAccept(isViperFile => {
+        if (true) {
+          //notify client
+          Coordinator.client.notifyFileOpened(uri)
+          if (!Coordinator.files.contains(uri)) {
+            //create new task for opened file
+            val manager = new FileManager(uri)
+            Coordinator.files += (uri -> manager)
+          }
+        }
+      })
+    } catch {
+      case e: Throwable => Log.debug("Error handling TextDocument opened", e)
+    }
+  }
+
+  @JsonNotification("workspace/didChangeConfiguration")
+  def onDidChangeConfig(params: DidChangeConfigurationParams): Unit = {
+    Log.info("On config change")
+    try {
+      Log.lowLevel("check if restart needed")
+      if (Coordinator.verifier == null) {
+        Log.info("Change Backend: from 'No Backend' to Silicon")
+        val backend = "Silicon"
+        Coordinator.backend = BackendProperties(name = s"Viper$backend", backend_type = backend)
+        Coordinator.client.notifyBackendStarted(BackendStartedParams(backend))
+      } else {
+        Log.log("No need to restart backend. It is still the same", LogLevel.Debug)
+      }
+    } catch {
+      case e: Throwable => Log.debug("Error handling swap backend request: " + e)
+    }
+  }
+
+  @JsonNotification("textDocument/didChange")
+  def onDidChangeDocument(params: DidChangeTextDocumentParams): Unit = {
+    Log.info("On changing document")
+    val manager_opt = Coordinator.files.get(params.getTextDocument.getUri)
+    val manager: FileManager = manager_opt.getOrElse(return)
+    manager.symbolInformation = ArrayBuffer()
+    manager.definitions = ArrayBuffer()
+  }
+
+  @JsonRequest("textDocument/documentSymbol")
+  def onGetDocumentSymbol(params: DocumentSymbolParams): CFuture[Array[SymbolInformation]] = {
+    Log.info("On getting document symbol")
+    var symbolInfo_list: Array[SymbolInformation] = Array()
+    val manager_opt = Coordinator.files.get(params.getTextDocument.getUri)
+    val manager = manager_opt.getOrElse(return CFuture.completedFuture(symbolInfo_list))
+    symbolInfo_list = manager.symbolInformation.toArray
+    CFuture.completedFuture(symbolInfo_list)
+  }
+
+  @JsonRequest("textDocument/definition")
+  def onGetDefinition(params: TextDocumentPositionParams): CFuture[Location] = {
+    Log.log("Handling definitions request for params: " + params.toString, LogLevel.Debug)
+    val document = params.getTextDocument
+    val pos = params.getPosition
+    val manager_opt = Coordinator.files.get(params.getTextDocument.getUri)
+
+    manager_opt match {
+      case Some(manager) =>
+        Log.log("Found verification task for URI " + document.getUri, LogLevel.LowLevelDebug)
+        Coordinator.client.requestIdentifier(pos).thenApply(word => {
+          Log.log("Got word: " + word, LowLevelDebug)
+          def hasGlobalScope(d: Definition) = d.scope == null
+          def isPosInScope(d: Definition) = hasGlobalScope(d) ||
+            (Common.comparePosition(d.scope.getStart, pos) <= 0 &&
+              Common.comparePosition(d.scope.getEnd, pos) >= 0)
+          val defs_in_scope = manager.definitions.filter(isPosInScope)
+          val matching_def = defs_in_scope.find(d => word == d.name).getOrElse(return null)
+          val def_range = new Range(matching_def.code_location, matching_def.code_location)
+          new Location(document.getUri, def_range)
+        })
+      case None =>
+        // No definition found - maybe it's a keyword.
+        val e = s"Verification task not found for URI ${document.getUri}"
+        Log.debug(e)
+        CFuture.completedFuture({throw new Throwable(e)}) // needs to return some CF.
+    }
+  }
+
+  @JsonNotification("textDocument/didClose")
+  def onDidCloseDocument(params: DidCloseTextDocumentParams): Unit = {
+    Log.info("On closing document")
+    try {
+      val uri = params.getTextDocument.getUri
+      Common.isViperSourceFile(uri).thenAccept(isViperFile => {
+        if (isViperFile) Coordinator.client.notifyFileClosed(uri)
+      })
+    } catch {
+      case _: Throwable => Log.debug("Error handling TextDocument opened")
+    }
+  }
+
+  @JsonRequest(value = "shutdown")
+  def onShutdown(): CFuture[AnyRef] = {
+    Log.debug("shutdown")
+    received_shutdown = true
+    CFuture.completedFuture(null)
+  }
+
+  @JsonNotification(value = "exit")
+  def onExit(): Unit = {
+    Log.debug("exit")
+    Coordinator.verifier.stop()
+    if(received_shutdown) sys.exit(0) else sys.exit(1)
+  }
+}
+
+class CustomReceiver extends StandardReceiver {
+
+  @JsonNotification(S2C_Commands.FileClosed)
+  def onFileClosed(uri: String): Unit = {
+    Log.debug("On closing file")
+    val manager_opt = Coordinator.files.get(uri)
+    val manager = manager_opt.getOrElse(return)
+    manager.resetDiagnostics()
+    Coordinator.files -= uri
+  }
+
+  @JsonRequest(C2S_Commands.RemoveDiagnostics)
+  def onRemoveDiagnostics(uri: String): CFuture[Boolean] = {
+    Log.debug("On removing diagnostics")
+    val manager_opt = Coordinator.files.get(uri)
+    val manager = manager_opt.getOrElse(return CFuture.completedFuture(false))
+    manager.resetDiagnostics()
+    CFuture.completedFuture(true)
+  }
+
+  @JsonRequest("GetLanguageServerUrl")
+  def onGetServerUrl(): CFuture[String] = {
+    Log.debug("On getting server URL")
+    CFuture.completedFuture(Coordinator.getAddress)
+  }
+
+  @JsonNotification(C2S_Commands.StartBackend)
+  def onStartBackend(backend: String): Unit = {
+    Log.debug("On starting ViperServeService")
+    try {
+      if(backend == "Silicon" || backend == "Carbon") {
+          Coordinator.backend = BackendProperties(name = s"Viper$backend", backend_type = backend)
+      } else {
+        throw new Throwable("Unexpected Backend")
+      }
+      Coordinator.verifier = new ViperServerService(Array())
+      Coordinator.verifier.setReady(Coordinator.backend)
+    } catch {
+      case e: Throwable => Log.debug("Error handling swap backend request: " + e)
+    }
+  }
+
+  @JsonNotification(C2S_Commands.SwapBackend)
+  def onSwapBackend(backend: String): Unit = {
+    Log.debug("on swapping backend")
+    try {
+      if(backend == "Silicon" || backend == "Carbon") {
+        Coordinator.backend = BackendProperties(name = s"Viper$backend", backend_type = backend)
+      } else {
+        throw new Throwable("Unexpected Backend")
+      }
+      Coordinator.verifier.is_ready = true
+      val param = BackendReadyParams(backend, false, true)
+      Coordinator.client.notifyBackendReady(param)
+      Log.info("The backend has been swapped and is now ready for verification")
+    } catch {
+      case e: Throwable => Log.debug("Error handling swap backend request: " + e)
+    }
+  }
+
+  @JsonRequest(C2S_Commands.RequestBackendNames)
+  def onGetNames(backendName: String): CFuture[Array[String]] = {
+    Log.debug("on getting backend names")
+    CFuture.completedFuture(Array("Silicon", "Carbon"))
+  }
+
+  @JsonNotification(C2S_Commands.StopBackend)
+  def onBackendStop(backendName: String): Unit= {
+    Log.debug("on stopping backend")
+    Coordinator.verifier.setStopping()
+    Coordinator.verifier.setStopped()
+  }
+
+  @JsonNotification(C2S_Commands.Verify)
+  def onVerify(data: VerifyRequest): Unit = {
+    Log.debug("On verifying")
+    if (Coordinator.canVerificationBeStarted(data.uri, data.manuallyTriggered)) {
+      //stop all other verifications because the backend crashes if multiple verifications are run in parallel
+      Coordinator.stopAllRunningVerifications().thenAccept(_ => {
+        Log.log("start or restart verification", LogLevel.Info)
+
+        val manager = Coordinator.files.getOrElse(data.uri, return)
+        val hasVerificationstarted = manager.startVerification(data.manuallyTriggered)
+
+        Log.log("Verification Started", LogLevel.Info)
+        if (!hasVerificationstarted) {
+          Coordinator.client.notifyVerificationNotStarted(data.uri)
+        }
+      }).exceptionally(_ => {
+        Log.debug("Error handling verify request")
+        Coordinator.client.notifyVerificationNotStarted(data.uri)
+        null //java void
+      })
+    } else {
+      Log.log("The verification cannot be started.", LogLevel.Info)
+      Coordinator.client.notifyVerificationNotStarted(data.uri)
+    }
+  }
+
+  @JsonNotification(C2S_Commands.FlushCache)
+  def onFlushCache(file: String): Unit = {
+    Log.debug("flushing cache...")
+    val file_arg: Option[String] = if(file == null) Option.empty else Some(file)
+    Coordinator.verifier.flushCache(file_arg)
+  }
+
+  @JsonNotification(C2S_Commands.StopVerification)
+  def onStopVerification(uri: String): CFuture[Boolean] = {
+    Log.debug("on stopping verification")
+    try {
+      val manager = Coordinator.files.getOrElse(uri, return CFuture.completedFuture(false))
+        manager.abortVerification().thenApply((success) => {
+          val params = StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = uri)
+          Coordinator.sendStateChangeNotification(params, Some(manager))
+          true
+        })
+    } catch {
+      case e: Throwable =>
+        Log.debug("Error handling stop verification request (critical): " + e);
+        CFuture.completedFuture(false)
+    }
+  }
+
+  override def connect(client: LanguageClient): Unit = {
+    val c = client.asInstanceOf[IdeLanguageClient]
+    Coordinator.client = c
+  }
+}
diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
new file mode 100644
index 0000000..596a0ca
--- /dev/null
+++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
@@ -0,0 +1,160 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.frontends.lsp
+
+import scala.language.postfixOps
+
+import java.util.concurrent.{CompletableFuture => CFuture}
+
+import akka.actor.{PoisonPill, Props}
+import akka.pattern.ask
+import akka.util.Timeout
+import viper.server.core.{ViperBackendConfig, ViperCache, ViperCoreServer}
+import viper.server.frontends.lsp.VerificationState.Stopped
+import viper.server.utility.AstGenerator
+import viper.server.utility.Helpers.getArgListFromArgString
+import viper.server.vsi.VerificationProtocol.StopVerification
+import viper.server.vsi.{VerJobId, VerificationServer}
+import viper.silver.ast.Program
+
+import scala.compat.java8.FutureConverters._
+import scala.concurrent.Future
+import scala.concurrent.duration._
+
+class ViperServerService(args: Array[String]) extends ViperCoreServer(args) with VerificationServer {
+
+  protected var timeout: Int = _
+
+  def isRunningServer: Boolean = isRunning
+
+  var is_ready = false
+
+  def setReady(backend: BackendProperties): Unit = {
+    Coordinator.backend = backend
+    start()
+    is_ready = true
+    val param = BackendReadyParams("Silicon", false, true)
+    Coordinator.client.notifyBackendReady(param)
+    Log.info("The backend is ready for verification")
+  }
+
+  def setStopping(): Unit = {
+    Log.debug("Set Stopping... ")
+    if(isRunning){
+      isRunning = false
+      val params = StateChangeParams(Stopped.id)
+      Coordinator.sendStateChangeNotification(params, None)
+    } else {
+      Log.debug("Server stopped")
+    }
+  }
+  def setStopped(): Unit = {
+    Log.debug("Set Stopped. ")
+    if(isRunning){
+      isRunning = false
+      val params = StateChangeParams(Stopped.id)
+      Coordinator.sendStateChangeNotification(params, None)
+    } else {
+      Log.debug("Server stopped")
+    }
+  }
+
+  def verify(command: String): VerJobId = {
+    Log.debug("Requesting ViperServer to start new job...")
+
+    val arg_list = getArgListFromArgString(command)
+    val file: String = arg_list.last
+    val arg_list_partial = arg_list.dropRight(1)
+
+    // Parse file
+    val astGen = new AstGenerator(_logger.get)
+    var ast_option: Option[Program] = None
+    try {
+      // TODO use AstWorker instead
+      ast_option = astGen.generateViperAst(file)
+    } catch {
+      case _: java.nio.file.NoSuchFileException =>
+        Log.debug("The file for which verification has been requested was not found.")
+        return VerJobId(-1)
+    }
+    val ast = ast_option.getOrElse({
+      Log.debug("The file for which verification has been requested contained syntax errors.")
+      return VerJobId(-1)
+    })
+
+    // prepare backend config
+    val backend = try {
+      ViperBackendConfig(arg_list_partial)
+    } catch {
+      case _: IllegalArgumentException =>
+        logger.get.error(s"Invalid arguments: ${command} " +
+          s"You need to specify the verification backend, e.g., `silicon [args]`")
+        return VerJobId(-1)
+    }
+
+    val jid: VerJobId = verify(file, backend, ast)
+    if (jid.id >= 0) {
+      Log.info(s"Verification process #${jid.id} has successfully started.")
+    } else {
+      Log.debug(s"Could not start verification process. " +
+        s"the maximum number of active verification jobs are currently running (${ver_jobs.MAX_ACTIVE_JOBS}).")
+    }
+    jid
+  }
+
+  def startStreaming(jid: VerJobId, relayActor_props: Props): Unit = {
+    Log.debug("Sending verification request to ViperServer...")
+    val relay_actor = system.actorOf(relayActor_props)
+    streamMessages(jid, relay_actor)
+  }
+
+  def stopVerification(jid: VerJobId): CFuture[Boolean] = {
+    ver_jobs.lookupJob(jid) match {
+      case Some(handle_future) =>
+        handle_future.flatMap(handle => {
+          implicit val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds)
+          val interrupt: Future[String] = (handle.job_actor ? StopVerification).mapTo[String]
+          handle.job_actor ! PoisonPill // the actor played its part.
+          interrupt
+        }).toJava.toCompletableFuture.thenApply(msg => {
+          Log.info(msg)
+          true
+        })
+      case _ =>
+        // Did not find a job with this jid.
+        CFuture.completedFuture({throw new Throwable(s"The verification job #$jid does not exist.")})
+    }
+  }
+
+  def flushCache(filePath: Option[String]): Unit = {
+    filePath match {
+      case Some(file) =>
+        Log.info(s"Requesting ViperServer to flush the cache for $file...")
+        val flushed_file_opt = ViperCache.forgetFile("silicon", file)
+
+        if (flushed_file_opt.isDefined) {
+          Log.debug(s"ViperServer has confirmed that the cache for $file has been flushed.")
+        } else {
+          Log.debug(s"Error while requesting ViperServer to flush the cache for $file: File not found.")
+        }
+      case None =>
+        Log.info("Flush entire cache...")
+        super.flushCache()
+    }
+  }
+
+  def isSupportedType(t: String): Boolean = {
+    if (t == null) {
+      return false
+    }
+    t.toLowerCase() == "carbon" || t.toLowerCase() == "silicon" || t.toLowerCase() == "other"
+  }
+
+  def supportedTypes(): String = {
+    "'carbon', 'silicon', 'other'"
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/utility/AstGenerator.scala b/src/main/scala/viper/server/utility/AstGenerator.scala
index 6e7b339..42e3fcd 100644
--- a/src/main/scala/viper/server/utility/AstGenerator.scala
+++ b/src/main/scala/viper/server/utility/AstGenerator.scala
@@ -6,71 +6,45 @@
 
 package viper.server.utility
 
-import java.nio.file.Paths
+import java.nio.file.NoSuchFileException
 
-import viper.silicon.SiliconFrontend
+import ch.qos.logback.classic.Logger
+import viper.server.utility.Helpers.validateViperFile
 import viper.silver.ast.Program
-import viper.silver.frontend.SilFrontend
-import viper.silver.logger.ViperLogger
-import viper.silver.parser.PProgram
-import viper.silver.reporter.StdIOReporter
+import viper.silver.frontend.{SilFrontend, ViperAstProvider}
+import viper.silver.reporter.{NoopReporter, Reporter}
 
-class AstGenerator (private val _logger: ViperLogger){
-  private val ver_backend: SilFrontend = create_backend()
+class AstGenerator(private val _logger: Logger,
+                   private val _reporter: Reporter = NoopReporter) extends ProgramDefinitionsProvider {
 
   /** Creates a backend that reads and parses the file
     */
-  private def create_backend() : SilFrontend = {
-    _logger.get.info(s"Creating new verification backend.")
-    new SiliconFrontend(StdIOReporter("Parsing Reporter", true), _logger.get)
+  protected override val _frontend: SilFrontend = {
+    _logger.info(s"Creating new AstGenerator instance.")
+    new ViperAstProvider(_reporter)
   }
-
   /** Parses and translates a Viper file into a Viper AST.
     *
-    * Throws an exception when passed an inexistent file!
+    * Throws an exception when passed an non-existent file!
     */
   def generateViperAst(vpr_file_path: String): Option[Program] = {
+
+    if (!validateViperFile(vpr_file_path)) {
+      throw new NoSuchFileException(vpr_file_path)
+    }
+
     val args: Array[String] = Array(vpr_file_path)
-    _logger.get.info(s"Parsing viper file.")
-    ver_backend.setVerifier(ver_backend.createVerifier(args.mkString(" ")))
-    ver_backend.prepare(args.toIndexedSeq)
-    ver_backend.init(ver_backend.verifier)
-    ver_backend.reset(Paths.get(ver_backend.config.file()))
-    val parse_ast = parse()
-    translate(parse_ast)
-  }
+    _logger.info(s"Parsing Viper file ...")
 
-  /** Parses a Viper file
-    */
-  private def parse(): Option[PProgram] = {
-    ver_backend.parsing()
-    if(ver_backend.errors.isEmpty) {
-      _logger.get.info("There was no error while parsing!")
-      Some(ver_backend.parsingResult)
+    _frontend.execute(args)
+    if (_frontend.program.isDefined) {
+      reportProgramStats()
+    }
+    if (_frontend.errors.isEmpty) {
+      Some(_frontend.translationResult)
     } else {
-      _logger.get.error(s"There was some error while parsing: ${ver_backend.errors}")
+      _logger.error(s"An error occurred while translating ${_frontend.errors}")
       None
     }
   }
-
-  /** Translates a Parsed Viper file into a Viper AST
-    */
-  private def translate(parse_ast : Option[PProgram]) : Option[Program] = {
-    if(parse_ast.isDefined){
-      _logger.get.info(s"Translating parsed file.")
-      ver_backend.semanticAnalysis()
-      ver_backend.translation()
-      ver_backend.consistencyCheck()
-      if(ver_backend.errors.isEmpty){
-        _logger.get.info("There was no error while translating!")
-        ver_backend.verifier.stop()
-        return Some(ver_backend.translationResult)
-      } else {
-        _logger.get.error (s"There was some error while translating ${ver_backend.errors}")
-      }
-    }
-    ver_backend.verifier.stop()
-    None
-  }
 }
-
diff --git a/src/main/scala/viper/server/utility/Helpers.scala b/src/main/scala/viper/server/utility/Helpers.scala
new file mode 100644
index 0000000..c4aadf2
--- /dev/null
+++ b/src/main/scala/viper/server/utility/Helpers.scala
@@ -0,0 +1,40 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.utility
+
+import java.io.File
+
+object Helpers {
+  def getArgListFromArgString(arg_str: String): List[String] = {
+    val possibly_quoted_string = raw"""[^\s"']+|"[^"]*"|'[^']*'""".r
+    val quoted_string = """^["'](.*)["']$""".r
+    possibly_quoted_string.findAllIn(arg_str).toList.map {
+      case quoted_string(noqt_a) => noqt_a
+      case a => a
+    }
+  }
+
+  def canonizedFile(some_file_path: String): File = {
+    val f = new File(some_file_path)
+    if (f.isAbsolute) {
+      f
+    } else {
+      java.nio.file.Paths.get(System.getProperty("user.dir"), some_file_path).toFile
+    }
+  }
+
+  def validatePath(path: String): Boolean = {
+    val f = canonizedFile(path)
+    (f.isFile || f.isDirectory) && f.canWrite || f.getParentFile.canWrite
+  }
+
+  def validateViperFile(path: String): Boolean = {
+    val f = canonizedFile(path)
+    f.isFile && f.canWrite
+  }
+
+}
diff --git a/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala
new file mode 100644
index 0000000..25cfa37
--- /dev/null
+++ b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala
@@ -0,0 +1,125 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.utility
+
+import scala.language.postfixOps
+
+import viper.silver.ast.{AbstractSourcePosition, Domain, Field, Function, LocalVarDecl, Method, NamedDomainAxiom, Positioned, Predicate, Program, Scope}
+import viper.silver.frontend.SilFrontend
+import viper.silver.reporter.{Definition, ProgramDefinitionsReport, ProgramOutlineReport, StatisticsReport}
+
+trait ProgramDefinitionsProvider {
+  protected val _frontend: SilFrontend
+
+  def collect(program: Program): List[Definition] = {
+    (program.members.collect {
+      case t: Method =>
+        (Definition(t.name, "Method", t.pos) +: (t.pos match {
+          case p: AbstractSourcePosition =>
+            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) } ++
+              t.formalReturns.map { arg => Definition(arg.name, "Return", arg.pos, Some(p)) }
+          case _ => Seq()
+        })) ++ t.deepCollectInBody {
+          case scope: Scope with Positioned =>
+            scope.pos match {
+              case p: AbstractSourcePosition =>
+                scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
+              case _ => Seq()
+            }
+        }.flatten
+
+      case t: Function =>
+        (Definition(t.name, "Function", t.pos) +: (t.pos match {
+          case p: AbstractSourcePosition =>
+            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) }
+          case _ => Seq()
+        })) ++ (t.body match {
+          case Some(exp) =>
+            exp.deepCollect {
+              case scope:Scope with Positioned =>
+                scope.pos match {
+                  case p: AbstractSourcePosition =>
+                    scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
+                  case _ => Seq()
+                }
+            } flatten
+          case _ => Seq()
+        })
+
+      case t: Predicate =>
+        (Definition(t.name, "Predicate", t.pos) +: (t.pos match {
+          case p: AbstractSourcePosition =>
+            t.formalArgs.map { arg => Definition(arg.name, "Argument", arg.pos, Some(p)) }
+          case _ => Seq()
+        })) ++ (t.body match {
+          case Some(exp) =>
+            exp.deepCollect {
+              case scope:Scope with Positioned =>
+                scope.pos match {
+                  case p: AbstractSourcePosition =>
+                    scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
+                  case _ => Seq()
+                }
+            } flatten
+          case _ => Seq()
+        })
+
+      case t: Domain =>
+        (Definition(t.name, "Domain", t.pos) +: (t.pos match {
+          case p: AbstractSourcePosition =>
+            t.functions.flatMap { func =>
+              Definition(func.name, "Function", func.pos, Some(p)) +: (func.pos match {
+                case func_p: AbstractSourcePosition =>
+                  func.formalArgs.map { arg => Definition(if (arg.isInstanceOf[LocalVarDecl]) arg.asInstanceOf[LocalVarDecl].name else "unnamed parameter", "Argument", arg.pos, Some(func_p)) }
+                case _ => Seq()
+              })
+            } ++ t.axioms.flatMap { ax =>
+              Definition(if (ax.isInstanceOf[NamedDomainAxiom]) ax.asInstanceOf[NamedDomainAxiom].name else "", "Axiom", ax.pos, Some(p)) +: (ax.pos match {
+                case ax_p: AbstractSourcePosition =>
+                  ax.exp.deepCollect {
+                    case scope:Scope with Positioned =>
+                      scope.pos match {
+                        case p: AbstractSourcePosition =>
+                          scope.scopedDecls.map { local_decl => Definition(local_decl.name, "Local", local_decl.pos, Some(p)) }
+                        case _ => Seq()
+                      }
+                  } flatten
+                case _ => Seq()
+              }) }
+          case _ => Seq()
+        })) ++ Seq()
+
+      case t: Field =>
+        Seq(Definition(t.name, "Field", t.pos))
+
+    } flatten) toList
+  }
+
+  private def countInstances(p: Program): Map[String, Int] = p.members.groupBy({
+    case m: Method => "method"
+    case fu: Function => "function"
+    case p: Predicate => "predicate"
+    case d: Domain => "domain"
+    case fi: Field => "field"
+    case _ => "other"
+  }).mapValues(_.size).toMap
+
+  def reportProgramStats(): Unit = {
+    val prog = _frontend.program.get
+    val stats = countInstances(prog)
+
+    _frontend.reporter.report(ProgramOutlineReport(prog.members.toList))
+    _frontend.reporter.report(StatisticsReport(
+      stats.getOrElse("method", 0),
+      stats.getOrElse("function", 0),
+      stats.getOrElse("predicate", 0),
+      stats.getOrElse("domain", 0),
+      stats.getOrElse("field", 0)
+    ))
+    _frontend.reporter.report(ProgramDefinitionsReport(collect(prog)))
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/vsi/Cache.scala b/src/main/scala/viper/server/vsi/Cache.scala
index 3ff92a9..77c9c59 100644
--- a/src/main/scala/viper/server/vsi/Cache.scala
+++ b/src/main/scala/viper/server/vsi/Cache.scala
@@ -46,10 +46,10 @@ abstract class Cache {
     * The inner map is referred to as the fileCache. As the name indicates, it stores, for each
     * file, a number of hashes and corresponding cache entries.
     */
-  protected val _cache = MutableMap[String, FileCash]()
+  protected val _cache: MutableMap[String, FileCash] = MutableMap()
   type FileCash = MutableMap[String, List[CacheEntry]]
 
-  protected val _program_cache = MutableMap[Ast, MutableMap[CacheableMember, List[Member]]]()
+  protected val _program_cache: MutableMap[Ast, MutableMap[CacheableMember, List[Member]]] = MutableMap()
 
   /** This method transforms a program and returns verification results based on the cache's
     * current state.
@@ -113,10 +113,9 @@ abstract class Cache {
 
   /** Utility function to retrieve entries for single members.
     * */
-  final def get(
-                 file_key: String,
-                 key: CacheableMember,
-                 dependencies: List[Member]): Option[CacheEntry] = {
+  final def get(file_key: String,
+                key: CacheableMember,
+                dependencies: List[Member]): Option[CacheEntry] = {
 
     val concerning_hash = key.hash()
     val dependencies_hash = dependencies.map(_.hash()).mkString(" ")
@@ -214,8 +213,8 @@ trait CacheContent
   * */
 trait Member {
 
- /** Must be implemented to return a hash String for this Member.
-   * */
+  /** Must be implemented to return a hash String for this Member.
+    * */
   def hash(): String
 }
 
diff --git a/src/main/scala/viper/server/vsi/Envelope.scala b/src/main/scala/viper/server/vsi/Envelope.scala
index 4121b3c..2d7df97 100644
--- a/src/main/scala/viper/server/vsi/Envelope.scala
+++ b/src/main/scala/viper/server/vsi/Envelope.scala
@@ -12,18 +12,12 @@ package viper.server.vsi
   * */
 trait Envelope
 
-sealed trait Post {
+trait Post {
   type A
-}
-
-trait Packer extends Post {
 
   /** Must be implemented to map client-specific messages to Envelopes.
     * */
   def pack(m: A): Envelope
-}
-
-trait Unpacker extends Post {
 
   /** Must be implemented to map Envelopes to client-specific messages.
     * */
diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala
index 97e02a9..e1b4ecb 100644
--- a/src/main/scala/viper/server/vsi/HTTP.scala
+++ b/src/main/scala/viper/server/vsi/HTTP.scala
@@ -16,7 +16,7 @@ import akka.http.scaladsl.server.Route
 import akka.pattern.ask
 import akka.stream.scaladsl.Source
 import akka.util.Timeout
-import viper.server.vsi.VerificationProtocol.Stop
+import viper.server.vsi.VerificationProtocol.StopVerification
 
 import scala.concurrent.Future
 import scala.concurrent.duration._
@@ -26,6 +26,11 @@ import scala.util.{Failure, Success, Try}
   * */
 sealed trait BasicHttp {
 
+  /** Specifies the port through which the clients may access this server instance.
+    *
+    * The default port number tells the system to automatically pick an available port
+    * (depends on the implementation of the underlying socket library)
+    * */
   var port: Int = _
 
   /** Must be implemented to return the routes defined for this server.
@@ -56,16 +61,17 @@ sealed trait CustomizableHttp extends BasicHttp {
   * server. In particular, this means providing a protocol that returns the VerificationServer's
   * responses as type [[ToResponseMarshallable]].
   * */
-trait VerificationServerHTTP extends VerificationServer with CustomizableHttp {
+trait VerificationServerHttp extends VerificationServer with CustomizableHttp {
 
   def setRoutes(): Route
 
   var bindingFuture: Future[Http.ServerBinding] = _
 
   override def start(active_jobs: Int): Unit = {
-    jobs = new JobPool(active_jobs)
+    ast_jobs = new JobPool("AST-pool", active_jobs)
+    ver_jobs = new JobPool("Verification-pool", active_jobs)
     bindingFuture = Http().bindAndHandle(setRoutes(), "localhost", port)
-    _termActor = system.actorOf(Terminator.props(bindingFuture), "terminator")
+    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), "terminator")
     isRunning = true
   }
 
@@ -113,46 +119,94 @@ trait VerificationServerHTTP extends VerificationServer with CustomizableHttp {
         complete(onVerifyPost(r))
       }
     }
-  } ~ path("verify" / IntNumber) { jid =>
-    /** Send GET request to "/verify/<jid>" where <jid> is a non-negative integer.
-      * <jid> must be an ID of an existing verification job.
-      */
+  } ~ path("ast" / IntNumber) { id =>
+    val ast_id = AstJobId(id)
     get {
-      jobs.lookupJob(JobID(jid)) match {
+      ast_jobs.lookupJob(ast_id) match {
         case Some(handle_future) =>
-          // Found a job with this jid.
           onComplete(handle_future) {
             case Success(handle) =>
-              val s: Source[Envelope, NotUsed] = Source.fromPublisher((handle.publisher))
-              _termActor ! Terminator.WatchJobQueue(JobID(jid), handle)
+              val s: Source[Envelope, NotUsed] = Source.fromPublisher(handle.publisher)
               complete(unpackMessages(s))
             case Failure(error) =>
-              complete(verificationRequestRejection(jid, error))
+              // TODO use AST-specific response
+              complete(verificationRequestRejection(id, error))
+          }
+        case None =>
+          // TODO use AST-specific response
+          complete(verificationRequestRejection(id, JobNotFoundException))
+      }
+    }
+  } ~ path("verify" / IntNumber) { id =>
+    /** Send GET request to "/verify/<jid>" where <jid> is a non-negative integer.
+      * <jid> must be an ID of an existing verification job.
+      */
+    val ver_id = VerJobId(id)
+    get {
+      ver_jobs.lookupJob(ver_id) match {
+        case None =>
+          /** Verification job with this ID is not found. */
+          complete(verificationRequestRejection(id, JobNotFoundException))
+
+        case Some(handle_future) =>
+          /** Combine the future AST and the future verification results. */
+          onComplete(handle_future.flatMap((ver_handle: VerHandle) => {
+            /** If there exists a verification job, there should have existed
+              * (or should still exist) a corresponding AST construction job. */
+            val ast_id: AstJobId = ver_handle.prev_job_id.get
+
+            /** The AST construction job may have been cleaned up
+              * (if all of its messages were already consumed) */
+            ast_jobs.lookupJob(ast_id) match {
+              case Some(ast_handle_fut) =>
+                ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle))
+              case None =>
+                Future.successful((None, ver_handle))
+            }
+          })) {
+            case Success((ast_handle_maybe, ver_handle)) =>
+              val ver_source = ver_handle match {
+                case VerHandle(null, null, null, ast_id) =>
+                  /** There were no messages produced during verification. */
+                  Source.empty[Envelope]
+                case _ =>
+                  Source.fromPublisher(ver_handle.publisher)
+              }
+              val ast_source = ast_handle_maybe match {
+                case None =>
+                  /** The AST messages were already consumed. */
+                  Source.empty[Envelope]
+                case Some(ast_handle) =>
+                  Source.fromPublisher(ast_handle.publisher)
+              }
+              val resulting_source = ver_source.prepend(ast_source)
+              complete(unpackMessages(resulting_source))
+            case Failure(error) =>
+              complete(verificationRequestRejection(id, error))
           }
-        case _ =>
-          complete(verificationRequestRejection(jid, JobNotFoundException()))
       }
     }
-  } ~ path("discard" / IntNumber) { jid =>
+  } ~ path("discard" / IntNumber) { id =>
     /** Send GET request to "/discard/<jid>" where <jid> is a non-negative integer.
       * <jid> must be an ID of an existing verification job.
       */
+    val ver_id = VerJobId(id)
     get {
-      jobs.lookupJob(JobID(jid)) match {
+      ver_jobs.lookupJob(ver_id) match {
         case Some(handle_future) =>
           onComplete(handle_future) {
             case Success(handle) =>
               implicit val askTimeout: Timeout = Timeout(5000 milliseconds)
-              val interrupt_done: Future[String] = (handle.job_actor ? Stop).mapTo[String]
+              val interrupt_done: Future[String] = (handle.job_actor ? StopVerification).mapTo[String]
               onSuccess(interrupt_done) { msg =>
                 handle.job_actor ! PoisonPill // the actor played its part.
-                complete(discardJobConfirmation(jid, msg))
+                complete(discardJobConfirmation(id, msg))
               }
             case Failure(_) =>
-              complete(discardJobRejection(jid))
+              complete(discardJobRejection(id))
           }
         case _ =>
-          complete(discardJobRejection(jid))
+          complete(discardJobRejection(id))
       }
     }
   }
diff --git a/src/main/scala/viper/server/vsi/JobActor.scala b/src/main/scala/viper/server/vsi/JobActor.scala
new file mode 100644
index 0000000..3b8b92e
--- /dev/null
+++ b/src/main/scala/viper/server/vsi/JobActor.scala
@@ -0,0 +1,90 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.vsi
+
+import akka.actor.{Actor, Props}
+
+import scala.concurrent.Future
+
+
+class TaskThread[T](private val _task: MessageStreamingTask[T]) extends Thread(_task) {
+  def getArtifact: Option[Future[T]] = _task.artifact
+}
+
+// --- Actor: JobActor ---
+
+object JobActor {
+  def props[T](id: JobId): Props = Props(new JobActor[T](id))
+}
+
+class JobActor[T](private val id: JobId) extends Actor {
+
+  import VerificationProtocol._
+
+  private var _astConstructionTask: TaskThread[T] = _
+  private var _verificationTask: TaskThread[T] = _
+
+  private def interrupt(task: TaskThread[T]): Boolean = {
+    if (task != null && task.isAlive) {
+      task.interrupt()
+      task.join()
+      return true
+    }
+    false
+  }
+
+  private def resetTask(task: TaskThread[T]): Unit = {
+    if (task != null && task.isAlive) {
+      task.interrupt()
+      task.join()
+    }
+  }
+
+  private def resetAstConstructionTask(): Unit = {
+    resetTask(_astConstructionTask)
+    _astConstructionTask = null
+  }
+
+  private def resetVerificationTask(): Unit = {
+    resetTask(_verificationTask)
+    _verificationTask = null
+  }
+
+  override def receive: PartialFunction[Any, Unit] = {
+    case req: StartProcessRequest[T] =>
+      req match {
+        case _: ConstructAst[T] =>
+          //println(">>> JobActor received request ConstructAst")
+          resetAstConstructionTask()
+          _astConstructionTask = req.task
+          _astConstructionTask.start()
+          sender() ! AstHandle(self, req.queue, req.publisher, _astConstructionTask.getArtifact.get)
+
+        case ver_req: Verify[T] =>
+          //println(">>> JobActor received request Verify")
+          resetVerificationTask()
+          _verificationTask = ver_req.task
+          _verificationTask.start()
+          sender() ! VerHandle(self, ver_req.queue, ver_req.publisher, ver_req.prev_job_id)
+      }
+    case req: StopProcessRequest =>
+      val did_I_interrupt = req match {
+        case StopAstConstruction =>
+          interrupt(_astConstructionTask)
+        case StopVerification =>
+          interrupt(_verificationTask)
+      }
+      if (did_I_interrupt) {
+        sender() ! s"$id has been successfully interrupted."
+      } else {
+        // FIXME: Saying this is a potential vulnerability
+        sender() ! s"$id has already been finalized."
+      }
+    case msg =>
+      throw new Exception("JobActor: received unexpected message: " + msg)
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala
new file mode 100644
index 0000000..252a65d
--- /dev/null
+++ b/src/main/scala/viper/server/vsi/JobPool.scala
@@ -0,0 +1,101 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.vsi
+
+import akka.actor.ActorRef
+import akka.stream.scaladsl.SourceQueueWithComplete
+import org.reactivestreams.Publisher
+
+import scala.collection.mutable
+import scala.concurrent.{ExecutionContext, Future, Promise}
+
+sealed trait JobId {
+  val id: Int
+  def tag: String
+  override def toString: String = s"${tag}_id_${id}"
+}
+
+case class AstJobId(id: Int) extends JobId {
+  def tag = "ast"
+}
+
+case class VerJobId(id: Int) extends JobId {
+  def tag = "ver"
+}
+
+sealed trait JobHandle {
+  def tag: String  // identify the kind of job this is
+  val job_actor: ActorRef
+  val queue: SourceQueueWithComplete[Envelope]
+  val publisher: Publisher[Envelope]
+}
+
+case class AstHandle[R](job_actor: ActorRef,
+                        queue: SourceQueueWithComplete[Envelope],
+                        publisher: Publisher[Envelope],
+                        artifact: Future[R]) extends JobHandle {
+  def tag = "AST"
+}
+
+case class VerHandle(job_actor: ActorRef,
+                     queue: SourceQueueWithComplete[Envelope],
+                     publisher: Publisher[Envelope],
+                     prev_job_id: Option[AstJobId]) extends JobHandle {
+  def tag = "VER"
+}
+
+class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS: Int = 3)
+                                         (implicit val jid_fact: Int => S,
+                                          ctx: ExecutionContext) {
+
+  private val _jobHandles: mutable.Map[S, Promise[T]] = mutable.Map()
+  private val _jobExecutors: mutable.Map[S, () => Future[T]] = mutable.Map()
+  private val _jobCache: mutable.Map[S, Future[T]] = mutable.Map()
+  def jobHandles: Map[S, Future[T]] = _jobHandles.map{ case (id, hand) => (id, hand.future) }.toMap
+
+  private var _nextJobId: Int = 0
+
+  def newJobsAllowed: Boolean = jobHandles.size < MAX_ACTIVE_JOBS
+
+  def bookNewJob(job_executor: S => Future[T]): S = {
+    require(newJobsAllowed)
+
+    val new_jid: S = jid_fact(_nextJobId)
+
+    _jobHandles(new_jid) = Promise()
+    _jobExecutors(new_jid) = () => {
+      if (_jobCache.contains(new_jid)) {
+        /** This prevents recomputing the same future multiple times. */
+        _jobCache(new_jid)
+      } else {
+        /** Create Future[JobHandle]. */
+        val t_fut = job_executor(new_jid)
+
+        /** Cache the newly created Future[JobHandle] for later reference. */
+        _jobCache(new_jid) = t_fut
+        t_fut
+      }
+    }
+    _nextJobId = _nextJobId + 1
+    new_jid
+  }
+
+  def discardJob(jid: S): Unit = {
+    _jobHandles -= jid
+    _jobExecutors -= jid
+    _jobCache -= jid
+  }
+
+  def lookupJob(jid: S): Option[Future[T]] = {
+    _jobHandles.get(jid).map((promise: Promise[T]) => {
+      /** 1. Execute the job and get the result's future OR get the priorly cached result's future.
+        * 2. Complete the promise with this future. */
+      promise.completeWith(_jobExecutors(jid)())
+      promise.future
+    })
+  }
+}
diff --git a/src/main/scala/viper/server/vsi/MessageStreamingTask.scala b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala
new file mode 100644
index 0000000..492e66c
--- /dev/null
+++ b/src/main/scala/viper/server/vsi/MessageStreamingTask.scala
@@ -0,0 +1,70 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.vsi
+
+import scala.language.postfixOps
+
+import akka.actor.ActorRef
+import akka.pattern.ask
+import akka.stream.QueueOfferResult
+import akka.util.Timeout
+
+import scala.concurrent.{ExecutionContext, Future}
+import scala.concurrent.duration._
+
+
+
+/** This class is a generic wrapper for a any sort of verification a VerificationServer might
+  * work on.
+  *
+  * It has the following properties:
+  *  - implements runnable
+  *  - provides a reference to a queue actor.
+  *
+  *  The first serves the purpose of running the process concurrently. The second allows to
+  *  communicate from the verification process to the server.
+  * */
+abstract class MessageStreamingTask[T]()(implicit val executionContext: ExecutionContext) extends Runnable with Post {
+
+  def artifact: Option[Future[T]]
+
+  private var q_actor: ActorRef = _
+
+  final def setQueueActor(actor: ActorRef): Unit = {
+    q_actor = actor
+  }
+
+  /** Sends massage to the attached actor.
+    *
+    * The actor receiving this message offers it to a queue. This offering returns a Future,
+    * which  will eventually indicate whether or not the offer was successful. This method is
+    * blocking, as it waits for the successful completion of such an offer.
+    * */
+  protected def enqueueMessage(msg: Envelope): Unit = {
+    // FIXME ATG: this method needs a review
+    implicit val askTimeout: Timeout = Timeout(5000 milliseconds)
+
+    var current_offer: Future[QueueOfferResult] = null
+    val answer = q_actor ? TaskProtocol.BackendReport(msg)
+    current_offer = answer.flatMap({
+      case res: Future[QueueOfferResult] => res
+    })
+    while (current_offer == null || !current_offer.isCompleted) {
+      Thread.sleep(10)
+    }
+  }
+
+  /** Notify the queue actor that the task has come to an end
+    *
+    * The actor receiving this message will close the queue.
+    *
+    * @param success indicates whether or not the task has ended as successfully.
+    * */
+  protected def registerTaskEnd(success: Boolean): Unit = {
+    q_actor ! TaskProtocol.FinalBackendReport(success)
+  }
+}
diff --git a/src/main/scala/viper/server/vsi/Protocol.scala b/src/main/scala/viper/server/vsi/Protocol.scala
index 0541a0f..ba9efce 100644
--- a/src/main/scala/viper/server/vsi/Protocol.scala
+++ b/src/main/scala/viper/server/vsi/Protocol.scala
@@ -16,16 +16,35 @@ object TaskProtocol {
   case class FinalBackendReport(success: Boolean)
 }
 
-// Protocol to start/stop verification process.
 object VerificationProtocol {
 
-  // Request Job Actor to execute verification task
-  case class Verify(task: Thread, queue: SourceQueueWithComplete[Envelope], publisher: Publisher[Envelope])
+  sealed trait StartProcessRequest[T] {
+    val task: TaskThread[T]
+    val queue: SourceQueueWithComplete[Envelope]
+    val publisher: Publisher[Envelope]
+  }
 
-  // Verification interrupt request to Terminator Actor
-  case class Stop()
+  // Request Job Actor to execute an AST construction task
+  case class ConstructAst[T](task: TaskThread[T],
+                             queue: SourceQueueWithComplete[Envelope],
+                             publisher: Publisher[Envelope]) extends StartProcessRequest[T]
+
+  // Request Job Actor to execute a verification task
+  case class Verify[T](task: TaskThread[T],
+                       queue: SourceQueueWithComplete[Envelope],
+                       publisher: Publisher[Envelope],
+                       prev_job_id: Option[AstJobId]) extends StartProcessRequest[T]
+
+  sealed trait StopProcessRequest
+
+  // Request Job Actor to stop its verification task
+  case object StopAstConstruction extends StopProcessRequest
+
+  // Request Job Actor to stop its verification task
+  case object StopVerification extends StopProcessRequest
 }
 
+
 object Requests extends akka.http.scaladsl.marshallers.sprayjson.SprayJsonSupport with DefaultJsonProtocol {
 
   case class VerificationRequest(arg: String)
diff --git a/src/main/scala/viper/server/vsi/QueueActor.scala b/src/main/scala/viper/server/vsi/QueueActor.scala
new file mode 100644
index 0000000..be9dd6a
--- /dev/null
+++ b/src/main/scala/viper/server/vsi/QueueActor.scala
@@ -0,0 +1,29 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.vsi
+
+import akka.actor.{Actor, PoisonPill, Props}
+import akka.stream.scaladsl.SourceQueueWithComplete
+
+// --- Actor: MessageActor ---
+
+object QueueActor {
+  def props(queue: SourceQueueWithComplete[Envelope]): Props = Props(new QueueActor(queue))
+}
+
+class QueueActor(queue: SourceQueueWithComplete[Envelope]) extends Actor {
+
+  override def receive: PartialFunction[Any, Unit] = {
+    case TaskProtocol.BackendReport(msg) =>
+      val offer_status = queue.offer(msg)
+      sender() ! offer_status
+    case TaskProtocol.FinalBackendReport(_) =>
+      queue.complete()
+      self ! PoisonPill
+    case _ =>
+  }
+}
diff --git a/src/main/scala/viper/server/vsi/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala
new file mode 100644
index 0000000..7fd4f65
--- /dev/null
+++ b/src/main/scala/viper/server/vsi/Terminator.scala
@@ -0,0 +1,47 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.vsi
+
+import akka.actor.{Actor, ActorSystem, Props}
+import akka.http.scaladsl.Http
+
+import scala.concurrent.{ExecutionContext, Future}
+
+// --- Actor: Terminator ---
+
+
+object Terminator {
+  case object Exit
+  case class WatchJobQueue(jid: JobId, handle: JobHandle)
+
+  def props[R](ast_jobs: JobPool[AstJobId, AstHandle[R]],
+               ver_jobs: JobPool[VerJobId, VerHandle],
+               bindingFuture: Option[Future[Http.ServerBinding]] = None)
+            (implicit ctx: ExecutionContext, sys: ActorSystem): Props
+  = Props(new Terminator(ast_jobs, ver_jobs, bindingFuture)(ctx, sys))
+}
+
+class Terminator[R](ast_jobs: JobPool[AstJobId, AstHandle[R]],
+                    ver_jobs: JobPool[VerJobId, VerHandle],
+                    bindingFuture: Option[Future[Http.ServerBinding]])
+                (implicit val ctx: ExecutionContext,
+                 implicit val sys: ActorSystem) extends Actor {
+
+  override def receive: PartialFunction[Any, Unit] = {
+    case Terminator.Exit =>
+      bindingFuture match {
+        case Some(future) =>
+          future
+            .flatMap(_.unbind()) // trigger unbinding from the port
+            .onComplete(_ => {
+              sys.terminate() // and shutdown when done
+            })
+        case None =>
+          sys.terminate() // shutdown
+      }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala
index a5504b4..4830329 100644
--- a/src/main/scala/viper/server/vsi/VerificationServer.scala
+++ b/src/main/scala/viper/server/vsi/VerificationServer.scala
@@ -6,61 +6,23 @@
 
 package viper.server.vsi
 
-import akka.actor.{Actor, ActorRef, ActorSystem, PoisonPill, Props}
-import akka.http.scaladsl.Http
+import akka.Done
+import akka.actor.{ActorRef, ActorSystem, PoisonPill}
 import akka.pattern.ask
-import akka.stream.scaladsl.{Keep, Sink, Source, SourceQueueWithComplete}
-import akka.stream.{ActorMaterializer, OverflowStrategy, QueueOfferResult}
+import akka.stream.scaladsl.{Keep, Sink, Source}
+import akka.stream.{ActorMaterializer, OverflowStrategy}
 import akka.util.Timeout
-import akka.{Done, NotUsed}
-import org.reactivestreams.Publisher
 
-import scala.collection.mutable
 import scala.concurrent.duration._
-import scala.concurrent.{ExecutionContext, Future}
-import scala.util.{Failure, Success}
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor, Future}
 import scala.language.postfixOps
+import scala.reflect.ClassTag
+import scala.util.{Failure, Success}
 
 
-class VerificationServerException extends Exception
-case class JobNotFoundException() extends VerificationServerException
-
-case class JobID(id: Int)
-case class JobHandle(job_actor: ActorRef,
-                     queue: SourceQueueWithComplete[Envelope],
-                     publisher: Publisher[Envelope])
-
-/** This class manages the verification jobs the server receives.
-  */
-class JobPool(val MAX_ACTIVE_JOBS: Int = 3) {
-  var jobHandles: mutable.Map[Int, Future[JobHandle]] = mutable.Map[Int, Future[JobHandle]]()
-  private var _nextJobId: Int = 0
-
-  def newJobsAllowed = jobHandles.size < MAX_ACTIVE_JOBS
-
-  /** Creates a Future of a JobHandle.
-    *
-    * For the next available job ID the function job_executor will set up a JobActor. That actor
-    * will start a verification process and produce a Future JobHandle. The Future will
-    * successfully complete as soon as the verification process was started successfully.
-    * */
-  def bookNewJob(job_executor: Int => Future[JobHandle]): (Int, Future[JobHandle]) = {
-    val new_jid = _nextJobId
-    jobHandles(new_jid) = job_executor(new_jid)
-    _nextJobId = _nextJobId + 1
-    (new_jid, jobHandles(new_jid))
-  }
-
-  /** Discards the JobHandle for the given JobID
-    * */
-  def discardJob(jid: JobID): mutable.Map[Int, Future[JobHandle]] = {
-    jobHandles -= jid.id
-  }
-
-  def lookupJob(jid: JobID): Option[ Future[JobHandle] ] = {
-    jobHandles.get(jid.id)
-  }
-}
+abstract class VerificationServerException extends Exception
+case object JobNotFoundException extends VerificationServerException
+abstract class AstConstructionException extends VerificationServerException
 
 /** This trait provides state and process management functionality for verification servers.
   *
@@ -77,131 +39,121 @@ class JobPool(val MAX_ACTIVE_JOBS: Int = 3) {
   *  between a VerificationTask's backend and the server. The Terminator Actor is in charge of
   *  terminating both individual processes and the server.
   */
-trait VerificationServer extends Unpacker {
+trait VerificationServer extends Post {
+
+  type AST
 
   implicit val system: ActorSystem = ActorSystem("Main")
-  implicit val executionContext = ExecutionContext.global
+  implicit val executionContext: ExecutionContextExecutor = ExecutionContext.global
   implicit val materializer: ActorMaterializer = ActorMaterializer()
 
-  protected var jobs: JobPool = _
+  protected var _termActor: ActorRef = _
+
+  implicit val ast_id_fact: Int => AstJobId = AstJobId.apply
+  implicit val ver_id_fact: Int => VerJobId = VerJobId.apply
+
+  protected var ast_jobs: JobPool[AstJobId, AstHandle[AST]] = _
+  protected var ver_jobs: JobPool[VerJobId, VerHandle] = _
+
   var isRunning: Boolean = false
 
-  /** Configures an instance of ViperCoreServer.
+  /** Configures an instance of VerificationServer.
     *
     * This function must be called before any other. Calling any other function before this one
     * will result in an IllegalStateException.
     * */
   def start(active_jobs: Int): Unit = {
-    jobs = new JobPool(active_jobs)
-    _termActor = system.actorOf(Terminator.props(), "terminator")
+    ast_jobs = new JobPool("VSI-AST-pool", active_jobs)
+    ver_jobs = new JobPool("VSI-Verification-pool", active_jobs)
+    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs), "terminator")
     isRunning = true
   }
 
-  // --- Actor: Terminator ---
-
-  protected var _termActor: ActorRef = _
+  protected def initializeProcess[S <: JobId, T <: JobHandle : ClassTag]
+                      (pool: JobPool[S, T],
+                      task_fut: Future[MessageStreamingTask[AST]],
+                      prev_job_id_maybe: Option[AstJobId] = None): S = {
 
-  object Terminator {
-    case object Exit
-    case class WatchJobQueue(jid: JobID, handle: JobHandle)
-
-    def props(bindingFuture: Future[Http.ServerBinding]): Props = Props(new Terminator(Some(bindingFuture)))
-    def props(): Props = Props(new Terminator(None))
-  }
-
-  class Terminator(bindingFuture: Option[Future[Http.ServerBinding]]) extends Actor {
-
-    override def receive: PartialFunction[Any, Unit] = {
-      case Terminator.Exit =>
-        bindingFuture match {
-          case Some(future) =>
-            future
-              .flatMap(_.unbind()) // trigger unbinding from the port
-              .onComplete(_ => {
-                system.terminate() // and shutdown when done
-              })
-          case None =>
-            system.terminate() // shutdown
-        }
-      case Terminator.WatchJobQueue(jid, handle) =>
-        val queue_completion_future: Future[Done] = handle.queue.watchCompletion()
-        queue_completion_future.onComplete( {
-          case Failure(e) =>
-            throw e
-          case Success(_) =>
-            jobs.discardJob(jid)
-        })
+    if (!isRunning) {
+      throw new IllegalStateException("Instance of VerificationServer already stopped")
     }
-  }
-
 
-  // --- Actor: JobActor ---
-
-  object JobActor {
-    def props(id: Int): Props = Props(new JobActor(id))
-  }
-
-  class JobActor(private val id: Int) extends Actor {
-
-    private var _verificationTask: Thread = _
-
-    private def interrupt: Boolean = {
-      if (_verificationTask != null && _verificationTask.isAlive) {
-        _verificationTask.interrupt()
-        _verificationTask.join()
-        return true
-      }
-      false
-    }
-
-    private def resetVerificationTask(): Unit = {
-      if (_verificationTask != null && _verificationTask.isAlive) {
-        _verificationTask.interrupt()
-        _verificationTask.join()
-      }
-      _verificationTask = null
-    }
-
-    override def receive: PartialFunction[Any, Unit] = {
-      case VerificationProtocol.Stop =>
-        val did_I_interrupt = interrupt
-        if (did_I_interrupt) {
-          sender() ! s"Job #$id has been successfully interrupted."
-        } else {
-          sender() ! s"Job #$id has already been finalized."
+    require(pool.newJobsAllowed)
+
+    /** Ask the pool to book a new job using the above function
+      * to construct Future[JobHandle] and Promise[AST] later on. */
+    pool.bookNewJob((new_jid: S) => task_fut.flatMap((task: MessageStreamingTask[AST]) => {
+
+      /** TODO avoid hardcoded parameters */
+      implicit val askTimeout: Timeout = Timeout(5000 milliseconds)
+
+      /** What we really want here is SourceQueueWithComplete[Envelope]
+        * Publisher[Envelope] might be needed to create a stream later on,
+        * but the publisher and the queue are synchronized are should be viewed
+        * as different representation of the same concept.
+        */
+      val (queue, publisher) = Source.queue[Envelope](10000, OverflowStrategy.backpressure)
+        .toMat(Sink.asPublisher(false))(Keep.both).run()
+
+      /** This actor will be responsible for managing ONE queue,
+        * whereas the JobActor can manage multiple tasks, all of which are related to some pipeline,
+        * e.g.   [Text] ---> [AST] ---> [VerificationResult]
+        *        '--- Task I ----'                         |
+        *                    '---------- Task II ----------'
+        **/
+      val message_actor = system.actorOf(QueueActor.props(queue), s"${pool.tag}--message_actor--${new_jid.id}")
+      task.setQueueActor(message_actor)
+
+      val job_actor = system.actorOf(JobActor.props(new_jid), s"${pool.tag}_job_actor_${new_jid}")
+
+      /** Register cleanup task. */
+      queue.watchCompletion().onComplete(_ => {
+        pool.discardJob(new_jid)
+        /** FIXME: if the job actors are meant to be reused from one phase to another (not implemented yet),
+          * FIXME: then they should be stopped only after the **last** job is completed in the pipeline. */
+        job_actor ! PoisonPill
+      })
+
+      (job_actor ? (new_jid match {
+        case _: AstJobId =>
+          VerificationProtocol.ConstructAst(new TaskThread(task), queue, publisher)
+        case _: VerJobId =>
+          VerificationProtocol.Verify(new TaskThread(task), queue, publisher,
+            /** TODO: Use factories for specializing the messages.
+              * TODO: Clearly, there should be a clean separation between concrete job types
+              * TODO: (AST Construction, Verification) and generic types (JobHandle). */
+            prev_job_id_maybe match {
+              case Some(prev_job_id: AstJobId) =>
+                Some(prev_job_id)
+              case Some(prev_job_id) =>
+                throw new IllegalArgumentException(s"cannot map ${prev_job_id.toString} to expected type AstJobId")
+              case None =>
+                None
+            })
+      })).mapTo[T]
+
+    }).recover({
+      case e: AstConstructionException =>
+        // If the AST construction phase failed, remove the verification job handle
+        // from the corresponding pool.
+        pool.discardJob(new_jid)
+        new_jid match {
+          case _: VerJobId =>
+            // FIXME perhaps return None instead of nulls here.
+            VerHandle(null, null, null, prev_job_id_maybe)
         }
-      case VerificationProtocol.Verify(task, queue, publisher) =>
-        resetVerificationTask()
-        sender() ! startJob(task, queue, publisher)
-      case msg =>
-        throw new Exception("Main Actor: unexpected message received: " + msg)
-    }
-
-    private def startJob(task: Thread, queue: SourceQueueWithComplete[Envelope], publisher: Publisher[Envelope]): JobHandle = {
-      _verificationTask = task
-      _verificationTask.start()
-      JobHandle(self, queue, publisher)
-    }
-  }
-
-
-  // --- Actor: MessageActor ---
-
-  object QueueActor {
-    def props(jid: Int, queue: SourceQueueWithComplete[Envelope]): Props =
-      Props(new QueueActor(jid, queue))
+    }).mapTo[T])
   }
 
-  class QueueActor(jid: Int, queue: SourceQueueWithComplete[Envelope]) extends Actor {
+  protected def initializeAstConstruction(task: MessageStreamingTask[AST]): AstJobId = {
+    if (!isRunning) {
+      throw new IllegalStateException("Instance of VerificationServer already stopped")
+    }
 
-    override def receive: PartialFunction[Any, Unit] = {
-      case TaskProtocol.BackendReport(msg) =>
-        val offer_status = queue.offer(msg)
-        sender() ! offer_status
-      case TaskProtocol.FinalBackendReport(_) =>
-        queue.complete()
-        self ! PoisonPill
-      case _ =>
+    if (ast_jobs.newJobsAllowed) {
+      initializeProcess(ast_jobs, Future.successful(task))
+    } else {
+      AstJobId(-1) // Process Management running  at max capacity.
     }
   }
 
@@ -209,30 +161,15 @@ trait VerificationServer extends Unpacker {
     *
     * As such, it accepts an instance of a VerificationTask, which it will pass to the JobActor.
     */
-  protected def initializeVerificationProcess(task:VerificationTask): JobID = {
-    if(!isRunning) {
-      throw new IllegalStateException("Instance of ViperCoreServer already stopped")
+  protected def initializeVerificationProcess(task_fut: Future[MessageStreamingTask[AST]], ast_job_id_maybe: Option[AstJobId]): VerJobId = {
+    if (!isRunning) {
+      throw new IllegalStateException("Instance of VerificationServer already stopped")
     }
 
-    if (jobs.newJobsAllowed) {
-      def createJob(new_jid: Int): Future[JobHandle] = {
-
-        implicit val askTimeout: Timeout = Timeout(5000 milliseconds)
-        val job_actor = system.actorOf(JobActor.props(new_jid), s"job_actor_$new_jid")
-        val (queue, publisher) = Source.queue[Envelope](10000, OverflowStrategy.backpressure)
-                                       .toMat(Sink.asPublisher(false))(Keep.both)
-                                       .run()
-        val message_actor = system.actorOf(QueueActor.props(new_jid, queue), s"queue_actor_$new_jid")
-        task.setQueueActor(message_actor)
-        val task_with_actor = new Thread(task)
-        val answer = job_actor ? VerificationProtocol.Verify(task_with_actor, queue, publisher)
-        val new_job_handle: Future[JobHandle] = answer.mapTo[JobHandle]
-        new_job_handle
-      }
-      val (id, _) = jobs.bookNewJob(createJob)
-      JobID(id)
+    if (ver_jobs.newJobsAllowed) {
+      initializeProcess(ver_jobs, task_fut, ast_job_id_maybe)
     } else {
-      JobID(-1) // Process Management running  at max capacity.
+      VerJobId(-1)  // Process Management running  at max capacity.
     }
   }
 
@@ -240,33 +177,65 @@ trait VerificationServer extends Unpacker {
     *
     * Deletes the JobHandle on completion.
     */
-  protected def streamMessages(jid: JobID, clientActor: ActorRef): Option[Future[Unit]] = {
-    if(!isRunning) {
-      throw new IllegalStateException("Instance of ViperCoreServer already stopped")
+  protected def streamMessages(jid: VerJobId, clientActor: ActorRef): Option[Future[Done]] = {
+    if (!isRunning) {
+      throw new IllegalStateException("Instance of VerificationServer already stopped")
     }
 
-    jobs.lookupJob(jid) match {
+    ver_jobs.lookupJob(jid) match {
+      case None =>
+        /** Verification job not found */
+        None
       case Some(handle_future) =>
-        def mapHandle(handle: JobHandle): Future[Unit] = {
-          val src_envelope: Source[Envelope, NotUsed] = Source.fromPublisher((handle.publisher))
-          val src_msg: Source[A , NotUsed] = src_envelope.map(e => unpack(e))
-          src_msg.runWith(Sink.actorRef(clientActor, Success))
-          _termActor ! Terminator.WatchJobQueue(jid, handle)
-          handle.queue.watchCompletion().map(_ => ())
-        }
-        Some(handle_future.flatMap(mapHandle))
-      case None => None
+        Some(handle_future.flatMap((ver_handle: VerHandle) => {
+          ver_handle.prev_job_id match {
+            case None =>
+              /** The AST for this verification job wasn't created by this server. */
+              Future.successful((None, ver_handle))
+            case Some(ast_id) =>
+              /** The AST construction job may have been cleaned up
+                * (if all of its messages were already consumed) */
+              ast_jobs.lookupJob(ast_id) match {
+                case Some(ast_handle_fut) =>
+                  ast_handle_fut.map(ast_handle => (Some(ast_handle), ver_handle))
+                case None =>
+                  Future.successful((None, ver_handle))
+              }
+          }
+        }) flatMap {
+          case (ast_handle_maybe: Option[AstHandle[AST]], ver_handle: VerHandle) =>
+            val ver_source = ver_handle match {
+              case VerHandle(null, null, null, ast_id) =>
+                /** There were no messages produced during verification. */
+                Source.empty[Envelope]
+              case _ =>
+                Source.fromPublisher(ver_handle.publisher)
+            }
+            val ast_source = ast_handle_maybe match {
+              case None =>
+                /** The AST messages were already consumed. */
+                Source.empty[Envelope]
+              case Some(ast_handle) =>
+                Source.fromPublisher(ast_handle.publisher)
+            }
+            val resulting_source = ver_source.prepend(ast_source).map(e => unpack(e))
+            resulting_source.runWith(Sink.actorRef(clientActor, Success))
+
+            // FIXME This assumes that someone will actually complete the verification job queue.
+            // FIXME Could we guarantee that the client won't forget to do this?
+            ver_handle.queue.watchCompletion()
+        })
     }
   }
 
-  /** Stops an instance of ViperCoreServer from running.
+  /** Stops an instance of VerificationServer from running.
     *
     * As such it should be the last method called. Calling any other function after stop will
     * result in an IllegalStateException.
     * */
   def stop(): Unit = {
     if(!isRunning) {
-      throw new IllegalStateException("Instance of ViperCoreServer already stopped")
+      throw new IllegalStateException("Instance of VerificationServer already stopped")
     }
     isRunning = false
 
@@ -274,7 +243,7 @@ trait VerificationServer extends Unpacker {
       case Success(_) =>
         _termActor ! Terminator.Exit
         println(s"shutting down...")
-      case Failure(_) =>
+      case Failure(err_msg) =>
         _termActor ! Terminator.Exit
         println(s"forcibly shutting down...")
     }
@@ -283,63 +252,17 @@ trait VerificationServer extends Unpacker {
   /** This method interrupts active jobs upon termination of the server.
     */
   protected def getInterruptFutureList(): Future[List[String]] = {
-    val interrupt_future_list: List[Future[String]] = jobs.jobHandles map { case (_, handle_future) =>
-      handle_future.flatMap {
-        case JobHandle(actor, _, _) =>
-          implicit val askTimeout: Timeout = Timeout(1000 milliseconds)
-          (actor ? VerificationProtocol.Stop).mapTo[String]
-      }
-    } toList
+    implicit val askTimeout: Timeout = Timeout(1000 milliseconds)
+    val interrupt_future_list: List[Future[String]] = (ver_jobs.jobHandles ++ ast_jobs.jobHandles) map {
+      case (jid, handle_future) =>
+        handle_future.flatMap {
+          case AstHandle(actor, _, _, _) =>
+            (actor ? VerificationProtocol.StopAstConstruction).mapTo[String]
+          case VerHandle(actor, _, _, _) =>
+            (actor ? VerificationProtocol.StopVerification).mapTo[String]
+        }
+      } toList
     val overall_interrupt_future: Future[List[String]] = Future.sequence(interrupt_future_list)
     overall_interrupt_future
   }
 }
-
-
-/** This class is a generic wrapper for a any sort of verification a VerificationServer might
-  * work on.
-  *
-  * It has the following properties:
-  *  - implements runnable
-  *  - provides a reference to a queue actor.
-  *
-  *  The first serves the purpose of running the process concurrently. The second allows to
-  *  communicate from the verification process to the server.
-  * */
-abstract class VerificationTask()(implicit val executionContext: ExecutionContext) extends Runnable with Packer {
-
-  private var q_actor: ActorRef = _
-
-  final def setQueueActor(actor: ActorRef): Unit = {
-    q_actor = actor
-  }
-
-  /** Sends massage to the attached actor.
-    *
-    * The actor receiving this message offers it to a queue. This offering returns a Future,
-    * which  will eventually indicate whether or not the offer was successful. This method is
-    * blocking, as it waits for the successful completion of such an offer.
-    * */
-  protected def enqueueMessages(msg: A): Unit = {
-    implicit val askTimeout: Timeout = Timeout(5000 milliseconds)
-
-    var current_offer: Future[QueueOfferResult] = null
-    val answer = q_actor ? TaskProtocol.BackendReport(pack(msg))
-    current_offer = answer.flatMap({
-      case res: Future[QueueOfferResult] => res
-    })
-    while(current_offer == null || !current_offer.isCompleted){
-      Thread.sleep(10)
-    }
-  }
-
-  /** Notify the queue actor that the task has come to an end
-    *
-    * The actor receiving this message will close the queue.
-    *
-    * @param success indicates whether or not the task has ended as successfully.
-    * */
-  protected def registerTaskEnd(success: Boolean): Unit = {
-    q_actor ! TaskProtocol.FinalBackendReport(success)
-  }
-}
diff --git a/src/test/scala/CoreServerTests.scala b/src/test/scala/CoreServerTests.scala
deleted file mode 100644
index 517a712..0000000
--- a/src/test/scala/CoreServerTests.scala
+++ /dev/null
@@ -1,412 +0,0 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2020 ETH Zurich.
-
-package viper.server.core
-
-import akka.actor.{Actor, ActorSystem, Props}
-import akka.http.scaladsl.testkit.ScalatestRouteTest
-import org.scalatest.wordspec.AnyWordSpec
-import org.scalatest.matchers.should.Matchers
-import viper.server.core.ViperBackendConfigs.SiliconConfig
-import viper.server.vsi._
-import viper.server.utility.AstGenerator
-import viper.silver.ast.Program
-import viper.silver.logger.SilentLogger
-import viper.silver.reporter._
-
-import scala.concurrent.Future
-import scala.util.{Failure, Success}
-
-class CoreServerTest extends AnyWordSpec with Matchers with ScalatestRouteTest {
-
-  implicit var actor_system: ActorSystem = ActorSystem("Test")
-  val test_actor_0 = actor_system.actorOf(ClientActor.props(0))
-  val test_actor_1 = actor_system.actorOf(ClientActor.props(1))
-  val test_actor_2 = actor_system.actorOf(ClientActor.props(2))
-  val actor_tests_results: Array[Option[Boolean]] = Array(None, None, None)
-
-  object ClientActor {
-    case object Terminate
-    def props(test_no: Int): Props = Props(new ClientActor(test_no))
-  }
-
-  class ClientActor(private val test_no: Int) extends Actor {
-
-    override def receive: PartialFunction[Any, Unit] = {
-      case m: Message =>
-        m match {
-          case _: OverallSuccessMessage =>
-            actor_tests_results(test_no) = Some(true)
-          case _: OverallFailureMessage =>
-            actor_tests_results(test_no) = Some(false)
-          case _ =>
-        }
-      case ClientActor.Terminate =>
-        system.terminate()
-    }
-  }
-
-  private val silent_logger = SilentLogger()
-
-  private val ast_gen = new AstGenerator(silent_logger)
-  private val empty_file = "src/test/resources/viper/empty.vpr"
-  private val sum_file = "src/test/resources/viper/sum_method.vpr"
-  private val verificationError_file = "src/test/resources/viper/verification_error.vpr"
-
-  private val empty_ast = ast_gen.generateViperAst(empty_file).get
-  private val sum_ast = ast_gen.generateViperAst(sum_file).get
-  private val verificationError_ast = ast_gen.generateViperAst(verificationError_file).get
-
-  private val noCache_backend = SiliconConfig(List("--disableCaching"))
-  private val cache_backend = SiliconConfig(List())
-
-  private val empty_args: Array[String] = Array()
-
-  "An instance of ViperCoreServer" when {
-    "verifying a single program with caching disabled" should {
-      val core = new ViperCoreServer(empty_args)
-
-      "be able to execute 'start()' without exceptions" in {
-        core.start()
-      }
-
-      var jid: JobID = null
-      "be able to execute 'verify()' without exceptions" in {
-        jid = core.verify(verificationError_file, noCache_backend, verificationError_ast)
-        assert(jid != null)
-      }
-
-      "be able to have 'verify()' return a JobHandler with non-negative id" in {
-        assert(jid.id >= 0)
-      }
-
-      var messages_future: Future[Seq[Message]] = null
-      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages." in {
-        messages_future = ViperCoreServerUtils.getMessagesFuture(core, jid)
-        assert(messages_future != null)
-      }
-
-      // "eventually see the future returned from 'getMessagesFuture()' completed successfully" in {
-      //   while (!messages_future.isCompleted) {
-      //     Thread.sleep(100)
-      //   }
-      //   messages_future.onComplete({
-      //     case Success(_) => succeed
-      //     case Failure(e) => fail(e)
-      //   })
-      // }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-
-      "not be able to execute 'verify()' after 'stop()' without exceptions" in {
-        assertThrows[IllegalStateException] {
-          core.verify(verificationError_file, noCache_backend, verificationError_ast)
-        }
-      }
-    }
-
-    "verifying a single program with caching enabled" should {
-      val core = new ViperCoreServer(empty_args)
-
-      "be able to execute 'start()' without exceptions" in {
-        core.start()
-      }
-
-      var jid: JobID = null
-      "be able to execute 'verify()' without exceptions" in {
-        jid = core.verify(sum_file, cache_backend, sum_ast)
-        assert(jid != null)
-      }
-
-      "be able to have 'verify()' return a JobHandler with  non-negative id" in {
-        assert(jid.id >= 0)
-      }
-
-      var messages_future: Future[Seq[Message]] = null
-      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages" in {
-        messages_future = ViperCoreServerUtils.getMessagesFuture(core, jid)
-        assert(messages_future != null)
-      }
-
-      // "see the future returned from 'getMessagesFuture()' eventually completed successfully" in {
-      //   while (!messages_future.isCompleted) {
-      //     Thread.sleep(100)
-      //   }
-      //   messages_future.onComplete({
-      //     case Success(_) => succeed
-      //     case Failure(e) => fail(e)
-      //   })
-      // }
-
-      "see the future returned by 'getMessagesFuture()' eventually complete unsuccessfully for an inexistent job" in {
-        val wrong_jid = JobID(42)
-        messages_future = ViperCoreServerUtils.getMessagesFuture(core, wrong_jid)
-        while (!messages_future.isCompleted) {
-          Thread.sleep(100)
-        }
-        messages_future.onComplete({
-          case Success(_) => fail()
-          case Failure(_) => succeed
-        })
-      }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-
-      "not be able to execute 'verify()' after 'stop()' without exceptions" in {
-        assertThrows[IllegalStateException] {
-          core.verify(sum_file, noCache_backend, sum_ast)
-        }
-      }
-    }
-
-    "verifying multiple programs with caching disabled and retrieving results via 'getMessagesFuture()'" should {
-      val files: List[String] = List(empty_file, sum_file, verificationError_file)
-      val programs: List[Program] = List(empty_ast, sum_ast, verificationError_ast)
-
-      val core = new ViperCoreServer(empty_args)
-      core.start()
-
-      val filesAndProgs: List[(String, Program)] = files.zip(programs)
-      var handlers: List[JobID] = null
-      "be able to have 'verify()' executed repeatedly without exceptions" in {
-        handlers = filesAndProgs map { case (f, p) => core.verify(f, noCache_backend, p) }
-      }
-
-      "be able to have 'verify()' return JobHandlers with unique non-negative ids" in {
-        assert(handlers(0).id == 0)
-        assert(handlers(1).id == 1)
-        assert(handlers(2).id == 2)
-      }
-
-      // "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages containing the expected verification result" in {
-      //   val messages_futures: List[Future[Seq[Message]]] = handlers.map(h => {
-      //     ViperCoreServerUtils.getMessagesFuture(core, h)
-      //   })
-      //   val filesAndFutures = files.zip(messages_futures)
-      //   filesAndFutures.foreach({ case (f, mf) =>
-      //     while (!mf.isCompleted) {
-      //       Thread.sleep(100)
-      //     }
-      //     mf.onComplete({
-      //       case Success(messages) =>
-      //         messages.last match {
-      //           case _: OverallSuccessMessage =>
-      //             assert(f != verificationError_file)
-      //           case _: OverallFailureMessage =>
-      //             assert(f == verificationError_file)
-      //           case _ => fail()
-      //         }
-      //       case Failure(e) => fail(e)
-      //     })
-      //   })
-      // }
-
-      // "be able to execute 'stop()' without exceptions" in {
-      //   core.stop()
-      // }
-    }
-
-    "verifying multiple programs with caching enabled and retrieving results via 'getMessagesFuture()'" should {
-      val files: List[String] = List(empty_file, sum_file, verificationError_file)
-      val programs: List[Program] = List(empty_ast, sum_ast, verificationError_ast)
-
-      val core = new ViperCoreServer(empty_args)
-      core.start()
-
-      val filesAndProgs: List[(String, Program)] = files.zip(programs)
-      var handlers: List[JobID] = null
-      "be able to have 'verify()' executed repeatedly without exceptions" in {
-        handlers = filesAndProgs map { case (f, p) => core.verify(f, noCache_backend, p) }
-      }
-
-      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages containing the expected verification result" in {
-        val messages_futures: List[Future[Seq[Message]]] = handlers.map(h => {
-          ViperCoreServerUtils.getMessagesFuture(core, h)
-        })
-        val filesAndFutures = files.zip(messages_futures)
-        filesAndFutures.foreach({ case (f, mf) =>
-          // while (!mf.isCompleted) {
-          //   Thread.sleep(100)
-          // }
-          mf.onComplete({
-            case Success(messages) =>
-              messages.last match {
-                case _: OverallSuccessMessage =>
-                  assert(f != verificationError_file)
-                case _: OverallFailureMessage =>
-                  assert(f == verificationError_file)
-                case _ => fail()
-              }
-            case Failure(e) => fail(e)
-          })
-        })
-      }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-    }
-
-    "verifying multiple programs with caching disabled and retrieving results via 'streamMessages()" should {
-      val file1 = empty_file
-      val file2 = sum_file
-      val file3 = verificationError_file
-
-      val ast1 = empty_ast
-      val ast2 = sum_ast
-      val ast3 = verificationError_ast
-
-      val core = new ViperCoreServer(empty_args)
-      core.start()
-
-      val jid1 = core.verify(file1, noCache_backend, ast1)
-      val jid2 = core.verify(file2, noCache_backend, ast2)
-      val jid3 = core.verify(file3, noCache_backend, ast3)
-
-      var streamOption1: Option[Future[Unit]] = null
-      var streamOption2: Option[Future[Unit]] = null
-      var streamOption3: Option[Future[Unit]] = null
-
-      var streamState1: Future[Unit] = null
-      var streamState2: Future[Unit] = null
-      var streamState3: Future[Unit] = null
-
-      "be able to have 'streamMessages()' stream a sequence of Viper messages without errors" in {
-        streamOption1 = core.streamMessages(jid1, test_actor_0)
-        streamOption2 = core.streamMessages(jid2, test_actor_1)
-        streamOption3 = core.streamMessages(jid3, test_actor_2)
-      }
-
-      "have the option returned by 'streamMessages()' be defined" in {
-        streamState1 = streamOption1.getOrElse(fail())
-        streamState2 = streamOption2.getOrElse(fail())
-        streamState3 = streamOption3.getOrElse(fail())
-      }
-
-      // "eventually have future returned by 'streamMessages()' be completed" in {
-      //   def allCompleted(): Boolean = {
-      //     streamState1.isCompleted &&
-      //     streamState2.isCompleted &&
-      //     streamState3.isCompleted
-      //   }
-
-      //   while(!allCompleted()){
-      //     Thread.sleep(500)
-      //   }
-      // }
-
-      // "have the stream of messages contain the expected verification result" in {
-      //   Thread.sleep(2000)
-      //   assert(actor_tests_results(0) == Some(true))
-      //   assert(actor_tests_results(1) == Some(true))
-      //   assert(actor_tests_results(2) == Some(false))
-      // }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-    }
-
-    "verifying an incorrect viper program several times with caching enabled" should {
-      val core = new ViperCoreServer(empty_args)
-      core.start()
-
-      // "produce an OverallFailure message with a non-empty error list upon first verification." in {
-      //   val jid_original = core.verify(verificationError_file, cache_backend, verificationError_ast)
-      //   val messages_future_original = ViperCoreServerUtils.getMessagesFuture(core, jid_original)
-      //     while (!messages_future_original.isCompleted) {
-      //       Thread.sleep(500)
-      //     }
-      //     messages_future_original.onComplete({
-      //       case Success(messages) =>
-      //         messages.last match {
-      //           case ofm: OverallFailureMessage =>
-      //             assert(ofm.result.errors.nonEmpty)
-      //           case _ => fail()
-      //         }
-      //       case Failure(e) => fail(e)
-      //     })
-      //   }
-
-      // "produce an EntityFailure message with a set cached flag when reverified." in {
-      //   val jid_cached = core.verify(verificationError_file, cache_backend, verificationError_ast)
-      //   val messages_future_cached = ViperCoreServerUtils.getMessagesFuture(core, jid_cached)
-      //   while (!messages_future_cached.isCompleted) {
-      //     Thread.sleep(100)
-      //   }
-      //   messages_future_cached.onComplete({
-      //     case Success(messages) =>
-      //       val has_cached_msg = messages.exists {
-      //         case EntityFailureMessage(_, _, _, _, true) => true
-      //         case _ => false
-      //       }
-      //       assert(has_cached_msg)
-      //     case Failure(e) => fail(e)
-      //   })
-      // }
-
-      "be able to execute 'flushCache()' without exceptions after several verifications" in {
-        core.flushCache()
-      }
-
-      // "produce an EntityFailure message with cleared cached flag and an OverallFailure message with an non-empty error list when reverified after flushing the cache." in {
-      //   val jid_flushed = core.verify(verificationError_file, cache_backend, verificationError_ast)
-      //   val messages_future_flushed = ViperCoreServerUtils.getMessagesFuture(core, jid_flushed)
-      //   while (!messages_future_flushed.isCompleted) {
-      //     Thread.sleep(100)
-      //   }
-      //   messages_future_flushed.onComplete({
-      //     case Success(messages) =>
-      //       val has_cached_msg = messages.exists {
-      //         case EntityFailureMessage(_, _, _, _, true) => true
-      //         case _ => false
-      //       }
-      //       val has_overall_failure = messages.last match {
-      //         case _: OverallFailureMessage => true
-      //         case _ => false
-      //       }
-      //       assert(!has_cached_msg && has_overall_failure)
-      //     case Failure(e) => fail(e)
-      //   })
-      // }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-    }
-
-    "maximum capacity of verification jobs is exceeded" should {
-      val core = new ViperCoreServer(empty_args)
-      core.start()
-
-      val jid = core.verify(sum_file, noCache_backend, sum_ast)
-      core.verify(sum_file, noCache_backend, sum_ast)
-      core.verify(sum_file, noCache_backend, sum_ast)
-
-      "have 'verify()' return a VerificationJobHandler with negative id" in {
-        val spillHandler = core.verify(sum_file, noCache_backend, sum_ast)
-        assert(spillHandler.id < 0)
-      }
-
-      // "have 'verify()' return a non-negative id upon freeing up a verification request by calling 'getMessagesFuture()'" in {
-      //   val result_future = ViperCoreServerUtils.getMessagesFuture(core, jid)
-      //   while (!result_future.isCompleted) {
-      //     Thread.sleep(100)
-      //   }
-      //   val newHandler = core.verify(sum_file, noCache_backend, sum_ast)
-      //   assert(newHandler.id > 0)
-      // }
-
-      "be able to execute 'stop()' without exceptions" in {
-        core.stop()
-      }
-    }
-  }
-}
\ No newline at end of file
diff --git a/src/test/scala/ParsingTests.scala b/src/test/scala/viper/server/core/AstGenerationTests.scala
similarity index 91%
rename from src/test/scala/ParsingTests.scala
rename to src/test/scala/viper/server/core/AstGenerationTests.scala
index 1073ce1..49cede9 100644
--- a/src/test/scala/ParsingTests.scala
+++ b/src/test/scala/viper/server/core/AstGenerationTests.scala
@@ -1,3 +1,5 @@
+package viper.server.core
+
 // This Source Code Form is subject to the terms of the Mozilla Public
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
@@ -7,13 +9,13 @@
 import java.nio.file.NoSuchFileException
 
 import akka.http.scaladsl.testkit.ScalatestRouteTest
-import org.scalatest.wordspec.AnyWordSpec
-import org.scalatest.matchers.should.Matchers
+import org.scalatest.{Matchers, WordSpec}
 import viper.server.utility.AstGenerator
 import viper.silver.ast.Program
 import viper.silver.logger.ViperStdOutLogger
 
-class ParsingTests extends AnyWordSpec with Matchers with ScalatestRouteTest {
+
+class AstGenerationTests extends WordSpec with Matchers with ScalatestRouteTest {
 
   private val verifiableFile = "src/test/resources/viper/let.vpr"
   private val emptyFile = "src/test/resources/viper/empty.vpr"
@@ -27,7 +29,7 @@ class ParsingTests extends AnyWordSpec with Matchers with ScalatestRouteTest {
   "AstGenerator" should {
     var ast_gen: AstGenerator = null
     s"should be instantiated without errors" in {
-      ast_gen = new AstGenerator(console_logger)
+      ast_gen = new AstGenerator(console_logger.get)
     }
 
     var test_ast: Option[Program] = null
diff --git a/src/test/scala/viper/server/core/AsyncCoreServerSpec.scala b/src/test/scala/viper/server/core/AsyncCoreServerSpec.scala
new file mode 100644
index 0000000..031785b
--- /dev/null
+++ b/src/test/scala/viper/server/core/AsyncCoreServerSpec.scala
@@ -0,0 +1,73 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.core
+
+import akka.actor.ActorSystem
+import org.scalatest.flatspec.AsyncFlatSpec
+import viper.server.core.ViperCoreServerUtils.getMessagesFuture
+import viper.server.utility.AstGenerator
+import viper.silver.ast.Program
+import viper.silver.logger.SilentLogger
+import viper.silver.reporter.{EntityFailureMessage, Message, OverallFailureMessage}
+
+class AsyncCoreServerSpec extends AsyncFlatSpec {
+  implicit var actor_system: ActorSystem = ActorSystem("Test")
+
+  private val test_file = "src/test/resources/viper/verification_error.vpr"
+  private val test_ast: Program = (new AstGenerator(SilentLogger().get)).generateViperAst(test_file).get
+
+  val server_args: Array[String] = Array()
+  val silicon_without_caching: SiliconConfig = SiliconConfig(List("--disableCaching"))
+  val silicon_with_caching: SiliconConfig = SiliconConfig(List())
+
+  val core = new ViperCoreServer(server_args)
+  core.start()
+
+  /* vvvvvvvvvvvvvvvvvvvvvvv */
+
+  behavior of "ViperCoreServer"
+
+  /* ^^^^^^^^^^^^^^^^^^^^^^^ */
+
+  it should s"be able to eventually produce an OverallFailureMessage @$test_file" in {
+    val jid = core.verify(test_file, silicon_with_caching, test_ast)
+    ViperCoreServerUtils.getMessagesFuture(core, jid) map {
+      messages: List[Message] =>
+        val ofms = messages collect {
+          case ofm: OverallFailureMessage => ofm
+        }
+        val efms = messages collect {
+          case efm: EntityFailureMessage => efm
+        }
+        assert(ofms.length === 1)
+        assert(efms.length === 1)
+    }
+  }
+
+  it should s"retrieve the cached results upon requesting to verify the same AST" in {
+    val jid = core.verify(test_file, silicon_with_caching, test_ast)
+    getMessagesFuture(core, jid) map {
+      messages: List[Message] =>
+        val efms: List[EntityFailureMessage] = messages collect {
+          case efm: EntityFailureMessage => efm
+        }
+//        println(ViperCache)
+//        println(efms.last)
+        assert(efms.length === 1 && efms.last.cached)
+//          ofms.last.result.errors.collect { case a: AbstractError => a.cached }.length === 1)
+    }
+  }
+
+  it should s"run getMessagesFuture() to get Seq[Message] containing the expected verification result" in {
+    val jid = core.verify(test_file, silicon_without_caching, test_ast)
+    getMessagesFuture(core, jid) map {
+      messages: List[Message] =>
+//        println(messages)
+        assert(true)
+    }
+  }
+}
diff --git a/src/test/scala/viper/server/core/CoreServerTest.scala b/src/test/scala/viper/server/core/CoreServerTest.scala
new file mode 100644
index 0000000..e2e5b1d
--- /dev/null
+++ b/src/test/scala/viper/server/core/CoreServerTest.scala
@@ -0,0 +1,339 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2020 ETH Zurich.
+
+package viper.server.core
+
+import akka.actor.{Actor, ActorSystem, Props}
+import akka.http.scaladsl.testkit.ScalatestRouteTest
+import org.scalatest.matchers.should.Matchers
+import org.scalatest.wordspec.AnyWordSpec
+import viper.server.utility.AstGenerator
+import viper.server.vsi.VerJobId
+import viper.silver.ast.Program
+import viper.silver.logger.SilentLogger
+import viper.silver.reporter._
+
+import scala.concurrent.duration.DurationInt
+import scala.concurrent.{Await, Future}
+import scala.language.postfixOps
+
+
+/**
+  * TODO rewrite all tests in terms of [[AsyncCoreServerSpec]]
+  *      which offers a the (reactive) specification for ViperCoreServer.
+  */
+class CoreServerTest extends AnyWordSpec with Matchers with ScalatestRouteTest {
+
+  implicit var actor_system: ActorSystem = ActorSystem("Test")
+  private val test_actors = 0 to 2 map ((i: Int) => actor_system.actorOf(ClientActor.props(i)))
+  private val expected_results: Array[Option[Boolean]] = Array(Some(true), Some(true), Some(false))
+
+  object ClientActor {
+    case object Terminate
+    case object ReportOutcome
+    def props(test_no: Int): Props = Props(new ClientActor(test_no))
+  }
+
+  class ClientActor(private val test_no: Int) extends Actor {
+
+    private var outcome: Option[Boolean] = None
+
+    override def receive: PartialFunction[Any, Unit] = {
+      case m: Message =>
+        m match {
+          case _: OverallSuccessMessage =>
+            outcome = Some(true)
+          case _: OverallFailureMessage =>
+            outcome = Some(false)
+          case m =>
+        }
+      case ClientActor.ReportOutcome =>
+        sender() ! outcome
+      case ClientActor.Terminate =>
+        system.terminate()
+    }
+  }
+
+  private val silent_logger = SilentLogger()
+
+  private val ast_gen = new AstGenerator(silent_logger.get)
+
+  private val ver_error_file = "src/test/resources/viper/verification_error.vpr"
+  private val empty_viper_file = "src/test/resources/viper/empty.vpr"
+  private val correct_viper_file = "src/test/resources/viper/sum_method.vpr"
+
+  private val files = List(empty_viper_file, correct_viper_file, ver_error_file)
+
+  private val asts = files.map(ast_gen.generateViperAst(_).get)
+
+  private def getAstByFileName(file: String): Program =
+    (files zip asts collect {
+      case (f, ast) if f==file => ast
+    }).last
+
+  private val noCache_backend = SiliconConfig(List("--disableCaching"))
+  private val cache_backend = SiliconConfig(List())
+
+  private val empty_args: Array[String] = Array()
+
+  "An instance of ViperCoreServer" when {
+    "verifying a single program with caching disabled" should {
+      val core = new ViperCoreServer(empty_args)
+
+      "be able to execute 'start()' without exceptions" in {
+        core.start()
+      }
+
+      var jid: VerJobId = null
+      "be able to execute 'verify()' without exceptions" in {
+        jid = core.verify(ver_error_file, noCache_backend, getAstByFileName(ver_error_file))
+        assert(jid != null)
+      }
+
+      "be able to have 'verify()' return a JobHandler with non-negative id" in {
+        assert(jid.id >= 0)
+      }
+
+      var messages_future: Future[Seq[Message]] = null
+      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages." in {
+        messages_future = ViperCoreServerUtils.getMessagesFuture(core, jid)
+        assert(messages_future != null)
+      }
+
+      "eventually see the future returned from 'getMessagesFuture()' completed successfully" in {
+        while (!messages_future.isCompleted) {
+          Thread.sleep(100)
+        }
+        messages_future.onComplete({
+          case scala.util.Success(_) => succeed
+          case scala.util.Failure(e) => fail(e)
+        })
+      }
+
+      "be able to execute 'stop()' without exceptions" in {
+        core.stop()
+      }
+
+      "not be able to execute 'verify()' after 'stop()' without exceptions" in {
+        assertThrows[IllegalStateException] {
+          core.verify(ver_error_file, noCache_backend, getAstByFileName(ver_error_file))
+        }
+      }
+    }
+
+    "verifying a single program with caching enabled" should {
+      val core = new ViperCoreServer(empty_args)
+
+      "be able to execute 'start()' without exceptions" in {
+        core.start()
+      }
+
+      var jid: VerJobId = null
+      "be able to execute 'verify()' without exceptions" in {
+        jid = core.verify(correct_viper_file, cache_backend, getAstByFileName(correct_viper_file))
+        assert(jid != null)
+      }
+
+      "be able to have 'verify()' return a JobHandler with  non-negative id" in {
+        assert(jid.id >= 0)
+      }
+
+      var messages_future: Future[Seq[Message]] = null
+      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages" in {
+        messages_future = ViperCoreServerUtils.getMessagesFuture(core, jid)
+        assert(messages_future != null)
+      }
+
+      "see the future returned from 'getMessagesFuture()' eventually completed successfully" in {
+        while (!messages_future.isCompleted) {
+          Thread.sleep(100)
+        }
+        messages_future.onComplete {
+          case scala.util.Success(_) => succeed
+          case scala.util.Failure(e) => fail(e)
+        }
+      }
+
+      "see the future returned by 'getMessagesFuture()' eventually complete unsuccessfully for an inexistent job" in {
+        val wrong_jid = VerJobId(42)
+        messages_future = ViperCoreServerUtils.getMessagesFuture(core, wrong_jid)
+        while (!messages_future.isCompleted) {
+          Thread.sleep(100)
+        }
+        messages_future.onComplete {
+          case scala.util.Success(_) => fail()
+          case scala.util.Failure(_) => succeed
+        }
+      }
+
+      "be able to execute 'stop()' without exceptions" in {
+        core.stop()
+      }
+
+      "not be able to execute 'verify()' after 'stop()' without exceptions" in {
+        assertThrows[IllegalStateException] {
+          core.verify(correct_viper_file, noCache_backend, getAstByFileName(correct_viper_file))
+        }
+      }
+    }
+
+    "verifying multiple programs with caching disabled and retrieving results via 'getMessagesFuture()'" should {
+
+      val core = new ViperCoreServer(empty_args)
+      core.start()
+
+      var handlers: List[VerJobId] = null
+      "be able to have 'verify()' executed repeatedly without exceptions" in {
+        handlers = (files zip asts) map { case (f, p) => core.verify(f, noCache_backend, p) }
+      }
+
+      "be able to have 'verify()' return JobHandlers with unique non-negative ids" in {
+        assert(handlers(0).id == 0)
+        assert(handlers(1).id == 1)
+        assert(handlers(2).id == 2)
+      }
+
+      /** Does not terminate. Rewritten in [[AsyncCoreServerSpec]]. */
+//      "be able to have 'getMessagesFuture()' return a future of a sequence of Viper messages containing the expected verification result" in {
+//        val messages_futures: List[Future[Seq[Message]]] = handlers.map(h => {
+//          ViperCoreServerUtils.getMessagesFuture(core, h)
+//        })
+//        files.zip(messages_futures).foreach({ case (f, mf) =>
+//          while (!mf.isCompleted) {
+//            Thread.sleep(100)
+//          }
+//          mf.onComplete({
+//            case scala.util.Success(messages) =>
+//              messages.last match {
+//                case _: OverallSuccessMessage =>
+//                  assert(f != ver_error_file)
+//                case _: OverallFailureMessage =>
+//                  assert(f == ver_error_file)
+//                case _ => fail()
+//              }
+//            case scala.util.Failure(e) => fail(e)
+//          })
+//        })
+//      }
+
+      "be able to execute 'stop()' without exceptions" in {
+        core.stop()
+      }
+    }
+
+    "verifying an incorrect Viper program several times with caching enabled" should {
+      val core = new ViperCoreServer(empty_args)
+      core.start()
+
+      "produce an OverallFailure message with a non-empty error list upon first verification." in {
+        val jid_original = core.verify(ver_error_file, cache_backend, getAstByFileName(ver_error_file))
+
+        val messages_fut = ViperCoreServerUtils.getMessagesFuture(core, jid_original)
+
+        messages_fut.onComplete {
+          case scala.util.Success(messages) =>
+            messages.last match {
+              case ofm: OverallFailureMessage =>
+                assert(ofm.result.errors.nonEmpty)
+              case _ =>
+                fail("last message in stream must be of type OverallFailureMessage")
+            }
+          case scala.util.Failure(e) =>
+            fail(e)
+        }
+
+        Await.ready(messages_fut, 5 seconds)
+      }
+
+      /** Rewritten in [[AsyncCoreServerSpec]] (but currently fails due to Silver issue#489) */
+//      "produce an EntityFailure message with a set cached flag when re-verified." in {
+//
+//        val jid_cached = files zip asts collect {
+//          case (file, ast) if file == ver_error_file =>
+//            core.verify(ver_error_file, cache_backend, ast)
+//        } last
+//
+//        val messages_fut = ViperCoreServerUtils.getMessagesFuture(core, jid_cached)
+//
+//        messages_fut.onComplete {
+//          case scala.util.Success(messages) =>
+//            val has_cached_msg = messages.exists {
+//              case EntityFailureMessage(_, _, _, _, true) => true
+//              case _ => false
+//            }
+//            has_cached_msg should be (true)
+//          case scala.util.Failure(e) => fail(e)
+//        }
+//
+//        Await.ready(messages_fut, 3 seconds)
+//      }
+
+      "be able to execute 'flushCache()' without exceptions after several verifications" in {
+        core.flushCache()
+      }
+
+      "produce an EntityFailure message with cleared cached flag and an OverallFailure message with an non-empty error list when reverified after flushing the cache." in {
+
+        val jid_flushed = files zip asts collect {
+          case (file, ast) if file == ver_error_file =>
+            core.verify(ver_error_file, cache_backend, ast)
+        } last
+
+        val messages_fut = ViperCoreServerUtils.getMessagesFuture(core, jid_flushed)
+
+        Await.result(messages_fut, 5 seconds) match {
+          case messages: List[Message] =>
+            val has_cached_msg = messages.exists {
+              case EntityFailureMessage(_, _, _, _, true) =>
+                true
+              case _ =>
+                false
+            }
+            val has_overall_failure = messages.last match {
+              case _: OverallFailureMessage => true
+              case _ => false
+            }
+            has_cached_msg should be (false)
+            has_overall_failure should be (true)
+        }
+      }
+
+      "be able to execute 'stop()' without exceptions" in {
+        core.stop()
+      }
+    }
+
+    "maximum capacity of verification jobs is exceeded" should {
+      val core = new ViperCoreServer(empty_args)
+      core.start()
+
+      val (test_file, test_ast) = files zip asts collect  {
+        case (file, ast) if file == ver_error_file => (file, ast)
+      } last
+
+      val jid = 1 to core.config.maximumActiveJobs() map {
+        _ => core.verify(test_file, noCache_backend, test_ast)
+      } last
+
+      "have 'verify()' return a VerificationJobHandler with negative id" in {
+        val spillHandler = core.verify(test_file, noCache_backend, test_ast)
+        assert(spillHandler.id < 0)
+      }
+
+      "have 'verify()' return a non-negative id upon freeing up a verification request by calling 'getMessagesFuture()'" in {
+        val result_fut = ViperCoreServerUtils.getMessagesFuture(core, jid)
+        Await.ready(result_fut, 5 seconds)
+
+        val newHandler = core.verify(test_file, noCache_backend, test_ast)
+        assert(newHandler.id > 0)
+      }
+
+      "be able to execute 'stop()' without exceptions" in {
+        core.stop()
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/test/scala/ViperServerTests.scala b/src/test/scala/viper/server/core/ViperServerHttpSpec.scala
similarity index 84%
rename from src/test/scala/ViperServerTests.scala
rename to src/test/scala/viper/server/core/ViperServerHttpSpec.scala
index 55fbd3d..08f44ca 100644
--- a/src/test/scala/ViperServerTests.scala
+++ b/src/test/scala/viper/server/core/ViperServerHttpSpec.scala
@@ -1,3 +1,5 @@
+package viper.server.core
+
 // This Source Code Form is subject to the terms of the Mozilla Public
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
@@ -18,7 +20,7 @@ import viper.server.vsi.Requests._
 
 import scala.concurrent.duration._
 
-class ViperServerSpec extends AnyWordSpec with Matchers with ScalatestRouteTest {
+class ViperServerHttpSpec extends AnyWordSpec with Matchers with ScalatestRouteTest {
 
   import scala.language.postfixOps
   implicit val jsonStreamingSupport: JsonEntityStreamingSupport = EntityStreamingSupport.json()
@@ -26,12 +28,13 @@ class ViperServerSpec extends AnyWordSpec with Matchers with ScalatestRouteTest
 
   ViperServerRunner.main(Array())
 
-  private val _routsUnderTest = ViperServerRunner.viperServerHTTP.routes()
+  private val _routsUnderTest = ViperServerRunner.viperServerHttp.routes()
 
   def printRequestResponsePair(req: String, res: String): Unit = {
     println(s">>> ViperServer test request `$req` response in the following response: $res")
   }
 
+  // FIXME this does not work with SBT for some reason
   def getResourcePath(vpr_file: String): String = {
     val cross_platform_path = new File(vpr_file) getPath
     val resource = getClass.getResource(cross_platform_path)
@@ -48,14 +51,14 @@ class ViperServerSpec extends AnyWordSpec with Matchers with ScalatestRouteTest
     "\"" + fname + "\""
   }
 
-  private val verifiableFile = "viper/let.vpr"
-  private val nonExistingFile = "viper/bla.vpr"
-  private val emptyFile = "viper/empty.vpr"
+  private val verifiableFile = "src/test/resources/viper/let.vpr"
+  private val nonExistingFile = "2165e0fbd4b980436557b5a6f1a41f68.vpr"
+  private val emptyFile = "src/test/resources/viper/empty.vpr"
 
   private val tool = "silicon"
-  private val testSimpleViperCode_cmd = s"$tool --disableCaching ${getResourcePath(verifiableFile)}"
-  private val testEmptyFile_cmd = s"$tool --disableCaching ${getResourcePath(emptyFile)}"
-  private val testNonExistingFile_cmd = s"$tool --disableCaching ${getResourcePath(nonExistingFile)}"
+  private val testSimpleViperCode_cmd = s"$tool --disableCaching ${verifiableFile}"
+  private val testEmptyFile_cmd = s"$tool --disableCaching ${emptyFile}"
+  private val testNonExistingFile_cmd = s"$tool --disableCaching ${nonExistingFile}"
 
   "ViperServer" should {
     s"start a verification process using `$tool` over a small Viper program" in {
@@ -63,15 +66,16 @@ class ViperServerSpec extends AnyWordSpec with Matchers with ScalatestRouteTest
         //printRequestResponsePair(s"POST, /verify, $testSimpleViperCode_cmd", responseAs[String])
         status should ===(StatusCodes.OK)
         contentType should ===(ContentTypes.`application/json`)
+        responseAs[String] should not include ("""File not found""")
       }
     }
 
     "respond with the result for process #0" in {
       Get("/verify/0") ~> _routsUnderTest ~> check {
         //printRequestResponsePair(s"GET, /verify/0", responseAs[String])
-        responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""")
         status should ===(StatusCodes.OK)
         contentType should ===(ContentTypes.`application/json`)
+        responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""")
       }
     }
 
@@ -80,24 +84,25 @@ class ViperServerSpec extends AnyWordSpec with Matchers with ScalatestRouteTest
         //printRequestResponsePair(s"POST, /verify, $testEmptyFile_cmd", responseAs[String])
         status should ===(StatusCodes.OK)
         contentType should ===(ContentTypes.`application/json`)
+        responseAs[String] should not include ("""File not found""")
       }
     }
 
     "respond with the result for process #1" in {
       Get("/verify/1") ~> _routsUnderTest ~> check {
         //printRequestResponsePair(s"GET, /verify/1", responseAs[String])
-        responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""")
         status should ===(StatusCodes.OK)
         contentType should ===(ContentTypes.`application/json`)
+        responseAs[String] should include (s""""kind":"overall","status":"success","verifier":"$tool"""")
       }
     }
 
-    s"start another verification process using `$tool` on an inexistent file" in {
+    s"start another verification process using `$tool` on an non-existent file" in {
       Post("/verify", VerificationRequest(testNonExistingFile_cmd)) ~> _routsUnderTest ~> check {
         //printRequestResponsePair(s"POST, /verify, $testEmptyFile_cmd", responseAs[String])
-        responseAs[String] should include (s"not found")
         status should ===(StatusCodes.OK)
         contentType should ===(ContentTypes.`application/json`)
+        responseAs[String] should include (s"not found")
       }
     }