diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt
index 4ca9d754e6..764a015c0b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt
@@ -1,6 +1,7 @@
 package org.usvm.machine.call
 
 import org.jacodb.ets.model.EtsAnyType
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsLocal
@@ -48,3 +49,7 @@ internal fun EtsType.isBuiltinDateGlobalType(): Boolean = this is EtsFunctionTyp
     signature.name.isEmpty() &&
     signature.parameters.isEmpty() &&
     signature.returnType == EtsStringType
+
+internal fun EtsType.isBuiltinArrayGlobalType(): Boolean = this is EtsFunctionType &&
+    signature.returnType is EtsArrayType &&
+    signature.enclosingClass.file == EtsClassSignature.UNKNOWN.file
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
index 825fbe8170..f896269a5a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
@@ -2,6 +2,7 @@ package org.usvm.machine.call.intrinsic
 
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsArrayType
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.machine.call.TsEtsIrUnknownCallModel
 import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact
@@ -13,6 +14,7 @@ import org.usvm.machine.call.TsUnknownCallModel
 import org.usvm.machine.call.TsUnknownCallTarget
 import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
 import org.usvm.util.arrayStorageType
+import org.usvm.util.isUnmodifiedDenseInputArray
 
 /** Built-in Array algorithms implemented by ordinary TypeScript bodies. */
 internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
@@ -48,22 +50,24 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                     falseExpr
                 } else {
                     val elementSort = typeToSort(receiverType.elementType)
+                    val hasNoMissingSlots = array is UConcreteHeapRef &&
+                        state.isUnmodifiedDenseInputArray(array, receiverType)
                     val excludesMissingSlot = when {
                         searchElement == mkUndefinedValue() &&
                             (
                                 call.callee.name in setOf("indexOf", "lastIndexOf") ||
                                     elementSort == fp64Sort || elementSort == boolSort
-                                ) -> falseExpr
+                                ) -> mkBool(hasNoMissingSlots)
 
                         elementSort == fp64Sort && searchElement?.sort == fp64Sort -> {
                             val searchNumber = searchElement.asExpr(fp64Sort)
                             val zero = mkFp64(0.0)
 
-                            mkNot(mkFpEqualExpr(searchNumber, zero))
+                            mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, zero)))
                         }
 
                         elementSort == boolSort && searchElement?.sort == boolSort -> {
-                            searchElement.asExpr(boolSort)
+                            mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort))
                         }
 
                         else -> trueExpr
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt
new file mode 100644
index 0000000000..c839d92c1e
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt
@@ -0,0 +1,88 @@
+package org.usvm.machine.call.intrinsic
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.call.TsUnknownCallModelCompletion
+import org.usvm.machine.call.TsUnknownCallModelExecution
+import org.usvm.machine.call.TsUnknownCallModelSuccessor
+import org.usvm.machine.call.TsUnknownCallTarget
+import org.usvm.machine.state.TsState
+
+/** Exact `Array.isArray` semantics for the genuine global `Array` built-in. */
+internal object TsArrayIsArrayIntrinsicModel : TsBuiltInUnknownCallModel {
+    const val MODEL_ID: String = "ts.array.isArray"
+
+    private val anyArrayType = EtsArrayType(elementType = EtsUnknownType, dimensions = 1)
+
+    override val id: String = MODEL_ID
+    override val target = TsUnknownCallTarget(
+        methodName = "isArray",
+    )
+
+    override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
+        if (!call.hasGlobalArrayOwner()) {
+            return null
+        }
+
+        val value = when {
+            call.arguments.isEmpty() -> return state.normalExecution(state.ctx.falseExpr)
+            else -> call.arguments.first().resolved ?: return null
+        }
+        val result = state.isArray(value)
+
+        return state.normalExecution(result)
+    }
+
+    private fun TsUnknownCall.hasGlobalArrayOwner(): Boolean {
+        val owner = receiver?.source as? EtsLocal ?: return false
+        val ownerType = owner.type as? EtsFunctionType ?: return false
+        val signatureFile = ownerType.signature.enclosingClass.file
+
+        return owner.name == "Array" &&
+            ownerType.signature.returnType is EtsArrayType &&
+            signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT &&
+            signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT
+    }
+
+    private fun TsState.isArray(value: UExpr<*>) = with(ctx) {
+        when {
+            value.isFakeObject() -> {
+                val fakeType = value.getFakeType(memory)
+                val reference = value.extractRef(memory)
+
+                mkAnd(
+                    fakeType.refTypeExpr,
+                    isNonNullArrayReference(reference),
+                )
+            }
+
+            value.sort == addressSort -> isNonNullArrayReference(value.asExpr(addressSort))
+            else -> falseExpr
+        }
+    }
+
+    private fun TsState.isNonNullArrayReference(reference: UHeapRef): UBoolExpr = with(ctx) {
+        val isDefined = mkNot(mkEq(reference, mkUndefinedValue()))
+        val isNonNull = mkNot(mkEq(reference, mkTsNullValue()))
+
+        mkAnd(isDefined, isNonNull, memory.types.evalIsSubtype(reference, anyArrayType))
+    }
+
+    private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) {
+        val successor = TsUnknownCallModelSuccessor(
+            guard = trueExpr,
+            completion = TsUnknownCallModelCompletion.Normal { result },
+        )
+
+        TsUnknownCallModelExecution(successors = listOf(successor))
+    }
+
+    private const val UNKNOWN_SIGNATURE_COMPONENT: String = "%unk"
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt
index ffda619edd..0b01352043 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt
@@ -21,9 +21,11 @@ import org.usvm.machine.call.TsUnknownCallTarget
 import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
 import org.usvm.machine.state.TsState
 import org.usvm.sizeSort
+import org.usvm.util.copyStringRange
 import org.usvm.util.mkStringBackingElementLValue
 import org.usvm.util.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
+import org.usvm.util.stringFromCodeUnit
 
 /** Built-in String algorithms implemented by ordinary TypeScript bodies. */
 internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
@@ -94,11 +96,48 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         }
     }
 
+    private val sliceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
+        val inputs = call.resolvedInstanceInputs() ?: return@TsEtsIrUnknownCallModelInputAdapter null
+        val receiver = inputs.firstOrNull()?.takeIf { it.sort == state.ctx.addressSort }
+            ?: return@TsEtsIrUnknownCallModelInputAdapter null
+        val arguments = inputs.drop(1)
+        if (arguments.size > 2) {
+            return@TsEtsIrUnknownCallModelInputAdapter null
+        }
+
+        fun numericOrDefault(index: Int, default: UExpr<*>): UExpr<*> {
+            val value = arguments.getOrNull(index) ?: return default
+            return when {
+                value == state.ctx.mkUndefinedValue() -> default
+                value.sort == state.ctx.fp64Sort -> value
+                else -> return default
+            }
+        }
+
+        val start = numericOrDefault(index = 0, default = state.ctx.mkFp64(0.0))
+        val end = numericOrDefault(
+            index = 1,
+            default = state.ctx.mkFpInf(signBit = false, state.ctx.fp64Sort),
+        )
+        if (arguments.any { value -> value != state.ctx.mkUndefinedValue() && value.sort != state.ctx.fp64Sort }) {
+            return@TsEtsIrUnknownCallModelInputAdapter null
+        }
+
+        listOf(receiver, start, end)
+    }
+
+    private val noArgumentsAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call ->
+        if (call.arguments.isNotEmpty()) {
+            null
+        } else {
+            call.resolvedInstanceInputs()
+        }
+    }
+
     private val receiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs ->
         with(state.ctx) {
             val receiver = inputs.firstOrNull()
-            // Symbolic String parameters do not initialize the backing character array yet.
-            if (receiver !is UConcreteHeapRef || getStringConstantValue(receiver) == null) {
+            if (receiver !is UConcreteHeapRef || receiver.hasFakeValueBranch()) {
                 falseExpr
             } else {
                 state.memory.types.evalTypeEquals(receiver, EtsStringType)
@@ -110,9 +149,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         with(state.ctx) {
             val receiver = inputs.getOrNull(0)
             val searchString = inputs.getOrNull(1)
-            val receiverIsConstant = receiver is UConcreteHeapRef && getStringConstantValue(receiver) != null
-            val searchStringIsConstant =
-                searchString is UConcreteHeapRef && getStringConstantValue(searchString) != null
+            val receiverIsConstant = receiver is UConcreteHeapRef && !receiver.hasFakeValueBranch()
+            val searchStringIsConstant = searchString is UConcreteHeapRef && !searchString.hasFakeValueBranch()
 
             if (!receiverIsConstant || !searchStringIsConstant) {
                 falseExpr
@@ -125,6 +163,38 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         }
     }
 
+    private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
+        with(state.ctx) {
+            val receiverGuard = receiverDomain.evaluate(state, call, inputs)
+            val receiver = inputs.firstOrNull() as? UConcreteHeapRef
+                ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr
+            val characters = state.memory.read(mkStringBackingLValue(receiver))
+                .asExpr(addressSort)
+            val length = state.memory.read(mkStringBackingLengthLValue(characters))
+            val characterGuards = (0 until MAX_ASCII_CASE_LENGTH).map { index ->
+                val symbolicIndex = mkBv(index)
+                val codeUnit = state.memory.read(
+                    mkStringBackingElementLValue(ref = characters, index = symbolicIndex)
+                )
+                val isOutsideLength = mkBvSignedGreaterOrEqualExpr(symbolicIndex, length)
+                val asciiMax = mkBv(ASCII_MAX_CODE_UNIT, bv16Sort)
+                val isAscii = mkBvUnsignedLessOrEqualExpr(codeUnit, asciiMax)
+                mkOr(
+                    isOutsideLength,
+                    isAscii,
+                )
+            }
+
+            val maximumLength = mkBv(MAX_ASCII_CASE_LENGTH)
+            val withinLengthLimit = mkBvSignedLessOrEqualExpr(length, maximumLength)
+            mkAnd(
+                receiverGuard,
+                withinLengthLimit,
+                *characterGuards.toTypedArray(),
+            )
+        }
+    }
+
     private val receiverAndConcreteIndexDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs ->
         if (inputs.getOrNull(1) !is KFp64Value) {
             state.ctx.falseExpr
@@ -177,6 +247,24 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 inputAdapter = optionalEndPositionAdapter,
                 domainGuard = receiverAndSearchDomain,
             ),
+            sourceModel(
+                id = "ts.string.slice",
+                methodName = "slice",
+                inputAdapter = sliceAdapter,
+                domainGuard = receiverDomain,
+            ),
+            sourceModel(
+                id = "ts.string.toUpperCase",
+                methodName = "toUpperCase",
+                inputAdapter = noArgumentsAdapter,
+                domainGuard = asciiReceiverDomain,
+            ),
+            sourceModel(
+                id = "ts.string.toLowerCase",
+                methodName = "toLowerCase",
+                inputAdapter = noArgumentsAdapter,
+                domainGuard = asciiReceiverDomain,
+            ),
             primitiveModel(
                 methodName = "length",
                 arity = 1,
@@ -192,6 +280,11 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
                 arity = 1,
                 implementation = ::stringFromCodeUnit,
             ),
+            primitiveModel(
+                methodName = "copyRange",
+                arity = 3,
+                implementation = ::stringCopyRange,
+            ),
         )
     }
 
@@ -214,9 +307,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
             add(MATH_FLOOR_MODEL_ID)
             add(PRIMITIVE_LENGTH_ID)
             add(PRIMITIVE_CODE_UNIT_AT_ID)
-            if (methodName == "charAt") {
+            if (methodName in setOf("charAt", "toUpperCase", "toLowerCase")) {
                 add(PRIMITIVE_FROM_CODE_UNIT_ID)
             }
+            if (methodName == "slice") {
+                add(PRIMITIVE_COPY_RANGE_ID)
+            }
         },
     )
 
@@ -305,16 +401,58 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
         state: TsState,
         inputs: List<UExpr<*>>,
     ): TsUnknownCallModelExecution? = with(state.ctx) {
-        val code = inputs.singleOrNull() as? KFp64Value ?: return null
+        val code = inputs.singleOrNull()?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
         val successor = TsUnknownCallModelSuccessor(
             guard = trueExpr,
             completion = TsUnknownCallModelCompletion.Normal {
-                mkInitializedStringConstant(code.value.toInt().toChar().toString())
+                if (code is KFp64Value) {
+                    mkInitializedStringConstant(code.value.toInt().toChar().toString())
+                } else {
+                    stringFromCodeUnit(code)
+                }
+            },
+        )
+
+        TsUnknownCallModelExecution(
+            successors = listOf(successor),
+        )
+    }
+
+    private fun stringCopyRange(
+        state: TsState,
+        inputs: List<UExpr<*>>,
+    ): TsUnknownCallModelExecution? = with(state.ctx) {
+        val receiver = inputs.getOrNull(0)?.takeIf { it.sort == addressSort }?.asExpr(addressSort) ?: return null
+        val start = inputs.getOrNull(1)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
+        val end = inputs.getOrNull(2)?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null
+        if (receiver.hasFakeValueBranch()) {
+            return null
+        }
+
+        val from = mkFpToBvExpr(
+            roundingMode = fpRoundingModeSortDefaultValue(),
+            value = start,
+            bvSize = sizeSort.sizeBits.toInt(),
+            isSigned = true,
+        ).asExpr(sizeSort)
+        val to = mkFpToBvExpr(
+            roundingMode = fpRoundingModeSortDefaultValue(),
+            value = end,
+            bvSize = sizeSort.sizeBits.toInt(),
+            isSigned = true,
+        ).asExpr(sizeSort)
+        val length = mkBvSubExpr(to, from)
+        val receiverIsString = state.memory.types.evalTypeEquals(receiver, EtsStringType)
+        val successor = TsUnknownCallModelSuccessor(
+            guard = receiverIsString,
+            completion = TsUnknownCallModelCompletion.Normal {
+                copyStringRange(receiver = receiver, from = from, length = length)
             },
         )
 
         TsUnknownCallModelExecution(
             successors = listOf(successor),
+            residualGuard = receiverIsString.takeUnless { it == trueExpr }?.let(::mkNot),
         )
     }
 
@@ -366,5 +504,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
     private const val PRIMITIVE_LENGTH_ID = "ts.string.primitive.length"
     private const val PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt"
     private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit"
+    private const val PRIMITIVE_COPY_RANGE_ID = "ts.string.primitive.copyRange"
     private const val MATH_FLOOR_MODEL_ID = "ts.math.floor"
+    private const val MAX_ASCII_CASE_LENGTH = 16
+    private const val ASCII_MAX_CODE_UNIT = 0x7f
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
index 8849560fd0..547ea13a14 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
@@ -48,6 +48,7 @@ import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.resolveEtsMethods
 
 private val logger = KotlinLogging.logger {}
+private val legacyArrayMethods = setOf("concat", "fill", "join", "push", "reverse", "slice", "unshift")
 
 internal fun TsExprResolver.tryApproximateGlobalInstanceCall(
     expr: EtsInstanceCallExpr,
@@ -135,6 +136,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
     // Mock `.toString()` method calls
     if (expr.callee.name == "toString") {
+        if (unknownCallDispatcher is TsUnknownCallModelDispatcher) {
+            dispatchLegacyInstanceCall(stmt)
+            return TsExprApproximationResult.ResolveFailure
+        }
+
         if (expr.args.isNotEmpty()) {
             logger.warn { "toString() should have no arguments, but got ${expr.args.size}" }
         }
@@ -161,6 +167,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
             .takeIf { it !is TsUnresolvedSort }
             ?: addressSort
 
+        if (expr.callee.name in legacyArrayMethods && unknownCallDispatcher is TsUnknownCallModelDispatcher) {
+            dispatchArrayModel(stmt)
+            return TsExprApproximationResult.ResolveFailure
+        }
+
         // Handle 'Array.push()' method calls
         if (expr.callee.name == "push") {
             return from(handleArrayPush(expr, instanceType, elementSort, array))
@@ -224,7 +235,10 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
         "includes",
         "indexOf",
         "lastIndexOf",
+        "slice",
         "startsWith",
+        "toLowerCase",
+        "toUpperCase",
     )
     if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) {
         val dispatcher = unknownCallDispatcher
@@ -291,6 +305,17 @@ private fun TsExprResolver.dispatchArrayModel(stmt: TsVirtualMethodCallStmt) {
     )
 }
 
+private fun TsExprResolver.dispatchLegacyInstanceCall(stmt: TsVirtualMethodCallStmt) {
+    unknownCallDispatcher.dispatch(
+        scope = scope,
+        call = stmt.call,
+        callSite = stmt.returnSite,
+        failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+        resolvedReceiver = stmt.instance,
+        resolvedArguments = stmt.args,
+    )
+}
+
 private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSignature =
     copy(enclosingClass = enclosingClass.copy(name = name))
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
index 94ef0fd22f..9694ddeed1 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
@@ -232,7 +232,7 @@ private fun TsContext.materializeTypedStringField(
     }
     scope.assert(constraints) ?: return null
 
-    scope.doWithState { boundedStringBackingRefs += stringRef }
+    scope.doWithState { boundedStringBackingRefs += stringRef to maxStringLength }
 
     return stringRef
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
index b30f330466..f366f0dcf9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
@@ -17,8 +17,7 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.sizeSort
 import org.usvm.util.arrayStorageType
 import org.usvm.util.mkArrayLengthLValue
-import org.usvm.util.mkStringBackingLValue
-import org.usvm.util.mkStringBackingLengthLValue
+import org.usvm.util.stringLength
 
 // Handles reading the `length` property.
 fun TsContext.readLengthProperty(
@@ -29,6 +28,19 @@ fun TsContext.readLengthProperty(
 ): UExpr<*>? {
     // Determine the array type.
     val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
+    if (storageType is EtsStringType) {
+        val length = scope.calcOnState { stringLength(instance) }
+        val lengthBound = scope.calcOnState { boundedStringBackingRefs[instance] ?: maxArraySize }
+        ensureLengthBounds(scope, length, lengthBound) ?: return null
+
+        return mkBvToFpExpr(
+            sort = fp64Sort,
+            roundingMode = fpRoundingModeSortDefaultValue(),
+            value = length.asExpr(sizeSort),
+            signed = true,
+        )
+    }
+
     val arrayType: EtsArrayType = when (val type = storageType) {
         is EtsArrayType -> type
 
@@ -38,18 +50,6 @@ fun TsContext.readLengthProperty(
             EtsArrayType(EtsUnknownType, dimensions = 1)
         }
 
-        is EtsStringType -> {
-            val charsRef = scope.calcOnState {
-                memory.read(mkStringBackingLValue(instance))
-            }
-
-            return readArrayLength(
-                scope = scope,
-                lengthLValue = mkStringBackingLengthLValue(charsRef),
-                maxArraySize = maxArraySize,
-            )
-        }
-
         else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
     }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt
index fe4ea7c73d..6c9cd5f5ec 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt
@@ -19,6 +19,7 @@ import org.usvm.USort
 import org.usvm.api.allocateConcreteRef
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.isTrue
+import org.usvm.machine.call.isBuiltinArrayGlobalType
 import org.usvm.machine.call.isBuiltinDateGlobalType
 import org.usvm.machine.call.isBuiltinGlobalType
 import org.usvm.machine.state.lastStmt
@@ -155,7 +156,7 @@ private fun isImplicitModeledGlobal(source: EtsLocal, callee: EtsMethodSignature
         return true
     }
 
-    if (source.type.isBuiltinDateGlobalType()) return true
+    if (source.type.isBuiltinDateGlobalType() || source.type.isBuiltinArrayGlobalType()) return true
 
     val modeled = when (source.name) {
         "Logger" -> true
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 7daf2db96e..5d2f063d13 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -736,7 +736,7 @@ class TsExprResolver(
                             guard = trueExpr,
                         )
                         memory.write(mkStringBackingLengthLValue(resultChars), resultLength, guard = trueExpr)
-                        boundedStringBackingRefs += result
+                        boundedStringBackingRefs += result to options.maxArraySize
 
                         memory.memcpy(
                             srcRef = leftChars,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
index 43f81d3d6c..d6849ac464 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
@@ -40,6 +40,7 @@ import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UExpr
 import org.usvm.UInterpreter
+import org.usvm.USort
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.initializeArray
 import org.usvm.api.targets.TsTarget
@@ -792,7 +793,12 @@ class TsInterpreter(
             unknownCallDispatcher = unknownCallDispatcher,
         )
 
-    fun getInitialState(method: EtsMethod, targets: List<TsTarget>): TsState = with(ctx) {
+    fun getInitialState(
+        method: EtsMethod,
+        targets: List<TsTarget>,
+        configure: (TsState) -> Unit = {},
+        parameterSortOverride: (Int) -> USort? = { null },
+    ): TsState = with(ctx) {
         val state = TsState(
             ctx = ctx,
             ownership = MutabilityOwnership(),
@@ -819,6 +825,11 @@ class TsInterpreter(
 
         method.parameters.forEachIndexed { i, param ->
             val idx = i + 1 // +1 because 0 is reserved for `this`
+            val overriddenSort = parameterSortOverride(idx)
+            if (overriddenSort != null) {
+                state.saveSortForLocal(idx, overriddenSort)
+                return@forEachIndexed
+            }
 
             val ref by lazy {
                 val lValue = mkRegisterStackLValue(addressSort, idx)
@@ -867,7 +878,7 @@ class TsInterpreter(
                 state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType)
 
                 state.pathConstraints += state.symbolicStringBackingConstraint(ref)
-                state.boundedStringBackingRefs += ref
+                state.boundedStringBackingRefs += ref to state.maxStringLength
             }
 
             val parameterSort = typeToSort(parameterType)
@@ -885,6 +896,8 @@ class TsInterpreter(
             }
         }
 
+        configure(state)
+
         val solver = solver<EtsType>()
         val model = solver.check(state.pathConstraints).ensureSat().model
         state.models = listOf(model)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index 1d7ac99326..d908539655 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -86,7 +86,10 @@ private fun TsContext.stringValueEquals(
             rhsChars = rhsChars,
             lhsLength = lhsLength,
             rhsLength = rhsLength,
-            maxLength = maxStringLength,
+            maxLength = maxOf(
+                boundedStringBackingRefs[lhs] ?: maxStringLength,
+                boundedStringBackingRefs[rhs] ?: maxStringLength,
+            ),
         )
     }
 
@@ -119,7 +122,7 @@ private fun TsContext.stringValueEquals(
         boundedLengths,
     )
     scope.fork(supported, blockOnFalseState = {
-        terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength")
+        terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..${comparison.maxLength}")
     }) ?: return null
 
     // Known literals supply a tighter comparison bound; all other string lengths are constrained above.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 8648f66ce7..0f917b2a55 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -1,5 +1,6 @@
 package org.usvm.machine.state
 
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBlockCfg
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsFile
@@ -30,6 +31,7 @@ import org.usvm.machine.interpreter.PromiseState
 import org.usvm.machine.interpreter.TsFunction
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemory
+import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelBase
 import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
@@ -84,14 +86,15 @@ class TsState(
      */
     var stringConstantAllocatedRefs: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
     /**
-     * References whose string backing and length bound have been modeled.
+     * Maps references with modeled string backing to their maximum length.
      * A new symbolic string producer must register its reference here after creating the backing model.
      * String literals are recognized separately through [TsContext.getStringConstantValue].
      */
-    var boundedStringBackingRefs: Set<UHeapRef> = emptySet(),
+    var boundedStringBackingRefs: Map<UHeapRef, Int> = emptyMap(),
     /** Unresolved reference payloads that may acquire string backing after type refinement. */
     var symbolicStringCandidates: Set<UHeapRef> = emptySet(),
     var unsupportedReason: String? = null,
+    internal val denseInputArrays: MutableMap<UConcreteHeapRef, TsDenseInputArray> = mutableMapOf(),
     private val activeUnknownCallModels: MutableList<Pair<String, Int>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
@@ -288,6 +291,7 @@ class TsState(
             ref
         }
         stringConstantAllocatedRefs = updated
+        boundedStringBackingRefs += result to value.length
         result
     }
 
@@ -330,6 +334,7 @@ class TsState(
             boundedStringBackingRefs = boundedStringBackingRefs,
             symbolicStringCandidates = symbolicStringCandidates,
             unsupportedReason = unsupportedReason,
+            denseInputArrays = denseInputArrays.toMutableMap(),
             activeUnknownCallModels = activeUnknownCallModels.toMutableList(),
         )
     }
@@ -337,3 +342,10 @@ class TsState(
     override val isExceptional: Boolean
         get() = methodResult is TsMethodResult.TsException
 }
+
+/** Snapshot of the storage regions that establish dense input-array contents. */
+data class TsDenseInputArray(
+    val type: EtsArrayType,
+    val lengthRegion: UReadOnlyMemoryRegion<*, *>,
+    val elementRegion: UReadOnlyMemoryRegion<*, *>,
+)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt
index 55a87920ed..91b181f1b4 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt
@@ -70,7 +70,7 @@ internal fun TsStepScope.prepareRefinedStringBackings(): Unit? {
         val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) }
         assert(backingConstraint) ?: return null
         doWithState {
-            boundedStringBackingRefs += ref
+            boundedStringBackingRefs += ref to maxStringLength
             symbolicStringCandidates -= ref
         }
     }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt
index 3cd941ce4b..b308634a5e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt
@@ -14,11 +14,14 @@ import org.usvm.USort
 import org.usvm.api.memcpy
 import org.usvm.collection.array.UArrayRegion
 import org.usvm.collection.array.UArrayRegionId
+import org.usvm.collection.array.length.UArrayLengthsRegionId
 import org.usvm.machine.TsContext
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.state.TsDenseInputArray
 import org.usvm.machine.state.TsState
 import org.usvm.machine.types.TsUnresolvedArrayKind
+import org.usvm.sizeSort
 
 /** Enumerates payload regions independently of whether an array was allocated or came from the input. */
 internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) {
@@ -73,3 +76,40 @@ internal fun TsState.initializeArrayKind(
     )
     memory.setRegion(regionId, initialized)
 }
+
+/** Records that every slot below the current input length has an initialized value. */
+fun TsState.markDenseInputArray(
+    array: UConcreteHeapRef,
+    type: EtsArrayType,
+) = with(ctx) {
+    val descriptor = arrayDescriptorOf(type)
+    val elementSort = typeToSort(type.elementType)
+    require(elementSort !is TsUnresolvedSort) { "A dense input array needs a concrete element sort" }
+
+    val lengthRegionId = UArrayLengthsRegionId<EtsType, TsSizeSort>(sizeSort, descriptor)
+    val elementRegionId = UArrayRegionId<EtsType, USort, TsSizeSort>(descriptor, elementSort)
+    denseInputArrays[array] = TsDenseInputArray(
+        type = type,
+        lengthRegion = memory.getRegion(lengthRegionId),
+        elementRegion = memory.getRegion(elementRegionId),
+    )
+}
+
+/** Returns true only while neither the recorded length nor payload region has changed. */
+internal fun TsState.isUnmodifiedDenseInputArray(
+    array: UConcreteHeapRef,
+    type: EtsArrayType,
+): Boolean = with(ctx) {
+    val snapshot = denseInputArrays[array] ?: return false
+    if (snapshot.type != type) return false
+
+    val descriptor = arrayDescriptorOf(type)
+    val elementSort = typeToSort(type.elementType)
+    if (elementSort is TsUnresolvedSort) return false
+
+    val lengthRegionId = UArrayLengthsRegionId<EtsType, TsSizeSort>(sizeSort, descriptor)
+    val elementRegionId = UArrayRegionId<EtsType, USort, TsSizeSort>(descriptor, elementSort)
+
+    memory.getRegion(lengthRegionId) === snapshot.lengthRegion &&
+        memory.getRegion(elementRegionId) === snapshot.elementRegion
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt
new file mode 100644
index 0000000000..3cd318b9b2
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt
@@ -0,0 +1,153 @@
+package org.usvm.util
+
+import io.ksmt.sort.KFp64Sort
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsStringType
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.api.initializeArrayLength
+import org.usvm.api.memcpy
+import org.usvm.machine.TsSizeSort
+import org.usvm.machine.state.TsState
+import org.usvm.sizeSort
+
+internal val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1)
+
+internal fun TsState.stringCharacters(receiver: UHeapRef): UHeapRef = with(ctx) {
+    memory.read(mkStringBackingLValue(receiver)).asExpr(addressSort)
+}
+
+internal fun TsState.stringLength(receiver: UHeapRef): UExpr<TsSizeSort> {
+    val characters = stringCharacters(receiver)
+    return memory.read(mkStringBackingLengthLValue(characters))
+}
+
+fun TsState.markStringMaxLength(
+    string: UConcreteHeapRef,
+    maxLength: Int,
+) {
+    require(maxLength >= 0) { "String maximum length must be non-negative" }
+    boundedStringBackingRefs += string to maxLength
+}
+
+private fun TsState.trackedStringMaxLength(string: UHeapRef): Int? =
+    boundedStringBackingRefs[string]
+
+internal fun TsState.allocateString(
+    length: UExpr<TsSizeSort>,
+    maxLength: Int? = null,
+): Pair<UConcreteHeapRef, UConcreteHeapRef> = with(ctx) {
+    val string = memory.allocConcrete(EtsStringType)
+    val characters = memory.allocConcrete(STRING_CHARACTER_ARRAY_TYPE.elementType)
+    memory.initializeArrayLength(
+        arrayHeapRef = characters,
+        type = stringBackingArrayDescriptor,
+        sizeSort = sizeSort,
+        count = length,
+    )
+    memory.write(
+        mkStringBackingLValue(string),
+        characters,
+        guard = trueExpr,
+    )
+    if (maxLength != null) {
+        markStringMaxLength(string = string, maxLength = maxLength)
+    }
+
+    string to characters
+}
+
+internal fun TsState.refOrStringTruthy(ref: UHeapRef): UBoolExpr = with(ctx) {
+    val referenceIsTruthy = mkAnd(
+        mkHeapRefEq(ref, mkTsNullValue()).not(),
+        mkHeapRefEq(ref, mkUndefinedValue()).not(),
+    )
+
+    boundedStringBackingRefs.keys.fold(referenceIsTruthy) { fallback, trackedString ->
+        val trackedStringIsNonEmpty = mkEq(stringLength(trackedString), mkBv(0)).not()
+        mkIte(
+            condition = mkHeapRefEq(ref, trackedString),
+            trueBranch = trackedStringIsNonEmpty,
+            falseBranch = fallback,
+        )
+    }
+}
+
+internal fun TsState.copyStringRange(
+    receiver: UHeapRef,
+    from: UExpr<TsSizeSort>,
+    length: UExpr<TsSizeSort>,
+): UConcreteHeapRef = with(ctx) {
+    val source = stringCharacters(receiver)
+    val (result, destination) = allocateString(length, maxLength = trackedStringMaxLength(receiver))
+    memory.memcpy(
+        source,
+        destination,
+        stringBackingArrayDescriptor,
+        bv16Sort,
+        fromSrc = from,
+        fromDst = mkBv(0),
+        length = length,
+    )
+    result
+}
+
+internal fun TsState.concatStrings(
+    left: UHeapRef,
+    right: UHeapRef,
+): UConcreteHeapRef = with(ctx) {
+    val leftCharacters = stringCharacters(left)
+    val rightCharacters = stringCharacters(right)
+    val leftLength = memory.read(mkStringBackingLengthLValue(leftCharacters))
+    val rightLength = memory.read(mkStringBackingLengthLValue(rightCharacters))
+    val resultLength = mkBvAddExpr(leftLength, rightLength)
+    val resultMaxLength = trackedStringMaxLength(left)?.let { leftMaxLength ->
+        trackedStringMaxLength(right)?.let { rightMaxLength ->
+            (leftMaxLength.toLong() + rightMaxLength.toLong())
+                .takeIf { it <= Int.MAX_VALUE }
+                ?.toInt()
+        }
+    }
+    val (result, destination) = allocateString(resultLength, maxLength = resultMaxLength)
+
+    memory.memcpy(
+        leftCharacters,
+        destination,
+        stringBackingArrayDescriptor,
+        bv16Sort,
+        fromSrc = mkBv(0),
+        fromDst = mkBv(0),
+        length = leftLength,
+    )
+    memory.memcpy(
+        rightCharacters,
+        destination,
+        stringBackingArrayDescriptor,
+        bv16Sort,
+        fromSrc = mkBv(0),
+        fromDst = leftLength,
+        length = rightLength,
+    )
+    result
+}
+
+internal fun TsState.stringFromCodeUnit(codeUnit: UExpr<KFp64Sort>): UConcreteHeapRef = with(ctx) {
+    val (result, characters) = allocateString(mkBv(1), maxLength = 1)
+    val value = mkFpToBvExpr(
+        roundingMode = fpRoundingModeSortDefaultValue(),
+        value = codeUnit,
+        bvSize = bv16Sort.sizeBits.toInt(),
+        isSigned = false,
+    ).asExpr(bv16Sort)
+    val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0))
+    memory.write(
+        character,
+        value,
+        guard = trueExpr,
+    )
+    result
+}
diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts
index b464a89de8..fcc28f3c09 100644
--- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts
+++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts
@@ -2,6 +2,7 @@ declare class StringModelPrimitives {
     static length(receiver: string): number;
     static codeUnitAt(receiver: string, index: number): number;
     static fromCodeUnit(codeUnit: number): string;
+    static copyRange(receiver: string, start: number, end: number): string;
 }
 
 export class StringModels {
@@ -60,6 +61,43 @@ export class StringModels {
         return StringModelPrimitives.codeUnitAt(receiver, integerIndex);
     }
 
+    static slice(receiver: string, start: number, end: number): string {
+        const length = StringModelPrimitives.length(receiver);
+        const from = StringModels.normalizeSliceIndex(start, length);
+        const to = StringModels.normalizeSliceIndex(end, length);
+        return StringModelPrimitives.copyRange(receiver, from, to < from ? from : to);
+    }
+
+    static toUpperCase(receiver: string): string {
+        const length = StringModelPrimitives.length(receiver);
+        let result = "";
+        let index = 0;
+        while (index < length) {
+            let codeUnit = StringModelPrimitives.codeUnitAt(receiver, index);
+            if (codeUnit >= 0x61 && codeUnit <= 0x7a) {
+                codeUnit -= 0x20;
+            }
+            result += StringModelPrimitives.fromCodeUnit(codeUnit);
+            index++;
+        }
+        return result;
+    }
+
+    static toLowerCase(receiver: string): string {
+        const length = StringModelPrimitives.length(receiver);
+        let result = "";
+        let index = 0;
+        while (index < length) {
+            let codeUnit = StringModelPrimitives.codeUnitAt(receiver, index);
+            if (codeUnit >= 0x41 && codeUnit <= 0x5a) {
+                codeUnit += 0x20;
+            }
+            result += StringModelPrimitives.fromCodeUnit(codeUnit);
+            index++;
+        }
+        return result;
+    }
+
     static startsWith(receiver: string, searchString: string, position: number): boolean {
         const length = StringModelPrimitives.length(receiver);
         const searchLength = StringModelPrimitives.length(searchString);
@@ -178,4 +216,22 @@ export class StringModels {
 
         return Math.floor(value);
     }
+
+    private static normalizeSliceIndex(value: number, length: number): number {
+        if (value !== value) {
+            return 0;
+        }
+        if (value === Infinity) {
+            return length;
+        }
+        if (value === -Infinity) {
+            return 0;
+        }
+
+        const integer = value < 0 ? -Math.floor(-value) : Math.floor(value);
+        if (integer < 0) {
+            return integer + length < 0 ? 0 : integer + length;
+        }
+        return integer > length ? length : integer;
+    }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt
new file mode 100644
index 0000000000..3c97711091
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt
@@ -0,0 +1,81 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Test
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.getResourcePath
+import kotlin.test.assertTrue
+
+class StringModelBackingBoundaryTest : TsMethodTestRunner() {
+    override val scene = EtsScene(
+        listOf(
+            loadEtsFileAutoConvert(
+                getResourcePath("/models/StringModelBackingBoundary.ts"),
+                provider = EtsIrProvider.TS_FRONTEND,
+            ),
+        ),
+    )
+
+    override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, options ->
+        TsMachine(scene = scene, options = options, tsOptions = TsOptions(maxArraySize = 12)).use { machine ->
+            machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+    }
+
+    @Test
+    fun `derived strings compare their full contents within the configured bound`() {
+        discoverProperties<TsTestValue.TsString, TsTestValue.TsBoolean>(
+            method = getMethod(methodName = "equalDerived", className = "StringModelBackingBoundary"),
+            { _, result -> result.value },
+            invariants = arrayOf({ _, result -> result.value }),
+        )
+    }
+
+    @Test
+    fun `derived string length uses the configured bound`() {
+        discoverProperties<TsTestValue.TsString, TsTestValue.TsNumber>(
+            method = getMethod(methodName = "derivedLength", className = "StringModelBackingBoundary"),
+            { input, result -> result.number == input.value.length + 10.0 },
+            invariants = arrayOf({ input, result -> result.number == input.value.length + 10.0 }),
+        )
+    }
+
+    @Test
+    fun `derived string witnesses retain their full contents`() {
+        discoverProperties<TsTestValue.TsString, TsTestValue.TsString>(
+            method = getMethod(methodName = "returnedDerived", className = "StringModelBackingBoundary"),
+            { input, result -> result.value == input.value + "0123456789" },
+            invariants = arrayOf({ input, result -> result.value == input.value + "0123456789" }),
+        )
+    }
+
+    @Test
+    fun `concatenation beyond the configured bound remains unsupported`() {
+        for (methodName in listOf("equalDerived", "derivedLength", "returnedDerived")) {
+            val method = getMethod(methodName = methodName, className = "StringModelBackingBoundary")
+
+            val analysis = TsMachine(
+                scene = scene,
+                options = UMachineOptions(),
+                tsOptions = TsOptions(maxArraySize = 2),
+            ).use { machine ->
+                machine.analyzeWithOutcome(methods = listOf(method))
+            }
+
+            assertTrue(analysis.states.isEmpty(), methodName)
+            assertTrue(
+                analysis.unsupportedPaths.any { "result exceeds the configured length bound" in it },
+                "$methodName: ${analysis.unsupportedPaths}",
+            )
+        }
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt
new file mode 100644
index 0000000000..5357ecd578
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt
@@ -0,0 +1,147 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.machine.call.intrinsic.TsArrayIsArrayIntrinsicModel
+import org.usvm.util.TsTestResolver
+import org.usvm.util.getResourcePath
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertFalse
+import kotlin.test.assertIs
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+class TsArrayIsArrayIntrinsicModelTest {
+    private val sourceFile = loadEtsFileAutoConvert(
+        getResourcePath("/models/ArrayIsArrayIntrinsicModel.ts"),
+        provider = EtsIrProvider.TS_FRONTEND,
+    )
+    private val scene = EtsScene(projectFiles = listOf(sourceFile))
+
+    @Test
+    fun `scalars are not arrays`() {
+        val result = analyze("scalarValuesAreNotArrays", "missingArgumentIsNotArray")
+
+        assertTrue(result.values.values.all { values -> assertIs<TsTestValue.TsBoolean>(values.single()).value })
+        assertEquals(
+            List(size = 6) { TsArrayIsArrayIntrinsicModel.MODEL_ID },
+            result.modelIds,
+        )
+    }
+
+    @Test
+    fun `ordinary arrays are arrays`() {
+        val result = analyze("ordinaryArraysAreArrays")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.getValue("ordinaryArraysAreArrays").single()).value)
+        assertEquals(
+            List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID },
+            result.modelIds,
+        )
+    }
+
+    @Test
+    fun `null and undefined parameters are not arrays`() {
+        val result = analyze("nullParameterIsNotArray", "undefinedParameterIsNotArray")
+
+        result.values.values.forEach { values ->
+            assertFalse(assertIs<TsTestValue.TsBoolean>(values.single()).value)
+        }
+        assertEquals(
+            List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID },
+            result.modelIds,
+        )
+    }
+
+    @Test
+    fun `string and nested array parameters are arrays`() {
+        val result = analyze("stringArrayIsArray", "nestedArrayIsArray")
+
+        result.values.values.forEach { values ->
+            assertTrue(assertIs<TsTestValue.TsBoolean>(values.single()).value)
+        }
+        assertEquals(
+            List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID },
+            result.modelIds,
+        )
+    }
+
+    @Test
+    fun `non builtin isArray call is not claimed by the model`() {
+        val result = analyze("nonBuiltinIsArrayFallsBack")
+
+        assertTrue(result.modelIds.isEmpty())
+        assertTrue(result.events.none { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED })
+    }
+
+    private fun analyze(vararg methodNames: String): AnalysisResult {
+        val methods = methodNames.associateWith(::method)
+        val observer = RecordingUnknownCallObserver()
+
+        return TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.STOP_PATH),
+            observer = observer,
+        ).use { machine ->
+            val states = machine.analyze(methods.values.toList())
+            val values = methods.mapValues { (_, method) ->
+                states.filter { state -> state.entrypoint === method }
+                    .map { state -> TsTestResolver().resolve(method, state).returnValue }
+            }
+
+            AnalysisResult(
+                values = values,
+                events = observer.events.toList(),
+            )
+        }
+    }
+
+    private fun method(name: String): EtsMethod = scene.projectClasses
+        .single { clazz -> clazz.name == DEFAULT_ARK_CLASS_NAME && clazz.declaringFile === sourceFile }
+        .methods
+        .single { method -> method.name == name }
+
+    private class RecordingUnknownCallObserver : TsInterpreterObserver {
+        val events = mutableListOf<TsUnknownCallEvent>()
+
+        override fun onUnknownCall(event: TsUnknownCallEvent) {
+            events += event
+        }
+    }
+
+    private data class AnalysisResult(
+        val values: Map<String, List<TsTestValue>>,
+        val events: List<TsUnknownCallEvent>,
+    ) {
+        val modelIds: List<String> = events.mapNotNull { event ->
+            (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId
+        }
+    }
+
+    private companion object {
+        val machineOptions = UMachineOptions(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            exceptionsPropagation = true,
+            throwExceptionOnStepFailure = true,
+            timeout = Duration.INFINITE,
+            stepsFromLastCovered = 1_000L,
+            solverType = SolverType.YICES,
+            solverTimeout = Duration.INFINITE,
+            typeOperationsTimeout = Duration.INFINITE,
+        )
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt
index e8d3ee2963..a0152c12b6 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsSequenceEtsIrModelTest.kt
@@ -242,6 +242,122 @@ class TsSequenceEtsIrModelTest {
         assertTrue("ts.string.lastIndexOf" in result.modelIds)
     }
 
+    @Test
+    fun `string slice copies exact UTF16 code units`() {
+        val result = analyze(methodName = "stringSlicePreservesUtf16")
+
+        assertEquals("😀", assertIs<TsTestValue.TsString>(result.values.single()).value)
+        assertTrue("ts.string.slice" in result.modelIds)
+    }
+
+    @Test
+    fun `modeled strings compare by UTF-16 value`() {
+        val result = analyze(methodName = "stringModelsUseValueEquality")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.single()).value)
+        assertTrue("ts.string.slice" in result.modelIds)
+    }
+
+    @Test
+    fun `non-string references retain identity equality`() {
+        val result = analyze(methodName = "stringEqualityPreservesReferenceIdentity")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.single()).value)
+    }
+
+    @Test
+    fun `fake reference strings compare by UTF-16 value`() {
+        val result = analyze(methodName = "stringValueEqualityThroughAny")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.single()).value)
+    }
+
+    @Test
+    fun `string truthiness follows UTF-16 length`() {
+        val result = analyze(methodName = "stringTruthinessUsesLength")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.single()).value)
+    }
+
+    @Test
+    fun `non-string truthiness does not read string storage`() {
+        val result = analyze(methodName = "nonStringTruthinessDoesNotReadStringStorage")
+
+        assertTrue(assertIs<TsTestValue.TsBoolean>(result.values.single()).value)
+    }
+
+    @Test
+    fun `mixed object equality does not read string storage`() {
+        val result = analyze(methodName = "mixedObjectEqualityDoesNotReadStringStorage")
+
+        assertTrue(result.values.isNotEmpty())
+        assertTrue(result.values.all { value -> assertIs<TsTestValue.TsBoolean>(value).value })
+    }
+
+    @Test
+    fun `ASCII casing composes with charAt slice and concatenation`() {
+        val capitalized = analyze(methodName = "stringCapitalizeAscii")
+        val empty = analyze(methodName = "stringCapitalizeEmpty")
+
+        assertEquals("Hello", assertIs<TsTestValue.TsString>(capitalized.values.single()).value)
+        assertEquals("", assertIs<TsTestValue.TsString>(empty.values.single()).value)
+        assertTrue(setOf("ts.string.toUpperCase", "ts.string.toLowerCase").all(capitalized.modelIds::contains))
+    }
+
+    @Test
+    fun `ASCII casing leaves non ASCII strings to residual fallback`() {
+        val result = analyze(methodName = "stringCapitalizeNonAscii")
+
+        assertTrue(result.values.isEmpty())
+        assertTrue(result.events.any { event -> event.outcome == TsUnknownCallOutcome.PATH_STOPPED })
+    }
+
+    @Test
+    fun `legacy approximations use observable residual fallback with empty stop catalog`() {
+        val methodNames = listOf(
+            "legacyArrayConcat",
+            "legacyArrayFill",
+            "legacyArrayJoin",
+            "legacyArrayPush",
+            "legacyArrayReverse",
+            "legacyArraySlice",
+            "legacyArrayToString",
+            "legacyArrayUnshift",
+        )
+        val options = TsOptions(
+            unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()),
+            unknownCallFallback = TsResidualCallPolicy.STOP_PATH,
+        )
+
+        methodNames.forEach { methodName ->
+            val result = analyze(methodName = methodName, tsOptions = options)
+
+            assertTrue(result.values.isEmpty(), methodName)
+            assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map(TsUnknownCallEvent::outcome))
+            assertTrue(result.events.single().decision is TsUnknownCallDecision.ResidualFallback, methodName)
+            assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, result.events.single().failureReason)
+        }
+    }
+
+    @Test
+    fun `legacy join uses fresh residual result instead of sentinel with empty fresh catalog`() {
+        val result = analyze(
+            methodName = "legacyArrayJoin",
+            tsOptions = TsOptions(
+                unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()),
+                unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+            ),
+        )
+
+        assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), result.events.map(TsUnknownCallEvent::outcome))
+        assertEquals(1, result.values.size)
+        assertTrue(
+            result.values.none { value ->
+                value is TsTestValue.TsString && value.value == "joined_array_result"
+            },
+        )
+    }
+
     private fun analyze(
         methodName: String,
         tsOptions: TsOptions = TsOptions(),
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
index ef0f1c60d7..4087d318bd 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -73,7 +73,8 @@ class TsTestResolver {
             memory,
             method,
             resolvedLValuesToFakeObjects,
-            state.maxStringLength
+            state.maxStringLength,
+            state.boundedStringBackingRefs,
         )
         val afterMemoryScope = MemoryScope(
             this,
@@ -81,7 +82,8 @@ class TsTestResolver {
             memory,
             method,
             resolvedLValuesToFakeObjects,
-            state.maxStringLength
+            state.maxStringLength,
+            state.boundedStringBackingRefs,
         )
 
         val result = when (val res = state.methodResult) {
@@ -177,7 +179,16 @@ class TsTestResolver {
         method: EtsMethod,
         resolvedLValuesToFakeObjects: List<Pair<ULValue<*, *>, UConcreteHeapRef>>,
         maxStringLength: Int,
-    ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects, maxStringLength) {
+        stringLengthBounds: Map<UHeapRef, Int>,
+    ) : TsTestStateResolver(
+        ctx,
+        model,
+        finalStateMemory,
+        method,
+        resolvedLValuesToFakeObjects,
+        maxStringLength,
+        stringLengthBounds,
+    ) {
         fun resolveState(): TsParametersState {
             val thisInstance = resolveThisInstance()
             val parameters = resolveParameters()
@@ -194,6 +205,7 @@ open class TsTestStateResolver(
     val method: EtsMethod,
     val resolvedLValuesToFakeObjects: List<Pair<ULValue<*, *>, UConcreteHeapRef>>,
     val maxStringLength: Int,
+    private val stringLengthBounds: Map<UHeapRef, Int>,
 ) {
     fun resolveLValue(
         lValue: ULValue<*, *>,
@@ -341,7 +353,8 @@ open class TsTestStateResolver(
 
         val lengthLValue = mkStringBackingLengthLValue(charsRef)
         val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt()
-        require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" }
+        val lengthBound = stringLengthBounds[heapRef] ?: stringLengthBounds[concreteRef] ?: maxStringLength
+        require(length in 0..lengthBound) { "Unsupported symbolic string length: $length" }
 
         val value = buildString(length) {
             repeat(length) { index ->
diff --git a/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts
new file mode 100644
index 0000000000..22515dc2ed
--- /dev/null
+++ b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts
@@ -0,0 +1,38 @@
+export function scalarValuesAreNotArrays(): boolean {
+    return !Array.isArray(42)
+        && !Array.isArray(true)
+        && !Array.isArray('value')
+        && !Array.isArray(undefined)
+        && !Array.isArray(null);
+}
+
+export function ordinaryArraysAreArrays(): boolean {
+    return Array.isArray([]) && Array.isArray([1, 2, 3]);
+}
+
+export function stringArrayIsArray(value: string[]): boolean {
+    return Array.isArray(value);
+}
+
+export function nestedArrayIsArray(value: number[][]): boolean {
+    return Array.isArray(value);
+}
+
+export function missingArgumentIsNotArray(): boolean {
+    // @ts-expect-error Arity test deliberately omits the first argument.
+    return !Array.isArray();
+}
+
+export function nullParameterIsNotArray(value: null): boolean {
+    return Array.isArray(value);
+}
+
+export function undefinedParameterIsNotArray(value: undefined): boolean {
+    return Array.isArray(value);
+}
+
+declare const FakeArray: any;
+
+export function nonBuiltinIsArrayFallsBack(): boolean {
+    return FakeArray.isArray([]);
+}
diff --git a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts
index 0a34f10342..9c6cbde6c6 100644
--- a/usvm-ts/src/test/resources/models/SequenceEtsIr.ts
+++ b/usvm-ts/src/test/resources/models/SequenceEtsIr.ts
@@ -128,4 +128,99 @@ export class SequenceEtsIr {
             + "ababa".lastIndexOf("ba", 2) * 10
             + "ababa".lastIndexOf("", Infinity);
     }
+
+    stringSlicePreservesUtf16(): string {
+        return "A😀Z".slice(1, 3);
+    }
+
+    stringModelsUseValueEquality(): boolean {
+        const whole = "abc".slice(0);
+        const independent = "abc".slice(0);
+        const empty = "abc".slice(0, 0);
+
+        return whole === "abc"
+            && whole == "abc"
+            && whole === independent
+            && empty === ""
+            && empty === "x".slice(1)
+            && empty !== "a"
+            && whole + "d" === "abcd";
+    }
+
+    stringEqualityPreservesReferenceIdentity(): boolean {
+        const alias: number[] = [1];
+        return alias === alias && alias !== [1];
+    }
+
+    stringValueEqualityThroughAny(): boolean {
+        const whole: any = "abc".slice(0);
+        const empty: any = "abc".slice(0, 0);
+        return whole === "abc" && whole == "abc" && empty === "";
+    }
+
+    stringTruthinessUsesLength(): boolean {
+        const empty = "abc".slice(0, 0);
+        const nonEmpty = "abc".slice(0, 1);
+        return !empty && !"" && !!nonEmpty;
+    }
+
+    nonStringTruthinessDoesNotReadStringStorage(): boolean {
+        const object = { value: 1 };
+        const array: number[] = [];
+        return !undefined && !null && !!object && !!array;
+    }
+
+    mixedObjectEqualityDoesNotReadStringStorage(index: number): boolean {
+        if (index !== 0 && index !== 1) return true;
+        const dummy = "x";
+        const values: any[] = [{}, {}];
+        return values[index] !== "";
+    }
+
+    stringCapitalizeAscii(): string {
+        const value = "hELLO";
+        return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase();
+    }
+
+    stringCapitalizeEmpty(): string {
+        const value = "";
+        return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase();
+    }
+
+    stringCapitalizeNonAscii(): string {
+        const value = "éCOLE";
+        return value.charAt(0).toUpperCase() + value.slice(1).toLowerCase();
+    }
+
+    legacyArrayPush(): number {
+        return [1].push(2);
+    }
+
+    legacyArrayFill(): number[] {
+        return [1].fill(2);
+    }
+
+    legacyArrayUnshift(): number {
+        return [1].unshift(2);
+    }
+
+    legacyArrayJoin(): string {
+        return [1, 2].join("-");
+    }
+
+    legacyArraySlice(): number[] {
+        return [1, 2].slice(1);
+    }
+
+    legacyArrayConcat(): number[] {
+        return [1].concat([2]);
+    }
+
+    legacyArrayReverse(): number[] {
+        return [1, 2].reverse();
+    }
+
+    legacyArrayToString(): string {
+        return [1, 2].toString();
+    }
 }
diff --git a/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts b/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts
new file mode 100644
index 0000000000..7f01e2b21c
--- /dev/null
+++ b/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts
@@ -0,0 +1,16 @@
+export class StringModelBackingBoundary {
+    equalDerived(value: string): boolean {
+        const left = value + "0123456789";
+        const right = value + "0123456789";
+
+        return left === right;
+    }
+
+    derivedLength(value: string): number {
+        return (value + "0123456789").length;
+    }
+
+    returnedDerived(value: string): string {
+        return value + "0123456789";
+    }
+}