diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala
index 3ae2dd116..a7ff7d420 100644
--- a/src/main/scala/viper/gobra/Gobra.scala
+++ b/src/main/scala/viper/gobra/Gobra.scala
@@ -6,9 +6,12 @@
 
 package viper.gobra
 
+import ch.qos.logback.classic.Logger
+
 import java.nio.file.Paths
 import java.util.concurrent.ExecutionException
 import com.typesafe.scalalogging.StrictLogging
+import org.slf4j.LoggerFactory
 import viper.gobra.ast.frontend.PPackage
 import viper.gobra.ast.internal.Program
 import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, OverflowChecksTransform}
@@ -143,8 +146,9 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     implicit val _executor: GobraExecutionContext = executor
 
     val task = Future {
-      val finalConfig = getAndMergeInFileConfig(config, pkgInfo)
       for {
+        finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
+        _ = setLogLevel(finalConfig)
         parsedPackage <- performParsing(pkgInfo, finalConfig)
         typeInfo <- performTypeChecking(parsedPackage, finalConfig)
         program <- performDesugaring(parsedPackage, typeInfo, finalConfig)
@@ -194,35 +198,44 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     * These in-file command options get combined for all files and passed to ScallopGobraConfig.
     * The current config merged with the newly created config is then returned
     */
-  def getAndMergeInFileConfig(config: Config, pkgInfo: PackageInfo): Config = {
-    val inFileConfigs = config.packageInfoInputMap(pkgInfo).flatMap(input => {
+  def getAndMergeInFileConfig(config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], Config] = {
+    val inFileEitherConfigs = config.packageInfoInputMap(pkgInfo).map(input => {
       val content = input.content
       val configs = for (m <- inFileConfigRegex.findAllMatchIn(content)) yield m.group(1)
       if (configs.isEmpty) {
-        None
+        Right(None)
       } else {
         // our current "merge" strategy for potentially different, duplicate, or even contradicting configurations is to concatenate them:
         val args = configs.flatMap(configString => configString.split(" ")).toList
         // skip include dir checks as the include should only be parsed and is not resolved yet based on the current directory
-        val inFileConfig = new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = true).config
-        // modify all relative includeDirs such that they are resolved relatively to the current file:
-        val resolvedConfig = inFileConfig.copy(includeDirs = inFileConfig.includeDirs.map(
-          // it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
-          includeDir => Paths.get(input.name).getParent.resolve(includeDir.toString)))
-        Some(resolvedConfig)
+        for {
+          inFileConfig <- new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = true).config
+          resolvedConfig = inFileConfig.copy(includeDirs = inFileConfig.includeDirs.map(
+            // it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
+            includeDir => Paths.get(input.name).getParent.resolve(includeDir.toString)))
+        } yield Some(resolvedConfig)
       }
     })
+    val (errors, inFileConfigs) = inFileEitherConfigs.partitionMap(identity)
+    if (errors.nonEmpty) Left(errors.map(ConfigError))
+    else {
+      // start with original config `config` and merge in every in file config:
+      val mergedConfig = inFileConfigs.flatten.foldLeft(config) {
+        case (oldConfig, fileConfig) => oldConfig.merge(fileConfig)
+      }
+      Right(mergedConfig)
+    }
+  }
 
-    // start with original config `config` and merge in every in file config:
-    inFileConfigs.foldLeft(config){ case (oldConfig, fileConfig) => oldConfig.merge(fileConfig) }
+  private def setLogLevel(config: Config): Unit = {
+    LoggerFactory.getLogger(GoVerifier.rootLogger)
+      .asInstanceOf[Logger]
+      .setLevel(config.logLevel)
   }
 
   private def performParsing(pkgInfo: PackageInfo, config: Config): Either[Vector[VerifierError], PPackage] = {
     if (config.shouldParse) {
-      val sourcesToParse = config.packageInfoInputMap(pkgInfo).filter {
-        // only parses sources with header when running in this mode
-        p => !config.onlyFilesWithHeader || Config.sourceHasHeader(p)
-      }
+      val sourcesToParse = config.packageInfoInputMap(pkgInfo)
       Parser.parse(sourcesToParse, pkgInfo)(config)
     } else {
       Left(Vector())
@@ -295,12 +308,17 @@ object GobraRunner extends GobraFrontend with StrictLogging {
     try {
       val scallopGobraConfig = new ScallopGobraConfig(args.toSeq)
       val config = scallopGobraConfig.config
-      // Print copyright report
-      config.reporter report CopyrightReport(s"${GoVerifier.name} ${GoVerifier.version}\n${GoVerifier.copyright}")
-
-      exitCode = verifier.verifyAllPackages(config)(executor) match {
-        case VerifierResult.Failure(_) => 1
-        case _ => 0
+      exitCode = config match {
+        case Left(validationError) =>
+          logger.error(validationError)
+          1
+        case Right(config) =>
+          // Print copyright report
+          config.reporter report CopyrightReport(s"${GoVerifier.name} ${GoVerifier.version}\n${GoVerifier.copyright}")
+          verifier.verifyAllPackages(config)(executor) match {
+            case VerifierResult.Failure(_) => 1
+            case _ => 0
+          }
       }
     } catch {
       case e: UglyErrorMessage =>
diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala
index 57b489ac6..82f52a2ea 100644
--- a/src/main/scala/viper/gobra/backend/ViperBackends.scala
+++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala
@@ -67,7 +67,7 @@ object ViperBackends {
       server.getOrElse({
         var serverConfig = List("--logLevel", config.logLevel.levelStr)
         if(config.cacheFile.isDefined) {
-          serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get))
+          serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString))
         }
 
         val createdServer = new ViperCoreServer(new ViperConfig(serverConfig))(executionContext)
diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala
index 9c016fffc..cd828ba87 100644
--- a/src/main/scala/viper/gobra/frontend/Config.scala
+++ b/src/main/scala/viper/gobra/frontend/Config.scala
@@ -7,16 +7,15 @@
 package viper.gobra.frontend
 
 import java.io.File
-import java.nio.file.{Files, Path, Paths}
-import ch.qos.logback.classic.{Level, Logger}
+import java.nio.file.Path
+import ch.qos.logback.classic.Level
 import com.typesafe.scalalogging.StrictLogging
-import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, message, noMessages}
 import org.bitbucket.inkytonik.kiama.util.{FileSource, Source}
-import org.rogach.scallop.{ScallopConf, ScallopOption, listArgConverter, singleArgConverter}
-import org.slf4j.LoggerFactory
+import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter}
 import viper.gobra.backend.{ViperBackend, ViperBackends}
 import viper.gobra.GoVerifier
-import viper.gobra.frontend.Source.{FromFileSource, getPackageInfo}
+import viper.gobra.frontend.PackageResolver.FileResource
+import viper.gobra.frontend.Source.getPackageInfo
 import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter}
 import viper.gobra.util.{TypeBounds, Violation}
 import viper.silver.ast.SourcePosition
@@ -28,50 +27,79 @@ object LoggerDefaults {
 }
 
 object ConfigDefaults {
-  val DefaultGobraDirectory: String = ".gobra"
-  val DefaultTaskName: String = "gobra-task"
+  lazy val DefaultModuleName: String = ""
+  lazy val DefaultProjectRoot: File = new File("").getAbsoluteFile // current working directory
+  lazy val DefaultIncludePackages: List[String] = List.empty
+  lazy val DefaultExcludePackages: List[String] = List.empty
+  lazy val DefaultIncludeDirs: List[File] = List.empty
+  lazy val DefaultReporter: GobraReporter = StdIOReporter()
+  lazy val DefaultBackend: ViperBackend = ViperBackends.SiliconBackend
+  lazy val DefaultIsolate: List[(Path, List[Int])] = List.empty
+  lazy val DefaultChoppingUpperBound: Int = 1
+  lazy val DefaultPackageTimeout: Duration = Duration.Inf
+  lazy val DefaultZ3Exe: Option[String] = None
+  lazy val DefaultBoogieExe: Option[String] = None
+  lazy val DefaultLogLevel: Level = LoggerDefaults.DefaultLevel
+  lazy val DefaultCacheFile: Option[File] = None
+  lazy val DefaultParseOnly: Boolean = false
+  lazy val DefaultCheckOverflows: Boolean = false
+  lazy val DefaultCheckConsistency: Boolean = false
+  lazy val DefaultShouldChop: Boolean = false
+  // The go language specification states that int and uint variables can have either 32bit or 64, as long
+  // as they have the same size. This flag allows users to pick the size of int's and uints's: 32 if true,
+  // 64 bit otherwise.
+  lazy val DefaultInt32bit: Boolean = false
+  // the following option is currently not controllable via CLI as it is meaningless without a constantly
+  // running JVM. It is targeted in particular to Gobra Server and Gobra IDE
+  lazy val DefaultCacheParser: Boolean = false
+  // this option introduces a mode where Gobra only considers files with a specific annotation ("// +gobra").
+  // this is useful when verifying large packages where some files might use some unsupported feature of Gobra,
+  // or when the goal is to gradually verify part of a package without having to provide an explicit list of the files
+  // to verify.
+  lazy val DefaultOnlyFilesWithHeader: Boolean = false
+  lazy val DefaultGobraDirectory: String = ".gobra"
+  lazy val DefaultTaskName: String = "gobra-task"
 }
 
 case class Config(
-                   recursive: Boolean = false,
                    gobraDirectory: Path = Path.of(ConfigDefaults.DefaultGobraDirectory),
                    // Used as an identifier of a verification task, ideally it shouldn't change between verifications
                    // because it is used as a caching key. Additionally it should be unique when using the StatsCollector
                    taskName: String = ConfigDefaults.DefaultTaskName,
                    // Contains a mapping of packages to all input sources for that package
-                   packageInfoInputMap: Map[PackageInfo, Vector[Source]] = Map(),
-                   moduleName: String = "",
-                   includeDirs: Vector[Path] = Vector(),
-                   projectRoot: Path = Path.of(""),
-                   reporter: GobraReporter = StdIOReporter(),
-                   backend: ViperBackend = ViperBackends.SiliconBackend,
+                   packageInfoInputMap: Map[PackageInfo, Vector[Source]] = Map.empty,
+                   moduleName: String = ConfigDefaults.DefaultModuleName,
+                   includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector,
+                   projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
+                   reporter: GobraReporter = ConfigDefaults.DefaultReporter,
+                   backend: ViperBackend = ConfigDefaults.DefaultBackend,
                    isolate: Option[Vector[SourcePosition]] = None,
-                   choppingUpperBound: Int = 1,
-                   packageTimeout: Duration = Duration.Inf,
-                   z3Exe: Option[String] = None,
-                   boogieExe: Option[String] = None,
-                   logLevel: Level = LoggerDefaults.DefaultLevel,
-                   cacheFile: Option[String] = None,
+                   choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound,
+                   packageTimeout: Duration = ConfigDefaults.DefaultPackageTimeout,
+                   z3Exe: Option[String] = ConfigDefaults.DefaultZ3Exe,
+                   boogieExe: Option[String] = ConfigDefaults.DefaultBoogieExe,
+                   logLevel: Level = ConfigDefaults.DefaultLogLevel,
+                   cacheFile: Option[Path] = ConfigDefaults.DefaultCacheFile.map(_.toPath),
                    shouldParse: Boolean = true,
                    shouldTypeCheck: Boolean = true,
                    shouldDesugar: Boolean = true,
                    shouldViperEncode: Boolean = true,
-                   checkOverflows: Boolean = false,
-                   checkConsistency: Boolean = false,
+                   checkOverflows: Boolean = ConfigDefaults.DefaultCheckOverflows,
+                   checkConsistency: Boolean = ConfigDefaults.DefaultCheckConsistency,
                    shouldVerify: Boolean = true,
-                   shouldChop: Boolean = false,
+                   shouldChop: Boolean = ConfigDefaults.DefaultShouldChop,
                    // The go language specification states that int and uint variables can have either 32bit or 64, as long
                    // as they have the same size. This flag allows users to pick the size of int's and uints's: 32 if true,
                    // 64 bit otherwise.
-                   int32bit: Boolean = false,
+                   int32bit: Boolean = ConfigDefaults.DefaultInt32bit,
                    // the following option is currently not controllable via CLI as it is meaningless without a constantly
                    // running JVM. It is targeted in particular to Gobra Server and Gobra IDE
-                   cacheParser: Boolean = false,
+                   cacheParser: Boolean = ConfigDefaults.DefaultCacheParser,
                    // this option introduces a mode where Gobra only considers files with a specific annotation ("// +gobra").
                    // this is useful when verifying large packages where some files might use some unsupported feature of Gobra,
                    // or when the goal is to gradually verify part of a package without having to provide an explicit list of the files
                    // to verify.
-                   onlyFilesWithHeader: Boolean = false,
+                   onlyFilesWithHeader: Boolean = ConfigDefaults.DefaultOnlyFilesWithHeader,
 ) {
 
   def merge(other: Config): Config = {
@@ -82,7 +110,6 @@ case class Config(
     }
 
     Config(
-      recursive = recursive,
       moduleName = moduleName,
       taskName = taskName,
       gobraDirectory = gobraDirectory,
@@ -130,8 +157,152 @@ object Config {
   def sourceHasHeader(s: Source): Boolean = header.findFirstIn(s.content).nonEmpty
 }
 
+// have a look at `Config` to see an inline description of some of these parameters
+case class BaseConfig(moduleName: String = ConfigDefaults.DefaultModuleName,
+                      includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector,
+                      reporter: GobraReporter = ConfigDefaults.DefaultReporter,
+                      backend: ViperBackend = ConfigDefaults.DefaultBackend,
+                      // list of pairs of file and line numbers. Indicates which lines of files should be isolated.
+                      isolate: List[(Path, List[Int])] = ConfigDefaults.DefaultIsolate,
+                      choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound,
+                      packageTimeout: Duration = ConfigDefaults.DefaultPackageTimeout,
+                      z3Exe: Option[String] = ConfigDefaults.DefaultZ3Exe,
+                      boogieExe: Option[String] = ConfigDefaults.DefaultBoogieExe,
+                      logLevel: Level = ConfigDefaults.DefaultLogLevel,
+                      cacheFile: Option[Path] = ConfigDefaults.DefaultCacheFile.map(_.toPath),
+                      shouldParseOnly: Boolean = ConfigDefaults.DefaultParseOnly,
+                      checkOverflows: Boolean = ConfigDefaults.DefaultCheckOverflows,
+                      checkConsistency: Boolean = ConfigDefaults.DefaultCheckConsistency,
+                      int32bit: Boolean = ConfigDefaults.DefaultInt32bit,
+                      cacheParser: Boolean = ConfigDefaults.DefaultCacheParser,
+                      onlyFilesWithHeader: Boolean = ConfigDefaults.DefaultOnlyFilesWithHeader,
+                     ) {
+  def shouldParse: Boolean = true
+  def shouldTypeCheck: Boolean = !shouldParseOnly
+  def shouldDesugar: Boolean = shouldTypeCheck
+  def shouldViperEncode: Boolean = shouldDesugar
+  def shouldVerify: Boolean = shouldViperEncode
+  def shouldChop: Boolean = choppingUpperBound > 1 || isolated.exists(_.nonEmpty)
+  lazy val isolated: Option[Vector[SourcePosition]] = {
+    val positions = isolate.flatMap{ case (path, idxs) => idxs.map(idx => SourcePosition(path, idx, 0)) }
+    // if there are zero positions, no member should be isolated as verifying the empty program is uninteresting.
+    positions match {
+      case Nil => None
+      case _ => Some(positions.toVector)
+    }
+  }
+}
+
+trait RawConfig {
+  /** converts a RawConfig to an actual `Config` for Gobra. Returns Left with an error message if validation fails. */
+  def config: Either[String, Config]
+  protected def baseConfig: BaseConfig
+
+  protected def createConfig(packageInfoInputMap: Map[PackageInfo, Vector[Source]]): Config = Config(
+    packageInfoInputMap = packageInfoInputMap,
+    moduleName = baseConfig.moduleName,
+    includeDirs = baseConfig.includeDirs,
+    reporter = baseConfig.reporter,
+    backend = baseConfig.backend,
+    isolate = baseConfig.isolated,
+    choppingUpperBound = baseConfig.choppingUpperBound,
+    packageTimeout = baseConfig.packageTimeout,
+    z3Exe = baseConfig.z3Exe,
+    boogieExe = baseConfig.boogieExe,
+    logLevel = baseConfig.logLevel,
+    cacheFile = baseConfig.cacheFile,
+    shouldParse = baseConfig.shouldParse,
+    shouldTypeCheck = baseConfig.shouldTypeCheck,
+    shouldDesugar = baseConfig.shouldDesugar,
+    shouldViperEncode = baseConfig.shouldViperEncode,
+    checkOverflows = baseConfig.checkOverflows,
+    checkConsistency = baseConfig.checkConsistency,
+    shouldVerify = baseConfig.shouldVerify,
+    shouldChop = baseConfig.shouldChop,
+    int32bit = baseConfig.int32bit,
+    cacheParser = baseConfig.cacheParser,
+    onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
+}
+
+/**
+  * Special case where we do not enforce that inputs (be it files, directories or recursive files) have to be provided.
+  * This is for example used when parsing in-file configs.
+  */
+case class NoInputModeConfig(baseConfig: BaseConfig) extends RawConfig {
+  override lazy val config: Either[String, Config] = Right(createConfig(Map.empty))
+}
+
+case class FileModeConfig(inputFiles: Vector[Path], baseConfig: BaseConfig) extends RawConfig {
+  override lazy val config: Either[String, Config] = {
+    val sources = inputFiles.map(path => FileSource(path.toString))
+    if (sources.isEmpty) Left(s"no input files have been provided")
+    else {
+      // we do not check whether the provided files all belong to the same package
+      // instead, we trust the programmer that she knows what she's doing.
+      // If they do not belong to the same package, Gobra will report an error after parsing.
+      // we simply use the first source's package info to create a single map entry:
+      val packageInfoInputMap = Map(getPackageInfo(sources.head, inputFiles.head) -> sources)
+      Right(createConfig(packageInfoInputMap))
+    }
+  }
+}
+
+trait PackageAndRecursiveModeConfig extends RawConfig {
+  def getSources(directory: Path, recursive: Boolean, onlyFilesWithHeader: Boolean): Vector[Source] = {
+    val inputResource = FileResource(directory)
+    PackageResolver.getSourceFiles(inputResource, recursive = recursive, onlyFilesWithHeader = onlyFilesWithHeader).map { resource =>
+      val source = resource.asSource()
+      // we do not need the underlying resources anymore, thus close them:
+      resource.close()
+      source
+    }
+  }
+}
+
+case class PackageModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
+                             inputDirectories: Vector[Path], baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig {
+  override lazy val config: Either[String, Config] = {
+    val (errors, mappings) = inputDirectories.map { directory =>
+      val sources = getSources(directory, recursive = false, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
+      // we do not check whether the provided files all belong to the same package
+      // instead, we trust the programmer that she knows what she's doing.
+      // If they do not belong to the same package, Gobra will report an error after parsing.
+      // we simply use the first source's package info to create a single map entry:
+      if (sources.isEmpty) Left(s"no sources found in directory ${directory}")
+      else Right((getPackageInfo(sources.head, projectRoot), sources))
+    }.partitionMap(identity)
+    if (errors.length == 1) Left(errors.head)
+    else if (errors.nonEmpty) Left(s"multiple errors have been found while localizing sources: ${errors.mkString(", ")}")
+    else Right(createConfig(mappings.toMap))
+  }
+}
+
+case class RecursiveModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
+                               includePackages: List[String] = ConfigDefaults.DefaultIncludePackages,
+                               excludePackages: List[String] = ConfigDefaults.DefaultExcludePackages,
+                               baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig {
+  override lazy val config: Either[String, Config] = {
+    val pkgMap = getSources(projectRoot, recursive = true, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
+      .groupBy(source => getPackageInfo(source, projectRoot))
+      // filter packages:
+      .filter { case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name) }
+      // filter packages with zero source files:
+      .filter { case (_, pkgFiles) => pkgFiles.nonEmpty }
+    if (pkgMap.isEmpty) {
+      Left(s"No packages have been found that should be verified")
+    } else {
+      Right(createConfig(pkgMap))
+    }
+  }
+}
+
+/**
+  * This represents Gobra's CLI interface.
+  * The idea is to just perform the necessary validations to convert the inputs into a `RawConfig`.
+  * All other validations will be deferred and performed on `RawConfig` before converting it to the actual Gobra config.
+  */
 class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = false, skipIncludeDirChecks: Boolean = false)
-    extends ScallopConf(arguments)
+  extends ScallopConf(arguments)
     with StrictLogging {
 
   /**
@@ -146,7 +317,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   )
 
   banner(
-    s""" Usage: ${GoVerifier.name} -i <input-files or a single package name> [OPTIONS]
+    s""" Usage: ${GoVerifier.name} -i <input-files> [OPTIONS] OR
+       |  ${GoVerifier.name} -p <directory> [OPTIONS]
        |
        | Options:
        |""".stripMargin
@@ -155,30 +327,58 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   /**
     * Command-line options
     */
+  /** input is a list of strings as opposed to a list of files because line positions can optionally be provided */
   val input: ScallopOption[List[String]] = opt[List[String]](
     name = "input",
-    descr = "List of Gobra programs, a project directory or a single package name to verify",
+    descr = "List of files to verify. Optionally, specific members can be verified by passing their line numbers (e.g. foo.gobra@42,111 corresponds to the members in lines 42 and 111)",
     short = 'i'
   )
+  /**
+    * List of input files together with their specified line numbers.
+    * Specified line numbers are removed from their corresponding input argument.
+    */
+  val cutInputWithIdxs: ScallopOption[List[(File, List[Int])]] = input.map(_.map{ arg =>
+    val pattern = """(.*)@(\d+(?:,\d+)*)""".r
+    arg match {
+      case pattern(prefix, idxs) =>
+        (new File(prefix), idxs.split(',').toList.map(_.toInt))
+
+      case _ => (new File(arg), List.empty[Int])
+    }
+  })
+  /** list of input files without line numbers */
+  val cutInput: ScallopOption[List[File]] = cutInputWithIdxs.map(_.map(_._1))
+
+  val directory: ScallopOption[List[File]] = opt[List[File]](
+    name = "directory",
+    descr = "List of directories to verify",
+    short = 'p'
+  )
 
   val recursive: ScallopOption[Boolean] = opt[Boolean](
     name = "recursive",
     descr = "Verify nested packages recursively",
-    default = Some(false),
     short = 'r'
   )
 
-  val includePackages: ScallopOption[List[String]] = opt[List[String]](
+  val projectRoot: ScallopOption[File] = opt[File](
+    name = "projectRoot",
+    descr = "The root directory of the project",
+    default = Some(ConfigDefaults.DefaultProjectRoot),
+    noshort = true
+  )
+
+  val inclPackages: ScallopOption[List[String]] = opt[List[String]](
     name = "includePackages",
     descr = "Packages to verify. All packages found in the specified directories are verified by default.",
-    default = Some(List.empty),
-    short = 'p'
+    default = Some(ConfigDefaults.DefaultIncludePackages),
+    noshort = true
   )
 
-  val excludePackages: ScallopOption[List[String]] = opt[List[String]](
+  val exclPackages: ScallopOption[List[String]] = opt[List[String]](
     name = "excludePackages",
     descr = "Packages to ignore. These packages will not be verified, even if they are found in the specified directories.",
-    default = Some(List.empty),
+    default = Some(ConfigDefaults.DefaultExcludePackages),
     noshort = true
   )
 
@@ -192,15 +392,16 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   val module: ScallopOption[String] = opt[String](
     name = "module",
     descr = "Name of current module that should be used for resolving imports",
-    default = Some("")
+    default = Some(ConfigDefaults.DefaultModuleName)
   )
 
   val include: ScallopOption[List[File]] = opt[List[File]](
     name = "include",
     short = 'I',
     descr = "Uses the provided directories to perform package-related lookups before falling back to $GOPATH",
-    default = Some(List())
-  )(listArgConverter(dir => new File(dir)))
+    default = Some(ConfigDefaults.DefaultIncludeDirs)
+  )
+  lazy val includeDirs: Vector[Path] = include.toOption.map(_.map(_.toPath).toVector).getOrElse(Vector())
 
   val backend: ScallopOption[ViperBackend] = choice(
     choices = Seq("SILICON", "CARBON", "VSWITHSILICON", "VSWITHCARBON"),
@@ -226,7 +427,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     name = "logLevel",
     choices = Seq("ALL", "TRACE", "DEBUG", "INFO", "WARN", "ERROR", "OFF"),
     descr = "Specifies the log level. The default is OFF.",
-    default = Some(if (debug()) Level.DEBUG.toString else LoggerDefaults.DefaultLevel.toString),
+    default = Some(if (debug()) Level.DEBUG.toString else ConfigDefaults.DefaultLogLevel.toString),
     noshort = true
   ).map{arg => Level.toLevel(arg)}
 
@@ -268,14 +469,14 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   val parseOnly: ScallopOption[Boolean] = opt[Boolean](
     name = "parseOnly",
     descr = "Perform only the parsing step",
-    default = Some(false),
+    default = Some(ConfigDefaults.DefaultParseOnly),
     noshort = true
   )
 
   val chopUpperBound: ScallopOption[Int] = opt[Int](
     name = "chop",
     descr = "Number of parts the generated verification condition is split into (at most)",
-    default = Some(1),
+    default = Some(ConfigDefaults.DefaultChoppingUpperBound),
     noshort = true
   )
 
@@ -285,63 +486,61 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     default = None,
     noshort = true
   )
+  lazy val packageTimeoutDuration: Duration = packageTimeout.toOption match {
+    case Some(d) => Duration(d)
+    case _ => Duration.Inf
+  }
 
   val z3Exe: ScallopOption[String] = opt[String](
     name = "z3Exe",
     descr = "The Z3 executable",
-    default = None,
+    default = ConfigDefaults.DefaultZ3Exe,
     noshort = true
   )
 
   val boogieExe: ScallopOption[String] = opt[String](
     name = "boogieExe",
     descr = "The Boogie executable",
-    default = None,
+    default = ConfigDefaults.DefaultBoogieExe,
     noshort = true
   )
 
   val checkOverflows: ScallopOption[Boolean] = opt[Boolean](
     name = "overflow",
     descr = "Find expressions that may lead to integer overflow",
-    default = Some(false),
+    default = Some(ConfigDefaults.DefaultCheckOverflows),
     noshort = false
   )
 
-  val rootDirectory: ScallopOption[Path] = opt[Path](
-    name = "projectRoot",
-    descr = "The root directory of the project",
-    default = None,
-    noshort = true
-  )
-
-  val cacheFile: ScallopOption[String] = opt[String](
+  val cacheFile: ScallopOption[File] = opt[File](
     name = "cacheFile",
     descr = "Cache file to be used by Viper Server",
-    default = None,
+    default = ConfigDefaults.DefaultCacheFile,
     noshort = true
   )
 
   val int32Bit: ScallopOption[Boolean] = opt[Boolean](
     name = "int32",
     descr = "Run with 32-bit sized integers (the default is 64-bit ints)",
-    default = Some(false),
+    default = Some(ConfigDefaults.DefaultInt32bit),
     noshort = false
   )
 
   val onlyFilesWithHeader: ScallopOption[Boolean] = opt[Boolean](
     name = "onlyFilesWithHeader",
     descr = s"When enabled, Gobra only looks at files that contain the header comment '${Config.prettyPrintedHeader}'",
-    default = Some(false),
+    default = Some(ConfigDefaults.DefaultOnlyFilesWithHeader),
     noshort = false
   )
 
   val checkConsistency: ScallopOption[Boolean] = opt[Boolean](
     name = "checkConsistency",
     descr = "Perform consistency checks on the generated Viper code",
-    default = Some(false),
+    default = Some(ConfigDefaults.DefaultCheckConsistency),
     noshort = true
   )
 
+
   /**
     * Exception handling
     */
@@ -350,251 +549,78 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     */
 
   /** Argument Dependencies */
-  if (!isInputOptional) {
-    requireAtLeastOne(input)
+  if (isInputOptional) {
+    mutuallyExclusive(input, directory, recursive)
+  } else {
+    // either `input`, `directory` or `recursive` must be provided but not both.
+    // this also checks that at least one file or directory is provided in the case of `input` and `directory`.
+    requireOne(input, directory, recursive)
   }
 
+  // `inclPackages` and `exclPackages` only make sense when `recursive` is specified, `projectRoot` can only be used in `directory` or `recursive` mode.
+  // Thus, we restrict their use:
+  conflicts(input, List(projectRoot, inclPackages, exclPackages))
+  conflicts(directory, List(inclPackages, exclPackages))
 
   /** File Validation */
-  def validateInput(inputOption: ScallopOption[List[String]],
-                    recOption: ScallopOption[Boolean],
-                    rootDirectoryOption: ScallopOption[Path],
-                    includeOption: ScallopOption[List[File]],
-                    includePkgOption: ScallopOption[List[String]],
-                    excludePkgOption: ScallopOption[List[String]]): Unit =
-    validateOpt(inputOption, recOption, rootDirectoryOption, includeOption, includePkgOption, excludePkgOption) {
-      (inputOpt, recOpt, rootDirectoryOpt, includeOpt, includePkgOpt, excludePkgOpt) =>
-      def checkConversion(input: List[String]): Either[String, Vector[Path]] = {
-        def validateSources(sources: Vector[Source]): Either[Messages, Vector[Path]] = {
-          val (remainingSources, paths) = sources.partitionMap {
-            case FileSource(name, _) => Right(Paths.get(name))
-            case FromFileSource(path, _, _) => Right(path)
-            case s => Left(s)
-          }
-          if (remainingSources.isEmpty) Right(paths)
-          else Left(message(null, s"Expected file sources but got $remainingSources"))
-        }
-
-        val shouldParseRecursively = recOpt.getOrElse(false)
-        val inputValidationMsgs = InputConverter.validate(input, shouldParseRecursively)
-
-        lazy val projectRoot = rootDirectoryOpt.getOrElse(
-          includeOpt.flatMap(_.headOption.map(_.toPath)).getOrElse(Path.of(""))
-        )
-
-        val paths = for {
-          _ <- if (inputValidationMsgs.isEmpty) Right(()) else Left(inputValidationMsgs)
-          sources = InputConverter.convert(input, shouldParseRecursively, projectRoot, includePkgOpt.getOrElse(List()), excludePkgOpt.getOrElse(List()))
-          paths <- validateSources(sources.values.flatten.toVector)
-        } yield paths
-
-        paths.left.map(msgs => s"The following errors have occurred: ${msgs.map(_.label).mkString(",")}")
-      }
-
-      def atLeastOnePath(paths: Vector[Path]): Either[String, Unit] = {
-        if (paths.nonEmpty || isInputOptional) Right(()) else Left(s"Package resolution has not found any files for verification - are you using '.${PackageResolver.gobraExtension}' or '.${PackageResolver.goExtension}' as file extension?")
-      }
-
-      def pathsExist(paths: Vector[Path]): Either[String, Unit] = {
-        val notExisting = paths.filterNot(Files.exists(_))
-        if (notExisting.isEmpty) Right(()) else Left(s"Files '${notExisting.mkString(",")}' do not exist")
-      }
-
-      def pathsAreFilesOrDirectories(paths: Vector[Path]): Either[String, Unit] = {
-        val notFilesOrDirectories = paths.filterNot(file => Files.isRegularFile(file) || Files.isDirectory(file))
-        if (notFilesOrDirectories.isEmpty) Right(()) else Left(s"Files '${notFilesOrDirectories.mkString(",")}' are neither files or directories")
-      }
-
-      def pathsAreReadable(paths: Vector[Path]): Either[String, Unit] = {
-        val notReadable = paths.filterNot(Files.isReadable)
-        if (notReadable.isEmpty) Right(()) else Left(s"Files '${notReadable.mkString(",")}' are not readable")
-      }
-
-      // perform the following checks:
-      // - validate fileOpt using includeOpt
-      // - convert fileOpt using includeOpt
-      //  - result should be non-empty, exist, be files and be readable
-      val input: List[String] = inputOpt.getOrElse(List())
-      for {
-        convertedFiles <- checkConversion(input)
-        _ <- atLeastOnePath(convertedFiles)
-        _ <- pathsExist(convertedFiles)
-        _ <- pathsAreFilesOrDirectories(convertedFiles)
-        _ <- pathsAreReadable(convertedFiles)
-      } yield ()
-  }
-
+  validateFilesExist(cutInput)
+  validateFilesIsFile(cutInput)
+  validateFilesExist(directory)
+  validateFilesIsDirectory(directory)
+  validateFileExists(projectRoot)
+  validateFileIsDirectory(projectRoot)
   if (!skipIncludeDirChecks) {
     validateFilesExist(include)
     validateFilesIsDirectory(include)
   }
 
-  // List of input arguments together with their specified line numbers.
-  // Specified line numbers are removed from their corresponding input argument.
-  val cutInputWithIdxs: ScallopOption[List[(String, List[Int])]] = input.map(_.map{ arg =>
-    val pattern = """(.*)@(\d+(?:,\d+)*)""".r
-    arg match {
-      case pattern(prefix, idxs) =>
-        (prefix, idxs.split(',').toList.map(_.toInt))
-
-      case _ => (arg, List.empty[Int])
-    }
-  })
-  val cutInput: ScallopOption[List[String]] = cutInputWithIdxs.map(_.map(_._1))
-
-  validateInput(input, recursive, rootDirectory, include, includePackages, excludePackages)
-
-  // cache file should only be usable when using viper server
-  validateOpt (backend, cacheFile) {
-    case (Some(_: ViperBackends.ViperServerWithSilicon), Some(_)) => Right(())
-    case (Some(_: ViperBackends.ViperServerWithCarbon), Some(_)) => Right(())
-    case (_, None) => Right(())
-    case (_, Some(_)) => Left("Cache file can only be specified when the backend uses Viper Server")
-  }
+  verify()
 
-  validateOpt (gobraDirectory) {
-    case Some(dir) =>
-      // Set up gobra directory
-      val gobraDirectory = dir.toFile
-      if(!gobraDirectory.exists && !gobraDirectory.mkdir()) {
-        Left( s"Could not create directory $gobraDirectory")
-      } else if (!gobraDirectory.isDirectory) {
-        Left(s"$dir is not a directory")
-      } else if (!gobraDirectory.canRead) {
-        Left(s"Couldn't read gobra directory $dir")
-      } else if (!gobraDirectory.canWrite) {
-        Left(s"Couldn't write to gobra directory $dir")
-      } else {
-        Right(())
-      }
-    case _ => Right(())
+  lazy val config: Either[String, Config] = rawConfig.config
+
+  // note that we use `recursive.isSupplied` instead of `recursive.toOption` because it defaults to `Some(false)` if it
+  // was not provided by the user. Specifying a different default value does not seem to be respected.
+  private lazy val rawConfig: RawConfig = (cutInputWithIdxs.toOption, directory.toOption, recursive.isSupplied) match {
+    case (Some(inputsWithIdxs), None, false) => fileModeConfig(inputsWithIdxs)
+    case (None, Some(dirs), false) => packageModeConfig(dirs)
+    case (None, None, true) => recursiveModeConfig()
+    case (None, None, false) =>
+      Violation.violation(isInputOptional, "the configuration mode should be one of file, package or recursive unless inputs are optional")
+      noInputModeConfig()
+    case _ => Violation.violation(s"multiple modes have been found, which should have been caught by input validation")
   }
 
-  validateOpt (packageTimeout) {
-    case Some(s) => try {
-      Right(Duration(s))
-    } catch {
-      case e: NumberFormatException => Left(s"Couldn't parse package timeout: " + e.getMessage)
-    }
-    case None => Right(())
-  }
-
-  lazy val packageTimeoutDuration: Duration = packageTimeout.toOption match {
-    case Some(d) => Duration(d)
-    case _ => Duration.Inf
+  private def fileModeConfig(cutInputWithIdxs: List[(File, List[Int])]): FileModeConfig = {
+    val cutPathsWithIdxs = cutInputWithIdxs.map { case (file, lineNrs) => (file.toPath, lineNrs) }
+    FileModeConfig(
+      inputFiles = cutPathsWithIdxs.map(_._1).toVector,
+      baseConfig = baseConfig(cutPathsWithIdxs)
+    )
   }
 
-  verify()
-
-  lazy val includeDirs: Vector[Path] = include.toOption.map(_.map(_.toPath).toVector).getOrElse(Vector())
-
-  // Take the user input for the project root or fallback to the fist include directory or the current directory
-  lazy val projectRoot: Path = rootDirectory.getOrElse(
-    includeDirs.headOption.getOrElse(Path.of(""))
+  private def packageModeConfig(dirs: List[File]): PackageModeConfig = PackageModeConfig(
+    inputDirectories = dirs.map(_.toPath).toVector,
+    projectRoot = projectRoot().toPath,
+    // we currently do not offer a way via CLI to pass isolate information to Gobra in the package mode
+    baseConfig = baseConfig(ConfigDefaults.DefaultIsolate),
   )
 
-  lazy val inputPackageMap: Map[PackageInfo, Vector[Source]] = InputConverter.convert(
-    input.toOption.getOrElse(List()),
-    recursive.getOrElse(false),
-    projectRoot,
-    includePackages.getOrElse(List()),
-    excludePackages.getOrElse(List())
+  private def recursiveModeConfig(): RecursiveModeConfig = RecursiveModeConfig(
+    projectRoot = projectRoot().toPath,
+    includePackages = inclPackages(),
+    excludePackages = exclPackages(),
+    // we currently do not offer a way via CLI to pass isolate information to Gobra in the recursive mode
+    baseConfig(ConfigDefaults.DefaultIsolate),
   )
-  lazy val isolated: Option[Vector[SourcePosition]] =
-    InputConverter.isolatedPosition(cutInputWithIdxs.toOption) match {
-      case Nil => None
-      case positions => Some(positions.toVector)
-    }
-
-
-  /** set log level */
-
-  LoggerFactory.getLogger(GoVerifier.rootLogger)
-    .asInstanceOf[Logger]
-    .setLevel(logLevel())
-
-  def shouldParse: Boolean = true
-  def shouldTypeCheck: Boolean = !parseOnly.getOrElse(true)
-  def shouldDesugar: Boolean = shouldTypeCheck
-  def shouldViperEncode: Boolean = shouldDesugar
-  def shouldVerify: Boolean = shouldViperEncode
-  def shouldChop: Boolean = chopUpperBound.toOption.exists(_ > 1) || isolated.exists(_.nonEmpty)
-
-  private object InputConverter {
-
-    def validate(inputs: List[String], recursive: Boolean): Messages = {
-      val files = inputs flatMap (file => getAllGobraFiles(file, recursive))
-      files match {
-        case files if files.nonEmpty => noMessages
-        case _ if isInputOptional => noMessages
-        // error states
-        case files if files.isEmpty => message(null, s"no files found in the specified input (use -r to traverse directories)")
-        case c => Violation.violation(s"This case should be unreachable, but got $c")
-      }
-    }
-
-    def convert(input: List[String], recursive: Boolean, projectRoot: Path, includePackages: List[String], excludePackages: List[String]): Map[PackageInfo, Vector[Source]] = {
-      val sources = parseInputStrings(input.toVector, recursive)
-      sources.groupBy(src => getPackageInfo(src, projectRoot))
-        .filter({case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name)})
-    }
-
-    /**
-     * Parses all provided inputs and returns a list of all gobra files found
-     *
-     */
-    private def parseInputStrings(inputs: Vector[String], recursive: Boolean): Vector[Source] = {
-      inputs.flatMap(input => getAllGobraFiles(input, recursive))
-        .map(file => FileSource(file.getPath))
-    }
 
-    /**
-     * Gets all gobra files in a input location. If the location is a file that ends in ".<ext>" it is returned.
-     * If it is a directory, all files contained in it, ending in ".<ext>", are returned.
-     *
-     * @param recursive if true, directories are traversed recursively
-     * @return a Vector of the resolved gobra files
-     */
-    private def getAllGobraFiles(input: String, recursive: Boolean): Vector[File] =
-      input match {
-        case PackageResolver.inputFileRegex(filename) => Vector(new File(filename))
-        case dirname => getInputFilesInDir(new File(dirname), recursive)
-      }
-
-    /**
-     * Gets all files with a go/gobra extension inside this directory
-     *
-     * @param directory directory to look for files
-     * @param recursive traverse subdirectories if this is set to true
-     * @return a List of go/gobra files
-     */
-    private def getInputFilesInDir(directory: File, recursive: Boolean): Vector[File] = {
-      Violation.violation(directory.exists && directory.isDirectory, "getInputFilesInDir didn't receive a directory as input: " + directory.toString)
-      directory.listFiles()
-        // Filters out all files that aren't either go/gobra files or directories (if recursive is set)
-        .filter(file => (file.isDirectory && recursive) || PackageResolver.inputFileRegex.matches(file.getName))
-        .flatMap(file => if (file.isDirectory) getInputFilesInDir(file, recursive) else List(file))
-        .toVector
-    }
-
-    def isolatedPosition(cutInputWithIdxs: Option[List[(String, List[Int])]]): List[SourcePosition] = {
-      cutInputWithIdxs.map(_.flatMap { case (input, idxs) =>
-        getAllGobraFiles(input, recursive = false) match {
-          // only go and gobra files and not directories can have a position
-          case Vector(file) => idxs.map(idx => SourcePosition(file.toPath, idx, 0))
-          case _ => List.empty
-        }
-      }).getOrElse(List.empty)
-    }
-  }
+  private def noInputModeConfig(): NoInputModeConfig = NoInputModeConfig(
+    // we currently do not offer a way via CLI to pass isolate information to Gobra in the recursive mode
+    baseConfig(ConfigDefaults.DefaultIsolate),
+  )
 
-  lazy val config: Config = Config(
-    recursive = recursive(),
-    gobraDirectory = gobraDirectory(),
-    packageInfoInputMap = inputPackageMap,
+  private def baseConfig(isolate: List[(Path, List[Int])]): BaseConfig = BaseConfig(
     moduleName = module(),
     includeDirs = includeDirs,
-    projectRoot = projectRoot,
     reporter = FileWriterReporter(
       unparse = unparse(),
       eraseGhost = eraseGhost(),
@@ -603,22 +629,18 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
       printInternal = printInternal(),
       printVpr = printVpr()),
     backend = backend(),
-    isolate = isolated,
+    isolate = isolate,
     choppingUpperBound = chopUpperBound(),
     packageTimeout = packageTimeoutDuration,
     z3Exe = z3Exe.toOption,
     boogieExe = boogieExe.toOption,
     logLevel = logLevel(),
-    cacheFile = cacheFile.toOption,
-    shouldParse = shouldParse,
-    shouldTypeCheck = shouldTypeCheck,
-    shouldDesugar = shouldDesugar,
-    shouldViperEncode = shouldViperEncode,
+    cacheFile = cacheFile.toOption.map(_.toPath),
+    shouldParseOnly = parseOnly(),
     checkOverflows = checkOverflows(),
-    int32bit = int32Bit(),
-    shouldVerify = shouldVerify,
-    shouldChop = shouldChop,
     checkConsistency = checkConsistency(),
-    onlyFilesWithHeader = onlyFilesWithHeader(),
+    int32bit = int32Bit(),
+    cacheParser = false, // caching does not make sense when using the CLI. Thus, we simply set it to `false`
+    onlyFilesWithHeader = onlyFilesWithHeader()
   )
 }
diff --git a/src/main/scala/viper/gobra/frontend/PackageResolver.scala b/src/main/scala/viper/gobra/frontend/PackageResolver.scala
index 7dae19b4e..9577c6c1d 100644
--- a/src/main/scala/viper/gobra/frontend/PackageResolver.scala
+++ b/src/main/scala/viper/gobra/frontend/PackageResolver.scala
@@ -46,14 +46,13 @@ object PackageResolver {
   /**
     * Resolves a package name (i.e. import path) to specific input sources
     * @param importTarget
-    * @param moduleName name of the module under verification
-    * @param includeDirs list of directories that will be used for package resolution before falling back to $GOPATH
+    * @param config
     * @return list of sources belonging to the package (right) or an error message (left) if no directory could be found
     *         or the directory contains input files having different package clauses
     */
-  def resolveSources(importTarget: AbstractImport, moduleName: String, includeDirs: Vector[Path]): Either[String, Vector[ResolveSourcesResult]] = {
+  def resolveSources(importTarget: AbstractImport)(config: Config): Either[String, Vector[ResolveSourcesResult]] = {
     for {
-      resources <- resolve(importTarget, moduleName, includeDirs)
+      resources <- resolve(importTarget)(config)
       sources = resources.map(r => ResolveSourcesResult(r.asSource(), r.builtin))
       // we do no longer need the resources, so we close them:
       _ = resources.foreach(_.close())
@@ -63,24 +62,15 @@ object PackageResolver {
   /**
     * Resolves a package name (i.e. import path) to specific input files
     * @param importTarget
-    * @param moduleName name of the module under verification
-    * @param includeDirs list of directories that will be used for package resolution before falling back to $GOPATH
+    * @param config
     * @return list of files belonging to the package (right) or an error message (left) if no directory could be found
     *         or the directory contains input files having different package clauses
     */
-  private def resolve(importTarget: AbstractImport, moduleName: String, includeDirs: Vector[Path]): Either[String, Vector[InputResource]] = {
-    val sourceFiles = for {
-      // pkgDir stores the path to the directory that should contain source files belonging to the desired package
-      pkgDir <- getLookupPath(importTarget, moduleName, includeDirs)
-      sourceFiles = getSourceFiles(pkgDir)
-    } yield sourceFiles
-
-    sourceFiles.foreach(checkPackageClauses(_, importTarget))
-
+  private def resolve(importTarget: AbstractImport)(config: Config): Either[String, Vector[InputResource]] = {
     for {
       // pkgDir stores the path to the directory that should contain source files belonging to the desired package
-      pkgDir <- getLookupPath(importTarget, moduleName, includeDirs)
-      sourceFiles = getSourceFiles(pkgDir)
+      pkgDir <- getLookupPath(importTarget)(config)
+      sourceFiles = getSourceFiles(pkgDir, onlyFilesWithHeader = config.onlyFilesWithHeader)
       // check whether all found source files belong to the same package (the name used in the package clause can
       // be absolutely independent of the import path)
       // in case of error, iterate over all resources and close them
@@ -97,17 +87,18 @@ object PackageResolver {
     * The returned package name can be used as qualifier for the implicitly qualified import.
     *
     * @param n implicitely qualified import for which a qualifier should be resolved
-    * @param moduleName name of the module under verification
-    * @param includeDirs list of directories that will be used for package resolution before falling back to $GOPATH
+    * @param config
     * @return qualifier with which members of the imported package can be accessed (right) or an error message (left)
     *         if no directory could be found or the directory contains input files having different package clauses
     */
-  def getQualifier(n: PImplicitQualifiedImport, moduleName: String, includeDirs: Vector[Path]): Either[String, String] = {
+  def getQualifier(n: PImplicitQualifiedImport)(config: Config): Either[String, String] = {
     val importTarget = RegularImport(n.importPath)
     for {
       // pkgDir stores the path to the directory that should contain source files belonging to the desired package
-      pkgDir <- getLookupPath(importTarget, moduleName, includeDirs)
-      sourceFiles = getSourceFiles(pkgDir)
+      pkgDir <- getLookupPath(importTarget)(config)
+      // note that we ignore the "onlyFilesWithHeader" option provided in `config`, because we still want to consider
+      // all source files when resolving the right qualifier for a package:
+      sourceFiles = getSourceFiles(pkgDir, onlyFilesWithHeader = false)
       // check whether all found source files belong to the same package (the name used in the package clause can
       // be absolutely independent of the import path)
       pkgName <- checkPackageClauses(sourceFiles, importTarget)
@@ -161,7 +152,9 @@ object PackageResolver {
   /**
     * Resolves import target using includeDirs to a directory which exists and from which source files should be retrieved
     */
-  private def getLookupPath(importTarget: AbstractImport, moduleName: String, includeDirs: Vector[Path]): Either[String, InputResource] = {
+  private def getLookupPath(importTarget: AbstractImport)(config: Config): Either[String, InputResource] = {
+    val moduleName = config.moduleName
+    val includeDirs = config.includeDirs
     val moduleNameWithTrailingSlash = if (moduleName.nonEmpty && !moduleName.endsWith("/")) s"$moduleName/" else moduleName
     importTarget match {
       case BuiltInImport => getBuiltInResource.toRight(s"Loading builtin package has failed")
@@ -194,27 +187,52 @@ object PackageResolver {
   private def shouldIgnoreResource(r: InputResource): Boolean = {
     val path = r.path.toString
     // files inside a directory named "testdata" should be ignored
-    val testDataDir = """.*/testdata($|/)""".r
+    val testDataDir = """.*/testdata(?:$|/.*)""".r
     // test files in Go have their name terminating in "_test.go"
     val testFilesEnding = """.*_test.go$""".r
     testFilesEnding.matches(path) || testDataDir.matches(path)
   }
 
   /**
-    * Returns the source files with file extension 'gobraExtension' or 'goExtension' in the input resource which
-    * are not test files and are not in a directory with name 'testdata'
+    * Decides whether an input resource should be considered by Gobra when considering only files with headers.
     */
-  private def getSourceFiles(input: InputResource): Vector[InputResource] = {
-    val dirContent = input.listContent()
-    val res = dirContent.filter { resource =>
-      val isRegular = Files.isRegularFile(resource.path)
-      // only consider files with the particular extension
-      val validExtension = FilenameUtils.getExtension(resource.path.toString) == gobraExtension ||
-        FilenameUtils.getExtension(resource.path.toString) == goExtension
-      val shouldBeConsidered = !shouldIgnoreResource(resource)
-      isRegular && validExtension && shouldBeConsidered
+  private def isResourceWithHeader(resource: InputResource): Boolean = {
+    resource match {
+      case i: InputResource if i.builtin =>
+        // standard library methods defined in stubs are always considered by Gobra
+        true
+      case _ => Config.sourceHasHeader(resource.asSource())
     }
-    (dirContent :+ input).foreach({
+  }
+
+  /**
+    * Returns the source files with file extension 'gobraExtension' or 'goExtension' in the input resource which
+    * are not test files and are not in a directory with name 'testdata'.
+    * Input can also be a file in which case the same file is returned if it passes all tests
+    */
+  def getSourceFiles(input: InputResource, recursive: Boolean = false, onlyFilesWithHeader: Boolean = false): Vector[InputResource] = {
+    // get content of directory if it's a directory, otherwise just return the file itself
+    val dirContentOrInput = if (Files.isDirectory(input.path)) { input.listContent() } else { Vector(input) }
+    val res = dirContentOrInput
+      .flatMap { resource =>
+        if (recursive && Files.isDirectory(resource.path)) {
+          getSourceFiles(resource, recursive = recursive, onlyFilesWithHeader = onlyFilesWithHeader)
+        } else if (Files.isRegularFile(resource.path)) {
+          // ignore files that are not Go or Gobra sources, have a filename or are placed in a directory that should be
+          // ignored according to the Go spec or that do not have a header we require them to have:
+          lazy val validExtension = FilenameUtils.getExtension(resource.path.toString) == gobraExtension ||
+            FilenameUtils.getExtension(resource.path.toString) == goExtension
+          lazy val shouldBeConsidered = !shouldIgnoreResource(resource)
+          // note that the following condition has to be lazily evaluated to avoid reading the file's content and applying
+          // a regex. The first part in particular can fail when the file does not contain text!
+          lazy val headerIsMissing = onlyFilesWithHeader && !isResourceWithHeader(resource)
+          if (validExtension && shouldBeConsidered && !headerIsMissing) Vector(resource) else Vector()
+        } else {
+          Vector()
+        }
+      }
+    // close all resource that are no longer needed:
+    (dirContentOrInput.toSet + input).foreach({
       case resource if !res.contains(resource) => resource.close()
       case _ =>
     })
diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 604284098..8ff2c1ffa 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -226,7 +226,7 @@ object Parser {
 
       def replace(n: PImplicitQualifiedImport): Option[PExplicitQualifiedImport] = {
         val qualifier = for {
-          qualifierName <- PackageResolver.getQualifier(n, config.moduleName, config.includeDirs)
+          qualifierName <- PackageResolver.getQualifier(n)(config)
           // create a new PIdnDef node and set its positions according to the old node (PositionedRewriter ensures that
           // the same happens for the newly created PExplicitQualifiedImport)
           idnDef = PIdnDef(qualifierName)
diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala
index 9c524b1c9..663760785 100644
--- a/src/main/scala/viper/gobra/frontend/Source.scala
+++ b/src/main/scala/viper/gobra/frontend/Source.scala
@@ -13,7 +13,7 @@ import viper.gobra.util.Violation
 import viper.silver.ast.SourcePosition
 
 import java.security.MessageDigest
-import java.util.{Base64, Objects}
+import java.util.Objects
 import scala.io.BufferedSource
 
 /**
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala
index ebb738759..b68269344 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala
@@ -13,7 +13,7 @@ import viper.gobra.ast.frontend._
 import viper.gobra.frontend.PackageResolver.{AbstractImport, BuiltInImport, RegularImport}
 import viper.gobra.frontend.info.base.BuiltInMemberTag
 import viper.gobra.frontend.info.base.BuiltInMemberTag.{BuiltInMPredicateTag, BuiltInMethodTag}
-import viper.gobra.frontend.{Config, PackageResolver, Parser, Source}
+import viper.gobra.frontend.{PackageResolver, Parser, Source}
 import viper.gobra.frontend.info.{ExternalTypeInfo, Info}
 import viper.gobra.frontend.info.base.SymbolTable._
 import viper.gobra.frontend.info.base.Type._
@@ -225,12 +225,9 @@ trait MemberResolution { this: TypeInfoImpl =>
 
   def tryPackageLookup(importTarget: AbstractImport, id: PIdnUse, errNode: PNode): Option[(Entity, Vector[MemberPath])] = {
     def parseAndTypeCheck(importTarget: AbstractImport): Either[Vector[VerifierError], ExternalTypeInfo] = {
-      val resolveSourcesResult = PackageResolver.resolveSources(importTarget, config.moduleName, config.includeDirs).getOrElse(Vector())
-      val pkgSources = if (config.onlyFilesWithHeader) {
-        resolveSourcesResult.filter(p => p.isBuiltin || Config.sourceHasHeader(p.source)).map(_.source)
-      } else {
-        resolveSourcesResult.map(_.source)
-      }
+      val pkgSources = PackageResolver.resolveSources(importTarget)(config)
+        .getOrElse(Vector())
+        .map(_.source)
       val res = for {
         nonEmptyPkgSources <- if (pkgSources.isEmpty)
           Left(Vector(NotFoundError(s"No source files for package '$importTarget' found")))
diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala
index 4f556157a..1f3c84567 100644
--- a/src/main/scala/viper/gobra/reporting/VerifierError.scala
+++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala
@@ -31,6 +31,11 @@ case class NotFoundError(message: String) extends VerifierError {
   val id = "not_found_error"
 }
 
+case class ConfigError(message: String) extends VerifierError {
+  val position: Option[SourcePosition] = None
+  val id = "config_error"
+}
+
 case class ParserError(message: String, position: Option[SourcePosition]) extends VerifierError {
   val id = "parser_error"
 }
diff --git a/src/test/scala/viper/gobra/BenchmarkTests.scala b/src/test/scala/viper/gobra/BenchmarkTests.scala
index f2513e646..afbe52588 100644
--- a/src/test/scala/viper/gobra/BenchmarkTests.scala
+++ b/src/test/scala/viper/gobra/BenchmarkTests.scala
@@ -12,7 +12,7 @@ import java.nio.file.Path
 import org.scalatest.{ConfigMap, DoNotDiscover}
 import viper.gobra.frontend.{Config, PackageResolver, ScallopGobraConfig}
 import viper.gobra.reporting.{NoopReporter, VerifierError, VerifierResult}
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
+import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext, Violation}
 import viper.silver.ast.{NoPosition, Position}
 import viper.silver.frontend.Frontend
 import viper.silver.testing.StatisticalTestSuite
@@ -71,7 +71,9 @@ trait GobraFrontendForTesting extends Frontend {
     // exception occurs (e.g. a validation failure)
     throwError.value = true
     // Simulate pick of package, Gobra normally does
-    new ScallopGobraConfig(args.toSeq).config.copy(reporter = NoopReporter, z3Exe = z3Exe)
+    val config = new ScallopGobraConfig(args.toSeq).config
+    Violation.violation(config.isRight, "creating the config has failed")
+    config.toOption.get.copy(reporter = NoopReporter, z3Exe = z3Exe)
   }
 
   def gobraResult: VerifierResult
diff --git a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala
index d5b7edcdc..06372fb81 100644
--- a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala
+++ b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala
@@ -97,7 +97,7 @@ class DetailedBenchmarkTests extends BenchmarkTests {
       val c = config.get
       assert(c.packageInfoInputMap.size == 1)
       val pkgInfo = c.packageInfoInputMap.keys.head
-      config = Some(gobra.getAndMergeInFileConfig(c, pkgInfo))
+      config = gobra.getAndMergeInFileConfig(c, pkgInfo).toOption
     }
 
     private val parsing = InitialStep("parsing", () => {
diff --git a/src/test/scala/viper/gobra/GobraPackageTests.scala b/src/test/scala/viper/gobra/GobraPackageTests.scala
index 2826a463f..d1b3a2e1b 100644
--- a/src/test/scala/viper/gobra/GobraPackageTests.scala
+++ b/src/test/scala/viper/gobra/GobraPackageTests.scala
@@ -12,7 +12,7 @@ import ch.qos.logback.classic.Level
 import org.bitbucket.inkytonik.kiama.util.Source
 import org.rogach.scallop.exceptions.ValidationFailure
 import org.rogach.scallop.throwError
-import viper.gobra.frontend.Source.FromFileSource
+import viper.gobra.frontend.Source.{FromFileSource, getPackageInfo}
 import viper.gobra.frontend.{Config, PackageInfo, ScallopGobraConfig, Source}
 import viper.gobra.reporting.{NoopReporter, ParserError}
 import viper.gobra.reporting.VerifierResult.{Failure, Success}
@@ -61,8 +61,8 @@ class GobraPackageTests extends GobraTests {
           pkgName <- getPackageClause(input.file.toFile)
           config <- createConfig(Array(
             "--logLevel", "INFO",
-            "-i", currentDir.toFile.getPath,
-            "-p", pkgName,
+            "--directory", currentDir.toFile.getPath,
+            "--projectRoot", currentDir.toFile.getPath, // otherwise, it assumes Gobra's root directory as the project root
             "-I", currentDir.toFile.getPath
           ))
         } yield config
@@ -108,7 +108,7 @@ class GobraPackageTests extends GobraTests {
       // exception occurs (e.g. a validation failure)
       throwError.value = true
 
-      Some(new ScallopGobraConfig(args.toSeq).config)
+      new ScallopGobraConfig(args.toSeq).config.toOption
     } catch {
       case _: ValidationFailure => None
       case other: Throwable => throw other
diff --git a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala b/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala
index a5240e6e7..25980a22a 100644
--- a/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala
+++ b/src/test/scala/viper/gobra/reporting/StatsCollectorTests.scala
@@ -11,7 +11,7 @@ import org.scalatest.funsuite.AnyFunSuite
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.{Config, PackageInfo, ScallopGobraConfig}
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
+import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext, Violation}
 import viper.gobra.Gobra
 
 import scala.concurrent.Await
@@ -32,13 +32,12 @@ class StatsCollectorTests extends AnyFunSuite with BeforeAndAfterAll {
   }
 
   test("Integration without chopper") {
-    val config = createConfig(Array("-i", statsCollectorTestDir, "-r", "-I", statsCollectorTestDir))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir))
     runIntegration(config)
   }
 
   test("Integration with chopper") {
-    val config = createConfig(Array("-i", statsCollectorTestDir, "-r", "-I", statsCollectorTestDir, "--chop", "10"
-    ))
+    val config = createConfig(Array("--recursive", "--projectRoot", statsCollectorTestDir, "-I", statsCollectorTestDir, "--chop", "10"))
     runPackagesSeparately(config)
     runIntegration(config)
   }
@@ -48,7 +47,9 @@ class StatsCollectorTests extends AnyFunSuite with BeforeAndAfterAll {
     // exception occurs (e.g. a validation failure)
     throwError.value = true
     // Simulate pick of package, Gobra normally does
-    new ScallopGobraConfig(args.toSeq).config
+    val config = new ScallopGobraConfig(args.toSeq).config
+    Violation.violation(config.isRight, "creating the config has failed")
+    config.toOption.get
   }
 
   private def runPackagesSeparately(config: Config): Unit = {