diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs
index 58755a0bffae..951e58f9a954 100644
--- a/cprover_bindings/src/goto_program/stmt.rs
+++ b/cprover_bindings/src/goto_program/stmt.rs
@@ -57,6 +57,8 @@ pub enum StmtBody {
     Break,
     /// `continue;`
     Continue,
+    /// End-of-life of a local variable
+    Dead(Expr),
     /// `lhs.typ lhs = value;` or `lhs.typ lhs;`
     Decl {
         lhs: Expr, // SymbolExpr
@@ -232,6 +234,11 @@ impl Stmt {
         BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc)
     }
 
+    /// Local variable goes out of scope
+    pub fn dead(symbol: Expr, loc: Location) -> Self {
+        stmt!(Dead(symbol), loc)
+    }
+
     /// `lhs.typ lhs = value;` or `lhs.typ lhs;`
     pub fn decl(lhs: Expr, value: Option<Expr>, loc: Location) -> Self {
         assert!(lhs.is_symbol());
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 16b8b69c8fe7..5c17ecf87b5d 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -433,6 +433,7 @@ impl ToIrep for StmtBody {
             }
             StmtBody::Break => code_irep(IrepId::Break, vec![]),
             StmtBody::Continue => code_irep(IrepId::Continue, vec![]),
+            StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
             StmtBody::Decl { lhs, value } => {
                 if value.is_some() {
                     code_irep(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 9296b713c862..6b764fb63365 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Codegen for a local
-    fn codegen_local(&mut self, l: Local) -> Expr {
+    pub fn codegen_local(&mut self, l: Local) -> Expr {
         let local_ty = self.local_ty_stable(l);
         // Check if the local is a function definition (see comment above)
         if let Some(fn_def) = self.codegen_local_fndef(local_ty) {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 05b153f9583f..6379a023423f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -75,8 +75,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 .goto_expr;
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
-            StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
-            StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
+            StatementKind::StorageLive(var_id) => {
+                Stmt::decl(self.codegen_local(*var_id), None, location)
+            }
+            StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location),
             StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
                 CopyNonOverlapping { src, dst, count },
             )) => {
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 9b6e0598daa5..fc41bac69d9c 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -122,6 +122,8 @@ impl KaniSession {
                 "symbol-mangling-version=v0",
                 "-Z",
                 "panic_abort_tests=yes",
+                "-Z",
+                "sanitizer=address",
             ]
             .map(OsString::from),
         );
diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected
index 7a9fef1ca77c..97ffbe1d96e4 100644
--- a/tests/coverage/reachable/assert-false/expected
+++ b/tests/coverage/reachable/assert-false/expected
@@ -1,8 +1,8 @@
 coverage/reachable/assert-false/main.rs, 6, FULL
 coverage/reachable/assert-false/main.rs, 7, FULL
-coverage/reachable/assert-false/main.rs, 11, FULL
-coverage/reachable/assert-false/main.rs, 12, FULL
-coverage/reachable/assert-false/main.rs, 15, FULL
+coverage/reachable/assert-false/main.rs, 11, PARTIAL
+coverage/reachable/assert-false/main.rs, 12, PARTIAL
+coverage/reachable/assert-false/main.rs, 15, PARTIAL
 coverage/reachable/assert-false/main.rs, 16, FULL
 coverage/reachable/assert-false/main.rs, 17, PARTIAL
 coverage/reachable/assert-false/main.rs, 19, FULL
diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected
index 67ae085a3e83..9d21185b3a83 100644
--- a/tests/coverage/reachable/assert/reachable_pass/expected
+++ b/tests/coverage/reachable/assert/reachable_pass/expected
@@ -1,4 +1,4 @@
 coverage/reachable/assert/reachable_pass/test.rs, 6, FULL
-coverage/reachable/assert/reachable_pass/test.rs, 7, FULL
+coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL
 coverage/reachable/assert/reachable_pass/test.rs, 8, FULL
 coverage/reachable/assert/reachable_pass/test.rs, 10, FULL
diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected
index af2f30e51fe2..fedfec8b2a1e 100644
--- a/tests/coverage/reachable/bounds/reachable_fail/expected
+++ b/tests/coverage/reachable/bounds/reachable_fail/expected
@@ -1,4 +1,4 @@
 coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL
 coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE
-coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL
+coverage/reachable/bounds/reachable_fail/test.rs, 10, PARTIAL
 coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected
index 1ec1abefffd8..c1ac77404680 100644
--- a/tests/coverage/reachable/div-zero/reachable_fail/expected
+++ b/tests/coverage/reachable/div-zero/reachable_fail/expected
@@ -1,4 +1,4 @@
 coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL
 coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE
-coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL
+coverage/reachable/div-zero/reachable_fail/test.rs, 10, PARTIAL
 coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected
index f20826fb1a8e..d45edcc37a63 100644
--- a/tests/coverage/reachable/overflow/reachable_fail/expected
+++ b/tests/coverage/reachable/overflow/reachable_fail/expected
@@ -1,5 +1,5 @@
 coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL
 coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL
 coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL
-coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL
+coverage/reachable/overflow/reachable_fail/test.rs, 14, PARTIAL
 coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE
diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected
index f7fa6ed7efeb..7852461e4f57 100644
--- a/tests/coverage/reachable/rem-zero/reachable_fail/expected
+++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected
@@ -1,4 +1,4 @@
 coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL
 coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE
-coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL
+coverage/reachable/rem-zero/reachable_fail/test.rs, 10, PARTIAL
 coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected
index f5b5f8044769..9bc6d8faa4f9 100644
--- a/tests/coverage/unreachable/assert/expected
+++ b/tests/coverage/unreachable/assert/expected
@@ -1,6 +1,6 @@
 coverage/unreachable/assert/test.rs, 6, FULL
-coverage/unreachable/assert/test.rs, 7, FULL
-coverage/unreachable/assert/test.rs, 9, FULL
+coverage/unreachable/assert/test.rs, 7, PARTIAL
+coverage/unreachable/assert/test.rs, 9, PARTIAL
 coverage/unreachable/assert/test.rs, 10, NONE
 coverage/unreachable/assert/test.rs, 12, NONE
 coverage/unreachable/assert/test.rs, 16, FULL
diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected
index f4e7608b2c13..9b13c3c96ded 100644
--- a/tests/coverage/unreachable/assert_eq/expected
+++ b/tests/coverage/unreachable/assert_eq/expected
@@ -1,5 +1,5 @@
 coverage/unreachable/assert_eq/test.rs, 6, FULL
 coverage/unreachable/assert_eq/test.rs, 7, FULL
-coverage/unreachable/assert_eq/test.rs, 8, FULL
+coverage/unreachable/assert_eq/test.rs, 8, PARTIAL
 coverage/unreachable/assert_eq/test.rs, 9, NONE
 coverage/unreachable/assert_eq/test.rs, 11, FULL
diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected
index 3b57defb4c36..f027f432e280 100644
--- a/tests/coverage/unreachable/assert_ne/expected
+++ b/tests/coverage/unreachable/assert_ne/expected
@@ -1,6 +1,6 @@
 coverage/unreachable/assert_ne/test.rs, 6, FULL
 coverage/unreachable/assert_ne/test.rs, 7, FULL
 coverage/unreachable/assert_ne/test.rs, 8, FULL
-coverage/unreachable/assert_ne/test.rs, 10, FULL
+coverage/unreachable/assert_ne/test.rs, 10, PARTIAL
 coverage/unreachable/assert_ne/test.rs, 11, NONE
 coverage/unreachable/assert_ne/test.rs, 14, FULL
diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected
index 214cbfa827bd..a2d296f0f9a3 100644
--- a/tests/coverage/unreachable/check_id/expected
+++ b/tests/coverage/unreachable/check_id/expected
@@ -1,5 +1,5 @@
 coverage/unreachable/check_id/main.rs, 5, FULL
-coverage/unreachable/check_id/main.rs, 6, FULL
+coverage/unreachable/check_id/main.rs, 6, PARTIAL
 coverage/unreachable/check_id/main.rs, 8, NONE
 coverage/unreachable/check_id/main.rs, 10, FULL
 coverage/unreachable/check_id/main.rs, 14, FULL
@@ -12,5 +12,5 @@ coverage/unreachable/check_id/main.rs, 20, FULL
 coverage/unreachable/check_id/main.rs, 21, FULL
 coverage/unreachable/check_id/main.rs, 22, FULL
 coverage/unreachable/check_id/main.rs, 23, FULL
-coverage/unreachable/check_id/main.rs, 24, FULL
+coverage/unreachable/check_id/main.rs, 24, PARTIAL
 coverage/unreachable/check_id/main.rs, 25, NONE
diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected
index 4460f23a80de..8b481863a163 100644
--- a/tests/coverage/unreachable/if-statement/expected
+++ b/tests/coverage/unreachable/if-statement/expected
@@ -1,4 +1,4 @@
-coverage/unreachable/if-statement/main.rs, 5, FULL
+coverage/unreachable/if-statement/main.rs, 5, PARTIAL
 coverage/unreachable/if-statement/main.rs, 7, PARTIAL
 coverage/unreachable/if-statement/main.rs, 8, NONE
 coverage/unreachable/if-statement/main.rs, 9, NONE
diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected
index cf45a502d295..624aa520edc9 100644
--- a/tests/coverage/unreachable/tutorial_unreachable/expected
+++ b/tests/coverage/unreachable/tutorial_unreachable/expected
@@ -1,5 +1,5 @@
 coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL
 coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL
-coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL
+coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL
 coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE
 coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL
diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected
index a0e43c183846..dc66d3e823d3 100644
--- a/tests/coverage/unreachable/while-loop-break/expected
+++ b/tests/coverage/unreachable/while-loop-break/expected
@@ -1,5 +1,5 @@
 coverage/unreachable/while-loop-break/main.rs, 8, FULL
-coverage/unreachable/while-loop-break/main.rs, 9, FULL
+coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL
 coverage/unreachable/while-loop-break/main.rs, 10, FULL
 coverage/unreachable/while-loop-break/main.rs, 11, FULL
 coverage/unreachable/while-loop-break/main.rs, 13, FULL
diff --git a/tests/expected/dead-invalid-access-via-raw/expected b/tests/expected/dead-invalid-access-via-raw/expected
new file mode 100644
index 000000000000..1d464eb5f031
--- /dev/null
+++ b/tests/expected/dead-invalid-access-via-raw/expected
@@ -0,0 +1,16 @@
+SUCCESS\
+address must be a multiple of its type's alignment
+FAILURE\
+unsafe { *raw_ptr } == 10
+SUCCESS\
+pointer NULL
+SUCCESS\
+pointer invalid
+SUCCESS\
+deallocated dynamic object
+FAILURE\
+dead object
+SUCCESS\
+pointer outside object bounds
+SUCCESS\
+invalid integer address
diff --git a/tests/expected/dead-invalid-access-via-raw/main.rs b/tests/expected/dead-invalid-access-via-raw/main.rs
new file mode 100644
index 000000000000..ed3ea655839e
--- /dev/null
+++ b/tests/expected/dead-invalid-access-via-raw/main.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// This test checks an issue reported in github.com/model-checking/kani#3063.
+// The access of the raw pointer should fail because the value being dereferenced has gone out of
+// scope at the time of access.
+
+#[kani::proof]
+pub fn check_invalid_ptr() {
+    let raw_ptr = {
+        let var = 10;
+        &var as *const _
+    };
+
+    // This should fail since it is de-referencing a dead object.
+    assert_eq!(unsafe { *raw_ptr }, 10);
+}