diff --git a/README.md b/README.md
index 9b78864bd..5a346e58f 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,16 @@
 # KSMT
-Kotlin API for various SMT solvers.
+Kotlin/Java API for various SMT solvers.
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/workflows/build-and-run-tests.yml)
 ![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)
+[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
+
+# Overview
+
+`KSMT` provides a simple and unified way to work with SMT:
+* Define formulas in a simple and solver-independent way
+* Simplify and transform formulas without involving the SMT solver
+* Solve SMT formulas using various SMT solvers through a unified API
 
 # Getting started
 Install via [Gradle](https://gradle.org/).
@@ -64,3 +72,10 @@ independent of the solver.
 KSMT provides a high-performant API for running SMT solvers in separate processes.
 This feature is important for implementing hard timeouts and 
 solving using multiple solvers in portfolio mode.
+
+### Formula simplification and manipulation utils
+KSMT provides a simplification engine that can simplify and especially evaluate all supported expressions in all
+supported theories.
+Also, KSMT provides utilities for performing formula transformation, visiting and expression substitution.
+
+Check out our [advanced features tutorial](docs/advanced-usage.md) for the examples.
diff --git a/docs/advanced-usage.md b/docs/advanced-usage.md
new file mode 100644
index 000000000..832762f07
--- /dev/null
+++ b/docs/advanced-usage.md
@@ -0,0 +1,239 @@
+# Advanced usage
+
+Advanced features usage tutorial.
+If you are new to KSMT, please check out our [getting started guide](/docs/getting-started.md) first.
+
+For complete code examples, see our [example project](/examples) and
+particularly [`AdvancedExamples.kt`](/examples/src/main/kotlin/AdvancedExamples.kt)
+
+## Working with SMT formulas
+
+### Parsing formulas in SMT-LIB2 format
+
+KSMT provides an API for parsing formulas in the SMT-LIB2 format.
+Currently, KSMT provides a parser implemented on top of the Z3 solver API
+and therefore `ksmt-z3` module is required for parsing.
+
+```kotlin
+val formula = """
+    (declare-fun x () Int)
+    (declare-fun y () Int)
+    (assert (>= x y))
+    (assert (>= y x))
+"""
+with(ctx) {
+   val assertions = KZ3SMTLibParser().parse(formula)
+}
+```
+
+### Simplification during expressions creation
+
+By default, `KContext` will attempt to apply lightweight simplifications during expression creation. If simplifications
+are not suitable for your use cases you can disable them using the `KContext.simplificationMode` parameter.
+
+```kotlin
+// Simplification is enabled by default
+val simplifyingContext = KContext()
+
+// Disable simplifications on a context level
+val nonSimplifyingContext = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+val simplifiedExpr = with(simplifyingContext) {
+   val a by boolSort
+   !(a and falseExpr)
+}
+
+val nonSimplifiedExpr = with(nonSimplifyingContext) {
+   val a by boolSort
+   !(a and falseExpr)
+}
+
+println(nonSimplifiedExpr) // (not (and a false))
+println(simplifiedExpr) // true
+```
+
+### Manual expression simplification
+
+KSMT provides a `KExprSimplifier` which allows you to manually perform simplification of an arbitrary expression.
+
+```kotlin
+// Context do not simplify expressions during creation
+val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+with(ctx) {
+   val a by boolSort
+   val nonSimplifiedExpr = !(a and falseExpr)
+
+   val simplifier = KExprSimplifier(ctx)
+   val simplifiedExpr = simplifier.apply(nonSimplifiedExpr)
+
+   println(nonSimplifiedExpr) // (not (and a false))
+   println(simplifiedExpr) // true
+}
+```
+
+### Expression substitution
+
+KSMT provides a `KExprSubstitutor` which allows you to replace all occurrences of one expression with another
+expression.
+
+```kotlin
+val a by boolSort
+val b by boolSort
+val expr = !(a and b)
+
+val substitutor = KExprSubstitutor(this).apply {
+   // Substitute all occurrences of `b` with `false`
+   substitute(b, falseExpr)
+}
+
+val exprAfterSubstitution = substitutor.apply(expr)
+
+println(expr) // (not (and a b))
+println(exprAfterSubstitution) // true
+```
+
+## Working with SMT solvers
+
+### Solver configuration
+
+KSMT provides an API for modifying solver-specific parameters.
+Since the parameters and their correct values are solver-specific
+KSMT does not perform any checks.
+See the corresponding solver documentation for a list of available options.
+
+```kotlin
+with(ctx) {
+   KZ3Solver(this).use { solver ->
+      solver.configure {
+         // set Z3 solver parameter random_seed to 42 
+         setZ3Option("random_seed", 42)
+      }
+   }
+}
+```
+
+### Solver independent models
+
+By default, SMT solver models lazily initialized.
+The values of the declared variables are loaded from the underlying solver's native model on demand.
+Therefore, models become invalid after solver close. Also, solvers like `Bitwuzla` invalidate their models every
+time `check-sat` is called.
+To overcome these problems, KSMT provides the `KModel.detach` function that allows you to make the model independent of
+the underlying native representation.
+
+```kotlin
+val a by boolSort
+val b by boolSort
+val expr = a and b
+
+val (model, detachedModel) = KZ3Solver(this).use { solver ->
+   solver.assert(expr)
+   println(solver.check()) // SAT
+   val model = solver.model()
+
+   // Detach model from solver
+   val detachedModel = model.detach()
+
+   model to detachedModel
+}
+
+try {
+   model.eval(expr)
+} catch (ex: Exception) {
+   println("Model no longer valid after solver close")
+}
+
+println(detachedModel.eval(expr)) // true
+```
+
+Note: it is usually a good idea to use `KModel.detach` when you need to keep model e.g. in a `List`.
+
+### Solver runner
+
+SMT solvers are implemented via native libraries and usually have the following issues:
+
+1. Timeout ignore. SMT solver may hang in a long-running operation before reaching a checkpoint.
+   Since solver is a native library, there is no way to interrupt it.
+2. Solvers are usually research projects with a bunch of bugs, e.g. pointer issues. Such
+   errors lead to the interruption of the entire process, including the user's app.
+
+To overcome these problems KSMT provides a solver runner that runs solvers in separate processes to preserve your
+application stability.
+
+```kotlin
+// Create a long-lived solver manager that manages a pool of solver workers
+KSolverRunnerManager().use { solverManager ->
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create solver using manager instead of direct constructor invocation
+      solverManager.createSolver(this, KZ3Solver::class).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```
+
+### Using custom solvers in a runner
+
+Solver runner also supports user defined solvers. Custom solvers must be registered before being used in the runner
+using `registerSolver`.
+
+```kotlin
+// Create a long-lived solver manager that manages a pool of solver workers
+KSolverRunnerManager().use { solverManager ->
+   // Register user-defined solver in a current manager
+   solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create solver using manager instead of direct constructor invocation
+      solverManager.createSolver(this, CustomZ3BasedSolver::class).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```
+
+### Solver portfolio
+
+Various SMT solvers usually show different performance on a same SMT formula.
+[Portfolio solving](https://arxiv.org/abs/1505.03340) is a simple idea of
+running different solvers on the same formula simultaneously and waiting only
+for the first result.
+The portfolio solver workflow in KSMT is similar to the solver runner.
+
+```kotlin
+// Create a long-lived portfolio solver manager that manages a pool of solver workers
+KPortfolioSolverManager(
+   // Solvers to include in portfolio
+   listOf(KZ3Solver::class, CustomZ3BasedSolver::class)
+).use { solverManager ->
+   // Since we use user-defined solver in our portfolio we must register it in the current manager
+   solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create portfolio solver using manager
+      solverManager.createPortfolioSolver(this).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 1d2bde4bf..531bfd0ab 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -340,39 +340,3 @@ with(ctx) {
     }
 }
 ```
-
-### Parsing formulas in SMT-LIB2 format
-
-KSMT provides an API for parsing formulas in the SMT-LIB2 format. 
-Currently, KSMT provides a parser implemented on top of the Z3 solver API 
-and therefore `ksmt-z3` module is required for parsing.
-
-```kotlin
-val formula = """
-    (declare-fun x () Int)
-    (declare-fun y () Int)
-    (assert (>= x y))
-    (assert (>= y x))
-"""
-with(ctx) {
-    val assertions = KZ3SMTLibParser().parse(formula)
-}
-```
-
-### Solver configuration
-
-KSMT provides an API for modifying solver-specific parameters. 
-Since the parameters and their correct values are solver-specific 
-KSMT does not perform any checks. 
-See the corresponding solver documentation for a list of available options. 
-
-```kotlin
-with(ctx) {
-    KZ3Solver(this).use { solver ->
-        solver.configure {
-            // set Z3 solver parameter random_seed to 42 
-            setZ3Option("random_seed", 42)
-        }
-    }
-}
-```
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 9651d77a1..af06a95c4 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -12,6 +12,8 @@ dependencies {
     implementation("io.ksmt:ksmt-core:0.5.3")
     // z3 solver
     implementation("io.ksmt:ksmt-z3:0.5.3")
+    // Runner and portfolio solver
+    implementation("io.ksmt:ksmt-runner:0.5.3")
 }
 
 java {
diff --git a/examples/src/main/kotlin/AdvancedExamples.kt b/examples/src/main/kotlin/AdvancedExamples.kt
new file mode 100644
index 000000000..2ca122da4
--- /dev/null
+++ b/examples/src/main/kotlin/AdvancedExamples.kt
@@ -0,0 +1,197 @@
+import io.ksmt.KContext
+import io.ksmt.expr.rewrite.KExprSubstitutor
+import io.ksmt.expr.rewrite.simplify.KExprSimplifier
+import io.ksmt.solver.KSolver
+import io.ksmt.solver.portfolio.KPortfolioSolverManager
+import io.ksmt.solver.runner.KSolverRunnerManager
+import io.ksmt.solver.z3.KZ3SMTLibParser
+import io.ksmt.solver.z3.KZ3Solver
+import io.ksmt.solver.z3.KZ3SolverConfiguration
+import io.ksmt.solver.z3.KZ3SolverUniversalConfiguration
+import io.ksmt.utils.getValue
+
+fun main() {
+    val ctx = KContext()
+
+    parseSmtFormula(ctx)
+    simplificationOnCreation()
+    manualExpressionSimplification()
+    expressionSubstitution(ctx)
+
+    solverConfiguration(ctx)
+    solverModelDetach(ctx)
+    solverRunnerUsageExample(ctx)
+    solverRunnerWithCustomSolverExample(ctx)
+    solverPortfolioExample(ctx)
+}
+
+fun simplificationOnCreation() {
+    // Simplification is enabled by default
+    val simplifyingContext = KContext()
+
+    // Disable simplifications on a context level
+    val nonSimplifyingContext = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+    val simplifiedExpr = with(simplifyingContext) {
+        val a by boolSort
+        !(a and falseExpr)
+    }
+
+    val nonSimplifiedExpr = with(nonSimplifyingContext) {
+        val a by boolSort
+        !(a and falseExpr)
+    }
+
+    println(nonSimplifiedExpr) // (not (and a false))
+    println(simplifiedExpr) // true
+}
+
+fun manualExpressionSimplification() {
+    // Context do not simplify expressions during creation
+    val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+    with(ctx) {
+        val a by boolSort
+        val nonSimplifiedExpr = !(a and falseExpr)
+
+        val simplifier = KExprSimplifier(ctx)
+        val simplifiedExpr = simplifier.apply(nonSimplifiedExpr)
+
+        println(nonSimplifiedExpr) // (not (and a false))
+        println(simplifiedExpr) // true
+    }
+}
+
+fun expressionSubstitution(ctx: KContext) = with(ctx) {
+    val a by boolSort
+    val b by boolSort
+    val expr = !(a and b)
+
+    val substitutor = KExprSubstitutor(this).apply {
+        // Substitute all occurrences of `b` with `false`
+        substitute(b, falseExpr)
+    }
+
+    val exprAfterSubstitution = substitutor.apply(expr)
+
+    println(expr) // (not (and a b))
+    println(exprAfterSubstitution) // true
+}
+
+fun parseSmtFormula(ctx: KContext) = with(ctx) {
+    val formula = """
+    (declare-fun x () Int)
+    (declare-fun y () Int)
+    (assert (>= x y))
+    (assert (>= y x))
+    """
+    val assertions = KZ3SMTLibParser(this).parse(formula)
+    println(assertions)
+}
+
+fun solverConfiguration(ctx: KContext) = with(ctx) {
+    KZ3Solver(this).use { solver ->
+        solver.configure {
+            // set Z3 solver parameter random_seed to 42
+            setZ3Option("random_seed", 42)
+        }
+    }
+}
+
+fun solverModelDetach(ctx: KContext) = with(ctx) {
+    val a by boolSort
+    val b by boolSort
+    val expr = a and b
+
+    val (model, detachedModel) = KZ3Solver(this).use { solver ->
+        solver.assert(expr)
+        println(solver.check()) // SAT
+        val model = solver.model()
+
+        // Detach model from solver
+        val detachedModel = model.detach()
+
+        model to detachedModel
+    }
+
+    try {
+        model.eval(expr)
+    } catch (ex: Exception) {
+        println("Model no longer valid after solver close")
+    }
+
+    println(detachedModel.eval(expr)) // true
+}
+
+fun solverRunnerUsageExample(ctx: KContext) {
+    // Create a long-lived solver manager that manages a pool of solver workers
+    KSolverRunnerManager().use { solverManager ->
+
+        // Use solver API as usual
+        with(ctx) {
+            val a by boolSort
+            val b by boolSort
+            val expr = a and b
+
+            // Create solver using manager instead of direct constructor invocation
+            solverManager.createSolver(this, KZ3Solver::class).use { solver ->
+                solver.assert(expr)
+                println(solver.check()) // SAT
+            }
+        }
+    }
+}
+
+// User defined solver
+class CustomZ3BasedSolver(ctx: KContext) : KSolver<KZ3SolverConfiguration> by KZ3Solver(ctx) {
+    init {
+        configure {
+            setZ3Option("smt.logic", "QF_BV")
+        }
+    }
+}
+
+fun solverRunnerWithCustomSolverExample(ctx: KContext) {
+    // Create a long-lived solver manager that manages a pool of solver workers
+    KSolverRunnerManager().use { solverManager ->
+        // Register user-defined solver in a current manager
+        solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+        // Use solver API as usual
+        with(ctx) {
+            val a by boolSort
+            val b by boolSort
+            val expr = a and b
+
+            // Create solver using manager instead of direct constructor invocation
+            solverManager.createSolver(this, CustomZ3BasedSolver::class).use { solver ->
+                solver.assert(expr)
+                println(solver.check()) // SAT
+            }
+        }
+    }
+}
+
+fun solverPortfolioExample(ctx: KContext) {
+    // Create a long-lived portfolio solver manager that manages a pool of solver workers
+    KPortfolioSolverManager(
+        // Solvers to include in portfolio
+        listOf(KZ3Solver::class, CustomZ3BasedSolver::class)
+    ).use { solverManager ->
+        // Since we use user-defined solver in our portfolio we must register it in the current manager
+        solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+        // Use solver API as usual
+        with(ctx) {
+            val a by boolSort
+            val b by boolSort
+            val expr = a and b
+
+            // Create portfolio solver using manager
+            solverManager.createPortfolioSolver(this).use { solver ->
+                solver.assert(expr)
+                println(solver.check()) // SAT
+            }
+        }
+    }
+}