diff --git a/src/main/scala/analysis/InterLiveVarsAnalysis.scala b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
index d1c794c76..d1c4a8552 100644
--- a/src/main/scala/analysis/InterLiveVarsAnalysis.scala
+++ b/src/main/scala/analysis/InterLiveVarsAnalysis.scala
@@ -17,6 +17,9 @@ import ir.{
   Return,
   Variable
 }
+import util.Logger
+
+import scala.collection.immutable.ListSet
 
 /** Micro-transfer-functions for LiveVar analysis
  *  This analysis works by inlining function calls - instead of just mapping parameters and returns, all live variables
@@ -136,6 +139,56 @@ trait LiveVarsAnalysisFunctions(inline: Boolean, addExternals: Boolean = true)
   }
 }
 
-class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false)
-    extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program),
+class InterLiveVarsAnalysis(program: Program, ignoreExternals: Boolean = false, entry: Option[Procedure] = None)
+    extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program, entry),
       LiveVarsAnalysisFunctions(true, !ignoreExternals)
+
+def interLiveVarsAnalysis(
+  program: Program,
+  ignoreExternals: Boolean = false
+): Map[CFGPosition, Map[Variable, TwoElement]] = {
+
+  var procs = ListSet.from(program.procedures)
+  var starts = List[Procedure]()
+
+  while {
+    val entries =
+      procs.toList.filter(p => p.incomingCalls().size == 0 && p.entryBlock.isDefined && p.returnBlock.isDefined)
+    if (entries.nonEmpty) {
+      starts = entries.head :: starts
+      val done = entries.head.reachableFrom
+      procs = procs -- done
+      procs.nonEmpty
+    } else {
+      Logger.warn(s"Live vars :: no program entry candidates remaining")
+      false
+    }
+  } do {}
+
+  val reachable = starts.toSet.flatMap(_.reachableFrom)
+  if (
+    !(reachable.contains(
+      program.mainProcedure
+    )) && procs.nonEmpty && program.mainProcedure.entryBlock.isDefined && program.mainProcedure.returnBlock.isDefined
+  ) {
+    Logger.warn(
+      s"mainProcedure has predecessors but is not reachable from an entry-candidate, using it as an entry candidate."
+    )
+    val remaining = program.procedures.toSet -- program.mainProcedure.reachableFrom
+    starts = List(program.mainProcedure)
+    procs = procs -- program.mainProcedure.reachableFrom
+  } else if (!reachable.contains(program.mainProcedure)) {
+    Logger.warn(s"mainProcedure ${program.mainProcedure.name} is a stub and is not reachable from any entry point")
+  }
+
+  if (procs.nonEmpty) {
+    Logger.error(s"Code unreachable for liveness analysis: ${procs.toList}")
+  }
+
+  var r = Map[CFGPosition, Map[Variable, TwoElement]]()
+  for (p <- starts) {
+    r = r ++ InterLiveVarsAnalysis(program, ignoreExternals, Some(p)).analyze()
+  }
+  r
+
+}
diff --git a/src/main/scala/analysis/solvers/IDESolver.scala b/src/main/scala/analysis/solvers/IDESolver.scala
index a711da891..104fa90bf 100644
--- a/src/main/scala/analysis/solvers/IDESolver.scala
+++ b/src/main/scala/analysis/solvers/IDESolver.scala
@@ -245,21 +245,14 @@ abstract class IDESolver[
   }
 
   def analyze(): Map[CFGPosition, Map[D, T]] = {
-    if (
-      program.mainProcedure.blocks.nonEmpty && program.mainProcedure.returnBlock.isDefined && program.mainProcedure.entryBlock.isDefined
-    ) {
-      val phase1 = Phase1()
-      val phase2 = Phase2(phase1)
-      phase2.restructure(phase2.analyze())
-    } else {
-      Logger.warn(s"Disabling IDE solver tests due to external main procedure: ${program.mainProcedure.name}")
-      Map()
-    }
+    val phase1 = Phase1()
+    val phase2 = Phase2(phase1)
+    phase2.restructure(phase2.analyze())
   }
 }
 
-abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
-    extends IDESolver[Procedure, Return, DirectCall, Command, D, T, L](program, program.mainProcedure),
+abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry: Option[Procedure] = None)
+    extends IDESolver[Procedure, Return, DirectCall, Command, D, T, L](program, entry.getOrElse(program.mainProcedure)),
       ForwardIDEAnalysis[D, T, L],
       IRInterproceduralForwardDependencies {
 
@@ -302,10 +295,12 @@ abstract class ForwardIDESolver[D, T, L <: Lattice[T]](program: Program)
     InterProcIRCursor.succ(exit).filter(_.isInstanceOf[Command]).map(_.asInstanceOf[Command])
 }
 
-abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program)
+abstract class BackwardIDESolver[D, T, L <: Lattice[T]](program: Program, entry: Option[Procedure] = None)
     extends IDESolver[Return, Procedure, Command, DirectCall, D, T, L](
-      program,
-      IRWalk.lastInProc(program.mainProcedure).getOrElse(program.mainProcedure)
+      program, {
+        val e = entry.getOrElse(program.mainProcedure)
+        IRWalk.lastInProc(e).getOrElse(e)
+      }
     ),
       BackwardIDEAnalysis[D, T, L],
       IRInterproceduralBackwardDependencies {
diff --git a/src/main/scala/ir/invariant/ReadUninitialised.scala b/src/main/scala/ir/invariant/ReadUninitialised.scala
new file mode 100644
index 000000000..a301de2b6
--- /dev/null
+++ b/src/main/scala/ir/invariant/ReadUninitialised.scala
@@ -0,0 +1,74 @@
+package ir.invariant
+
+import ir.*
+import util.Logger
+
+import scala.collection.mutable
+
+class ReadUninitialised() {
+
+  var init = Set[Variable]()
+  var readUninit = List[(Command, Set[Variable])]()
+
+  final def check(a: Command) = {
+    val free = freeVarsPos(a).filter(_.isInstanceOf[LocalVar]) -- init
+    if (free.size > 0) {
+      readUninit = (a, free) :: readUninit
+    }
+  }
+
+  final def readUninitialised(b: Iterable[Statement]): Boolean = {
+    val i = readUninit.size
+    b.foreach {
+      case a: Assign => {
+        check(a)
+        init = init ++ a.assignees
+      }
+      case o => {
+        check(o)
+      }
+    }
+    i != readUninit.size
+  }
+
+  final def readUninitialised(b: Block): Boolean = {
+    val i = readUninit.size
+    readUninitialised(b.statements)
+    check(b.jump)
+    i != readUninit.size
+  }
+
+  final def getResult(): Option[String] = {
+    if (readUninit.size > 0) {
+      val msg = readUninit
+        .map { case (s, vars) =>
+          s"   ${vars.mkString(", ")} uninitialised in statement $s"
+        }
+        .mkString("\n")
+      Some(msg)
+    } else {
+      None
+    }
+  }
+
+  final def readUninitialised(p: Procedure): Boolean = {
+    init = init ++ p.formalInParam
+
+    ir.transforms.reversePostOrder(p)
+
+    val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder))
+    worklist.addAll(p.blocks)
+
+    while (worklist.nonEmpty) {
+      val b = worklist.dequeue()
+      readUninitialised(b)
+    }
+    getResult().map(e => Logger.error(p.name + "\n" + e)).isDefined
+  }
+
+}
+
+def readUninitialised(p: Program): Boolean = {
+  val r = p.procedures.map(ReadUninitialised().readUninitialised)
+  r.forall(x => !x)
+}
diff --git a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala b/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
index c33f4dd0b..c7e28996a 100644
--- a/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
+++ b/src/main/scala/ir/transforms/DynamicSingleAssignment.scala
@@ -298,7 +298,7 @@ class OnePassDSA(
     val worklist = mutable.PriorityQueue[Block]()(Ordering.by(b => b.rpoOrder))
     worklist.addAll(p.blocks)
     var seen = Set[Block]()
-    val count = mutable.Map[Variable, Int]().withDefaultValue(0)
+    val count = mutable.Map[Variable, Int]().withDefaultValue(p.ssaCount)
 
     while (worklist.nonEmpty) {
       while (worklist.nonEmpty) {
diff --git a/src/main/scala/ir/transforms/Inline.scala b/src/main/scala/ir/transforms/Inline.scala
index 3cb11c327..9421ec601 100644
--- a/src/main/scala/ir/transforms/Inline.scala
+++ b/src/main/scala/ir/transforms/Inline.scala
@@ -28,11 +28,7 @@ def renameBlock(s: String): String = {
 class VarRenamer(proc: Procedure) extends CILVisitor {
 
   def doRename(v: Variable): Variable = v match {
-    case l: LocalVar if l.name.endsWith("_in") => {
-      val name = l.name.stripSuffix("_in")
-      proc.getFreshSSAVar(name, l.getType)
-    }
-    case l: LocalVar if l.index != 0 =>
+    case l: LocalVar =>
       proc.getFreshSSAVar(l.varName, l.getType)
     case _ => v
   }
diff --git a/src/main/scala/ir/transforms/ProcedureParameters.scala b/src/main/scala/ir/transforms/ProcedureParameters.scala
index a4c7453f1..a0b582832 100644
--- a/src/main/scala/ir/transforms/ProcedureParameters.scala
+++ b/src/main/scala/ir/transforms/ProcedureParameters.scala
@@ -4,7 +4,7 @@ import ir.cilvisitor.*
 import ir.{CallGraph, *}
 import specification.Specification
 import translating.PrettyPrinter
-import util.{DebugDumpIRLogger, Logger}
+import util.DebugDumpIRLogger
 
 import java.io.File
 import scala.collection.{immutable, mutable}
@@ -119,12 +119,7 @@ def liftProcedureCallAbstraction(ctx: ir.IRContext): ir.IRContext = {
   val mainHasReturn = ctx.program.mainProcedure.returnBlock.isDefined
   val mainHasEntry = ctx.program.mainProcedure.entryBlock.isDefined
 
-  val liveVars = if (mainNonEmpty && mainHasEntry && mainHasReturn) {
-    analysis.InterLiveVarsAnalysis(ctx.program).analyze()
-  } else {
-    Logger.error(s"Empty live vars $mainNonEmpty $mainHasReturn $mainHasEntry")
-    Map.empty
-  }
+  val liveVars = analysis.interLiveVarsAnalysis(ctx.program)
   transforms.applyRPO(ctx.program)
 
   val liveLab = () =>
diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala
index c97f34bb9..8b28781e9 100644
--- a/src/main/scala/ir/transforms/Simp.scala
+++ b/src/main/scala/ir/transforms/Simp.scala
@@ -1249,21 +1249,35 @@ object OffsetProp {
     val lastUpdate = mutable.Map[Block, Int]()
     var stSequenceNo = 1
 
-    def findOff(v: Variable, c: BitVecLiteral): BitVecLiteral | Variable | BinaryExpr = find(v) match {
-      case lc: BitVecLiteral => ir.eval.BitVectorEval.smt_bvadd(lc, c)
-      case lv: Variable => BinaryExpr(BVADD, lv, c)
-      case BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) =>
-        BinaryExpr(BVADD, l, ir.eval.BitVectorEval.smt_bvadd(r, c))
-      case _ => throw Exception("Unexpected expression structure created by find() at some point")
-    }
+    def findOff(v: Variable, c: BitVecLiteral, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr =
+      find(v, fuel) match {
+        case lc: BitVecLiteral => ir.eval.BitVectorEval.smt_bvadd(lc, c)
+        case lv: Variable => BinaryExpr(BVADD, lv, c)
+        case BinaryExpr(BVADD, l: Variable, r: BitVecLiteral) =>
+          BinaryExpr(BVADD, l, ir.eval.BitVectorEval.smt_bvadd(r, c))
+        case _ => throw Exception("Unexpected expression structure created by find() at some point")
+      }
 
-    def find(v: Variable): BitVecLiteral | Variable | BinaryExpr = {
+    def find(v: Variable, fuel: Int = 1000): BitVecLiteral | Variable | BinaryExpr = {
+      if (fuel == 0) {
+        var chain = List(v)
+        for (i <- 0 to 10) {
+          chain = st.get(chain.head) match {
+            case Some((Some(v: Variable), _)) => v :: chain
+            case o =>
+              chain
+          }
+        }
+        throw Exception(
+          s"Ran out of fuel recursively resolving copyprop (at $v): probable cycle. Next lookups are: $chain"
+        )
+      }
       st.get(v) match {
         case None => v
         case Some((None, None)) => v
         case Some((None, Some(c))) => c
-        case Some((Some(v), None)) => find(v)
-        case Some((Some(v), Some(c))) => findOff(v, c)
+        case Some((Some(v), None)) => find(v, fuel - 1)
+        case Some((Some(v), Some(c))) => findOff(v, c, fuel - 1)
       }
     }
 
diff --git a/src/main/scala/ir/transforms/SimplifyPipeline.scala b/src/main/scala/ir/transforms/SimplifyPipeline.scala
index 13a2ee535..0488f8ff9 100644
--- a/src/main/scala/ir/transforms/SimplifyPipeline.scala
+++ b/src/main/scala/ir/transforms/SimplifyPipeline.scala
@@ -53,6 +53,7 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
 
   transforms.OnePassDSA().applyTransform(program)
 
+  assert(ir.invariant.readUninitialised(ctx.program))
   // fixme: this used to be a plain function but now we have to supply an analysis manager!
   transforms.inlinePLTLaunchpad(ctx, AnalysisManager(ctx.program))
 
@@ -110,6 +111,7 @@ def doSimplify(ctx: IRContext, config: Option[StaticAnalysisConfig]): Unit = {
     }
   }
   Logger.info("Copyprop Start")
+  assert(ir.invariant.readUninitialised(ctx.program))
   transforms.copyPropParamFixedPoint(program, ctx.globalOffsets)
 
   transforms.fixupGuards(program)
diff --git a/src/main/scala/translating/offlineLifter/InstructionBuilder.scala b/src/main/scala/translating/offlineLifter/InstructionBuilder.scala
index 540a61f6b..0393fa376 100644
--- a/src/main/scala/translating/offlineLifter/InstructionBuilder.scala
+++ b/src/main/scala/translating/offlineLifter/InstructionBuilder.scala
@@ -82,7 +82,12 @@ trait LifterIFace[L] extends LiftState[Expr, L, BitVecLiteral] {
     smt_bvlshr(arg0, BitVecLiteral(arg1.value, arg0.size))
 
   def f_decl_bool(arg0: String): Expr = LocalVar(b.fresh_local + "_bool", BoolType)
-  def f_decl_bv(arg0: String, arg1: BigInt): Expr = LocalVar(b.fresh_local + "_bv" + arg1, BitVecType(arg1.toInt))
+  def f_decl_bv(arg0: String, arg1: BigInt): Expr = {
+    val v = LocalVar(b.fresh_local + "_bv" + arg1, BitVecType(arg1.toInt))
+    // FIXME: shouldn't need always clear
+    b.push_stmt(LocalAssign(v, BitVecLiteral(0, arg1.toInt)))
+    v
+  }
 
   def f_AtomicEnd(): Expr = LocalVar("ATOMICEND", BoolType)
   def f_AtomicStart(): Expr = LocalVar("ATOMICSTART", BoolType)
diff --git a/src/main/scala/translating/offlineLifter/OfflineLifter.scala b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
index 0cb1208c1..85f4fea48 100644
--- a/src/main/scala/translating/offlineLifter/OfflineLifter.scala
+++ b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
@@ -115,6 +115,7 @@ class StmtListLifter extends LifterIFace[Int] {
 object Lifter {
 
   def liftBlockBytes(ops: Iterable[Int], initialSp: BigInt): Seq[Seq[Statement]] = {
+
     var sp = initialSp
     ops.toSeq.map { op =>
       val ins = if (op == 0xd503201f.toInt) {
@@ -123,10 +124,15 @@ object Lifter {
         Seq(Assert(FalseLiteral, Some(s"aarch64_system_exceptions_debug_breakpoint (0x$op)")))
       } else {
         try {
+          val checker = ir.invariant.ReadUninitialised()
           val lift = StmtListLifter()
           lift.builder.pcValue = sp
           f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(BigInt(op), 32), BitVecLiteral(sp, 64))
-          lift.extract.toSeq
+          val stmts = lift.extract.toSeq
+          checker.readUninitialised(stmts)
+          val r = checker.getResult()
+          if (r.isDefined) throw Exception(r.get + "\n" + stmts.mkString("\n"))
+          stmts
         } catch {
           case e => {
             val o = "%x".format(op)
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 509a445e8..c53866924 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -53,23 +53,26 @@ object RunUtils {
     Logger.info("[!] Loading Program")
     val q = conf
     var ctx = q.context.getOrElse(IRLoading.load(q.loading))
+    assert(invariant.readUninitialised(ctx.program))
     postLoad(ctx) // allows extracting information from the original loaded program
 
-    assert(ir.invariant.checkTypeCorrect(ctx.program))
+    assert(invariant.checkTypeCorrect(ctx.program))
     assert(invariant.singleCallBlockEnd(ctx.program))
     assert(invariant.cfgCorrect(ctx.program))
     assert(invariant.blocksUniqueToEachProcedure(ctx.program))
+    assert(invariant.readUninitialised(ctx.program))
 
     val analysisManager = AnalysisManager(ctx.program)
 
     if conf.simplify then doCleanupWithSimplify(ctx, analysisManager)
     else doCleanupWithoutSimplify(ctx, analysisManager)
 
-    assert(ir.invariant.programDiamondForm(ctx.program))
+    assert(invariant.programDiamondForm(ctx.program))
+    assert(invariant.readUninitialised(ctx.program))
 
     transforms.inlinePLTLaunchpad(ctx, analysisManager)
 
-    assert(ir.invariant.programDiamondForm(ctx.program))
+    assert(invariant.programDiamondForm(ctx.program))
 
     if q.loading.trimEarly then
       getStripUnreachableFunctionsTransform(q.loading.procedureTrimDepth)(ctx, analysisManager)
@@ -83,6 +86,7 @@ object RunUtils {
     if (q.loading.parameterForm && !q.simplify) {
       ir.transforms.clearParams(ctx.program)
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
+      assert(ir.invariant.readUninitialised(ctx.program))
       if (conf.assertCalleeSaved) {
         transforms.CalleePreservedParam.transform(ctx.program)
       }
@@ -111,11 +115,15 @@ object RunUtils {
 
       ir.transforms.clearParams(ctx.program)
 
+      assert(ir.invariant.readUninitialised(ctx.program))
       ir.transforms.liftIndirectCall(ctx.program)
       transforms.liftSVCompNonDetEarlyIR(ctx.program)
+      assert(ir.invariant.readUninitialised(ctx.program))
 
       DebugDumpIRLogger.writeToFile(File("il-after-indirectcalllift.il"), pp_prog(ctx.program))
       ctx = ir.transforms.liftProcedureCallAbstraction(ctx)
+      DebugDumpIRLogger.writeToFile(File("il-after-param.il"), pp_prog(ctx.program))
+      assert(ir.invariant.readUninitialised(ctx.program))
       DebugDumpIRLogger.writeToFile(File("il-after-proccalls.il"), pp_prog(ctx.program))
 
       if (conf.assertCalleeSaved) {
@@ -146,6 +154,7 @@ object RunUtils {
         val memTransferTimer = PerformanceTimer("Mem Transfer Timer", INFO)
         visit_prog(MemoryTransform(dsaResults.topDown, dsaResults.globals), ctx.program)
         memTransferTimer.checkPoint("Performed Memory Transform")
+        invariant.readUninitialised(ctx.program)
     }
 
     if q.summariseProcedures then
diff --git a/src/test/scala/MemoryTransformTests.scala b/src/test/scala/MemoryTransformTests.scala
index 63c08b2d8..3f40fd7d9 100644
--- a/src/test/scala/MemoryTransformTests.scala
+++ b/src/test/scala/MemoryTransformTests.scala
@@ -214,7 +214,7 @@ class MemoryTransformTests extends AnyFunSuite with CaptureOutput {
           MemoryStore(mem, xAddress, R31, LittleEndian, 64, Some("01")),
           MemoryLoad(R0, mem, xAddress, LittleEndian, 64, Some("02")),
           MemoryStore(mem, zAddress, R0, LittleEndian, 64, Some("03")),
-          goto("k")
+          goto("k", "dummy")
         ),
         block("h", goto("k")),
         block("k", ret),