diff --git a/api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java b/api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java
index 0a5f467b9..6f6a59ec9 100644
--- a/api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java
+++ b/api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java
@@ -65,8 +65,9 @@ protected Collection<Pair<I, S>> initialNodes() {
 
         for (Entry<I, UniversalDeterministicAutomaton<S, I, ?, ?, ?>> e : subModels.entrySet()) {
             final S init = e.getValue().getInitialState();
-            assert init != null;
-            initialNodes.add(Pair.of(e.getKey(), init));
+            if (init != null) {
+                initialNodes.add(Pair.of(e.getKey(), init));
+            }
         }
 
         return initialNodes;
diff --git a/build-config/src/main/resources/automatalib-spotbugs-exclusions.xml b/build-config/src/main/resources/automatalib-spotbugs-exclusions.xml
index 910dc1480..c29d1371c 100644
--- a/build-config/src/main/resources/automatalib-spotbugs-exclusions.xml
+++ b/build-config/src/main/resources/automatalib-spotbugs-exclusions.xml
@@ -35,14 +35,21 @@ limitations under the License.
     </Match>
     <Match>
         <Bug pattern="NP_NULL_ON_SOME_PATH_FROM_RETURN_VALUE"/>
-        <And>
-            <!-- Fine according to JavaDoc -->
-            <Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
-            <Or>
-                <Method name="popBack" returns="java.lang.Object"/>
-                <Method name="popFront" returns="java.lang.Object"/>
-            </Or>
-        </And>
+        <Or>
+            <And>
+                <!-- Fine according to data-flow -->
+                <Class name="net.automatalib.util.automaton.ads.LeeYannakakis"/>
+                <Method name="computeValidities"/>
+            </And>
+            <And>
+                <!-- Fine according to JavaDoc -->
+                <Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
+                <Or>
+                    <Method name="popBack" returns="java.lang.Object"/>
+                    <Method name="popFront" returns="java.lang.Object"/>
+                </Or>
+            </And>
+        </Or>
     </Match>
     <Match>
         <!-- Passing references is mostly fine for performance reasons. Since we do not deal with security-related code,
diff --git a/build-parent/pom.xml b/build-parent/pom.xml
index f58ef0d09..d2bde3434 100644
--- a/build-parent/pom.xml
+++ b/build-parent/pom.xml
@@ -240,7 +240,6 @@ limitations under the License.
                                     <goal>compile</goal>
                                 </goals>
                                 <configuration>
-                                    <failOnWarning>true</failOnWarning>
                                     <fork>true</fork>
                                     <outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
                                     <annotationProcessorPaths combine.children="append">
@@ -273,7 +272,6 @@ limitations under the License.
                                         </arg>
                                         <arg>-AskipUses=^java.(awt.*|util.(Arrays|Map|ArrayDeque)|io.StreamTokenizer)|^javax.swing.*</arg>
                                         <arg>-AsuppressWarnings=uninitialized</arg>
-                                        <arg>-AassumeAssertionsAreEnabled</arg>
                                         <arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
                                     </compilerArgs>
                                 </configuration>
@@ -285,7 +283,6 @@ limitations under the License.
                                     <goal>testCompile</goal>
                                 </goals>
                                 <configuration>
-                                    <failOnWarning>true</failOnWarning>
                                     <fork>true</fork>
                                     <outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
                                     <annotationProcessorPaths combine.children="append">
@@ -311,7 +308,6 @@ limitations under the License.
                                         <arg>-AonlyDefs=^net\.automatalib</arg>
                                         <arg>-AskipUses=.*</arg>
                                         <arg>-AsuppressWarnings=uninitialized</arg>
-                                        <arg>-AassumeAssertionsAreEnabled</arg>
                                         <arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
                                     </compilerArgs>
                                 </configuration>
diff --git a/commons/smartcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java b/commons/smartcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java
index 1e2a2f80d..0688d15f1 100644
--- a/commons/smartcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java
+++ b/commons/smartcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java
@@ -36,6 +36,7 @@ public class ReflexiveMapView<T> extends AbstractMap<T, T> {
 
     private final Set<@KeyFor("this") T> domain;
 
+    @SuppressWarnings("type") // the provided items become keys for this map view
     public ReflexiveMapView(Set<T> domain) {
         this.domain = Collections.unmodifiableSet(domain);
     }
@@ -68,6 +69,7 @@ public boolean containsKey(@Nullable Object key) {
     }
 
     @Override
+    @SuppressWarnings("return") // it is okay that values are also keys for this map
     public Set<T> values() {
         return this.domain;
     }
diff --git a/core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java b/core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java
index 83022ab4f..3e413bc18 100644
--- a/core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java
+++ b/core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java
@@ -32,6 +32,7 @@
 import net.automatalib.symbol.time.TimedInput;
 import net.automatalib.symbol.time.TimedOutput;
 import net.automatalib.symbol.time.TimeoutSymbol;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -132,8 +133,9 @@ public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> so
                 }
             }
 
-            assert lastOutput != null;
-            return new MealyTransition<>(currentConfig, new TimedOutput<>(lastOutput));
+            @SuppressWarnings("nullness") // since remainingTime must be > 0, the while loop iterates at least once
+            final @NonNull O output = lastOutput;
+            return new MealyTransition<>(currentConfig, new TimedOutput<>(output));
         } else {
             throw new IllegalArgumentException("Unknown input symbol type");
         }
diff --git a/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java b/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java
index c38269c91..80c2f3983 100644
--- a/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java
+++ b/core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java
@@ -50,7 +50,7 @@ public StackSPA(ProceduralInputAlphabet<I> alphabet,
     }
 
     @Override
-    public StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
+    public @Nullable StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
         if (state.isTerm()) {
             return null;
         } else if (alphabet.isInternalSymbol(input)) {
diff --git a/core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java b/core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java
index 71f97e2ff..c2dc6cda9 100644
--- a/core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java
+++ b/core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java
@@ -15,7 +15,6 @@
  */
 package net.automatalib.automaton.procedural.impl;
 
-import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -54,21 +53,25 @@ StackState<S, I, P> push(P newProcedure, S newState) {
         return new StackState<>(this, newProcedure, newState);
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     StackState<S, I, P> pop() {
         assert !isStatic() : "This method should never be called on static states";
         return prev;
     }
 
+    @SuppressWarnings("type") // since this method is package-private, we are happy to only assert nullability
     StackState<S, I, P> updateState(S state) {
         assert !isStatic() : "This method should never be called on static states";
         return new StackState<>(prev, procedure, state);
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     P getProcedure() {
         assert !isStatic() : "This method should never be called on static states";
         return procedure;
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     S getCurrentState() {
         assert !isStatic() : "This method should never be called on static states";
         return procedureState;
@@ -92,9 +95,6 @@ boolean isTerm() {
         return this == TERM;
     }
 
-    // contract is satisfied by definition of constructors
-    @SuppressWarnings("contracts.conditional.postcondition")
-    @EnsuresNonNullIf(expression = {"this.prev", "this.procedure", "this.procedureState"}, result = false)
     private boolean isStatic() {
         return isInit() || isTerm();
     }
diff --git a/examples/src/main/java/net/automatalib/example/graph/DFSExample.java b/examples/src/main/java/net/automatalib/example/graph/DFSExample.java
index 868ea6374..9eef503ba 100644
--- a/examples/src/main/java/net/automatalib/example/graph/DFSExample.java
+++ b/examples/src/main/java/net/automatalib/example/graph/DFSExample.java
@@ -30,6 +30,7 @@
 import net.automatalib.visualization.Visualization;
 import net.automatalib.visualization.VisualizationHelper;
 import net.automatalib.visualization.VisualizationHelper.EdgeStyles;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * A small example of a {@link GraphTraversal graph traversal} that uses a custom {@link GraphTraversalVisitor} to
@@ -168,16 +169,16 @@ static class DFSResultDOTHelper<N, E> implements VisualizationHelper<N, E> {
         @Override
         public boolean getNodeProperties(N node, Map<String, String> properties) {
             String lbl = properties.get(NodeAttrs.LABEL);
-            DFSData record = records.get(node);
-            assert record != null;
+            @SuppressWarnings("nullness") // we have traversed all nodes before
+            @NonNull DFSData record = records.get(node);
             properties.put(NodeAttrs.LABEL, lbl + " [#" + record.dfsNumber + "]");
             return true;
         }
 
         @Override
         public boolean getEdgeProperties(N src, E edge, N tgt, Map<String, String> properties) {
-            EdgeType et = edgeTypes.get(edge);
-            assert et != null;
+            @SuppressWarnings("nullness") // we have traversed all nodes before
+            @NonNull EdgeType et = edgeTypes.get(edge);
             properties.put(EdgeAttrs.STYLE, et.getStyle());
             properties.remove(EdgeAttrs.LABEL);
             return true;
diff --git a/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java b/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java
index da37a8017..e7a961611 100644
--- a/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java
+++ b/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java
@@ -23,6 +23,7 @@
 import net.automatalib.incremental.ConflictException;
 import net.automatalib.incremental.dfa.Acceptance;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -74,7 +75,6 @@ public Acceptance lookup(Word<? extends I> word) {
      */
     @Override
     public void insert(Word<? extends I> word, boolean accepting) {
-        int len = word.length();
         Acceptance acc = Acceptance.fromBoolean(accepting);
 
         State curr = init;
@@ -99,6 +99,7 @@ public void insert(Word<? extends I> word, boolean accepting) {
             curr = succ;
         }
 
+        int len = word.length();
         int prefixLen = path.size();
 
         State last = curr;
@@ -139,8 +140,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
                 // confluence always requires cloning, to separate this path from other paths
                 last = hiddenClone(last);
                 if (conf == null) {
-                    Transition peek = path.peek();
-                    assert peek != null;
+                    // the root node is never confluent so in this context, the path always contains at least one node
+                    @SuppressWarnings("nullness")
+                    @NonNull Transition peek = path.peek();
                     State prev = peek.state;
                     if (prev == init) {
                         updateInitSignature(peek.transIdx, last);
diff --git a/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java b/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java
index ed35839fc..d306d5e40 100644
--- a/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java
+++ b/incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java
@@ -23,6 +23,7 @@
 import net.automatalib.incremental.ConflictException;
 import net.automatalib.incremental.dfa.Acceptance;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * The prefix-closed version of {@link IncrementalDFADAGBuilder}. Contrary to the regular lookup semantics, where an
@@ -145,8 +146,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
                 }
                 last = hiddenClone(last);
                 if (conf == null) {
-                    Transition peek = path.peek();
-                    assert peek != null;
+                    // the root node is never confluent so in this context, the path always contains at least one node
+                    @SuppressWarnings("nullness")
+                    @NonNull Transition peek = path.peek();
                     State prev = peek.state;
                     if (prev == init) {
                         updateInitSignature(peek.transIdx, last);
diff --git a/incremental/src/main/java/net/automatalib/incremental/mealy/dag/IncrementalMealyDAGBuilder.java b/incremental/src/main/java/net/automatalib/incremental/mealy/dag/IncrementalMealyDAGBuilder.java
index 8b2b25256..449e145bb 100644
--- a/incremental/src/main/java/net/automatalib/incremental/mealy/dag/IncrementalMealyDAGBuilder.java
+++ b/incremental/src/main/java/net/automatalib/incremental/mealy/dag/IncrementalMealyDAGBuilder.java
@@ -42,6 +42,7 @@
 import net.automatalib.visualization.VisualizationHelper;
 import net.automatalib.word.Word;
 import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -181,8 +182,9 @@ public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
             }
             last = hiddenClone(last);
             if (conf == null) {
-                Transition<O> peek = path.peek();
-                assert peek != null;
+                // the root node is never confluent so in this context, the path always contains at least one node
+                @SuppressWarnings("nullness")
+                @NonNull Transition<O> peek = path.peek();
                 State<O> prev = peek.state;
                 if (prev == init) {
                     updateInitSignature(peek.transIdx, last);
diff --git a/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java b/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java
index 3fc5be915..e8f2076e3 100644
--- a/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java
+++ b/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java
@@ -44,6 +44,7 @@
 import net.automatalib.word.Word;
 import net.automatalib.word.WordBuilder;
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -201,8 +202,9 @@ public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
             }
             last = hiddenClone(last);
             if (conf == null) {
-                Transition<O> peek = path.peek();
-                assert peek != null;
+                // the root node is never confluent so in this context, the path always contains at least one node
+                @SuppressWarnings("nullness")
+                @NonNull Transition<O> peek = path.peek();
                 State<O> prev = peek.state;
                 if (prev == init) {
                     updateInitSignature(peek.transIdx, last);
@@ -342,7 +344,8 @@ private State<O> updateSignature(State<O> state, int idx, State<O> succ) {
      *         the new successor state
      */
     private void updateInitSignature(int idx, State<O> succ) {
-        assert init != null;
+        @SuppressWarnings("nullness") // this internal method is only called after the root node has been initialized
+        @NonNull State<O> init = this.init;
         StateSignature<O> sig = init.getSignature();
         State<O> oldSucc = sig.successors.get(idx);
         if (oldSucc == succ) {
@@ -366,7 +369,8 @@ private void updateInitSignature(int idx, State<O> succ) {
      *         the output symbol
      */
     private void updateInitSignature(int idx, State<O> succ, O out) {
-        assert init != null;
+        @SuppressWarnings("nullness") // this internal method is only called after the root node has been initialized
+        @NonNull State<O> init = this.init;
         StateSignature<O> sig = init.getSignature();
         State<O> oldSucc = sig.successors.get(idx);
         if (oldSucc == succ && Objects.equals(out, succ.getOutput())) {
diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/AbstractDDSolver.java b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/AbstractDDSolver.java
index 2bf6d8e8d..1246b4223 100644
--- a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/AbstractDDSolver.java
+++ b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/AbstractDDSolver.java
@@ -418,8 +418,8 @@ private <E> T getEdgeTransformer(WorkUnit<?, E> unit, E edge) {
         final ProceduralModalProcessGraph<?, L, E, AP, ?> pmpg = unit.pmpg;
         final L label = pmpg.getEdgeLabel(edge);
         if (isProcessEdge(pmpg, edge)) {
-            final WorkUnit<?, ?> edgeUnit = workUnits.get(label);
-            assert edgeUnit != null;
+            @SuppressWarnings("nullness") // we constructed work units based on labels
+            final @NonNull WorkUnit<?, ?> edgeUnit = workUnits.get(label);
             edgeTransformer = getInitialEdgeTransformer(edgeUnit);
         } else {
             if (isMustEdge(pmpg, edge)) {
diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTree.java b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTree.java
index d98c8c929..c7c9c615d 100644
--- a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTree.java
+++ b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTree.java
@@ -38,9 +38,9 @@ public class WitnessTree<L, AP> extends CompactUniversalGraph<WitnessTreeState<?
 
     private @MonotonicNonNull Word<L> result;
 
+    @SuppressWarnings("nullness") // the witness tree is returned only after the path has been computed
     public Word<L> getWitness() {
-        assert result != null;
-        return result;
+        return this.result;
     }
 
     void computePath(int finishingNode) {
@@ -50,7 +50,6 @@ void computePath(int finishingNode) {
 
         while (currentNode >= 0) {
             final WitnessTreeState<?, L, ?, AP> prop = super.getNodeProperty(currentNode);
-            assert prop != null;
 
             final L label = prop.edgeLabel;
             prop.isPartOfResult = true;
diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeExtractor.java b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeExtractor.java
index d51239450..25ca22e45 100644
--- a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeExtractor.java
+++ b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeExtractor.java
@@ -81,8 +81,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
                                                   FormulaNode<L, AP> formula) {
 
         final Deque<WitnessTreeState<?, L, ?, AP>> queue = new ArrayDeque<>();
-        final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> mainUnit = units.get(cfmps.getMainProcess());
-        assert mainUnit != null;
+        @SuppressWarnings("nullness") // we constructed work units based on all labels
+        final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> mainUnit = units.get(cfmps.getMainProcess());
         final WitnessTreeState<?, L, ?, AP> init = getInitialTreeState(mainUnit, formula);
 
         queue.add(init);
@@ -167,7 +167,6 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
     private <N> List<WitnessTreeState<?, L, ?, AP>> exploreDia(DiamondNode<L, AP> formula,
                                                                WitnessTreeState<N, L, ?, AP> queueElement) {
         if (Objects.equals(queueElement.state, queueElement.pmpg.getFinalNode())) {
-            assert queueElement.stack != null;
             return findDiaMoveEndNodeReturn(queueElement);
         } else if (formula.getAction() == null) {
             return findDiaMoveWithEmpty(queueElement, formula);
@@ -199,8 +198,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
                     result.add(toAdd);
                 }
             } else {
-                final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> unit = units.get(label);
-                assert unit != null;
+                @SuppressWarnings("nullness") // we constructed work units based on all labels
+                final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> unit = units.get(label);
                 final WitnessTreeState<?, L, ?, AP> toAdd =
                         buildProcessNode(queueElement, unit, label, target, formula);
 
@@ -215,8 +214,9 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
 
     private <N, E> List<WitnessTreeState<?, L, ?, AP>> findDiaMoveEndNodeReturn(WitnessTreeState<N, L, E, AP> queueElement) {
 
-        assert queueElement.stack != null;
-        final WitnessTreeState<?, L, ?, AP> toAdd = buildReturnNode(queueElement, queueElement.stack);
+        @SuppressWarnings("nullness") // only the root node has no stack and it will never be mapped to a final/end node
+        @NonNull WitnessTreeState<?, L, ?, AP> prev = queueElement.stack;
+        final WitnessTreeState<?, L, ?, AP> toAdd = buildReturnNode(queueElement, prev);
 
         return Collections.singletonList(toAdd);
     }
@@ -245,8 +245,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
                     result.add(toAdd);
                 }
             } else {
-                final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> unit = units.get(label);
-                assert unit != null;
+                @SuppressWarnings("nullness") // we constructed work units based on all labels
+                final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> unit = units.get(label);
                 final WitnessTreeState<?, L, ?, AP> toAdd =
                         buildProcessNode(queueElement, unit, label, target, formula);
 
diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeState.java b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeState.java
index 193780486..35486c44b 100644
--- a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeState.java
+++ b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeState.java
@@ -50,7 +50,8 @@ public class WitnessTreeState<N, L, E, AP> {
     public boolean isPartOfResult;
 
     WitnessTreeState(AbstractDDSolver<?, L, AP>.WorkUnit<N, E> unit,
-                     @Nullable WitnessTreeState<?, L, ?, AP> stack, N state,
+                     @Nullable WitnessTreeState<?, L, ?, AP> stack,
+                     N state,
                      FormulaNode<L, AP> subformula,
                      BitSet context,
                      String displayLabel,
diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformer.java b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformer.java
index 3c44eb5d6..6f59dfe59 100644
--- a/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformer.java
+++ b/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformer.java
@@ -186,38 +186,39 @@ public ADDTransformer<L, AP> createUpdate(Set<AP> atomicPropositions,
                                               EquationalBlock<L, AP> currentBlock) {
         XDD<BooleanVector> updatedADD;
         final DiamondOperation<AP> diamondOp = new DiamondOperation<>(atomicPropositions, currentBlock);
+
         if (compositions.isEmpty()) {
-            assert this.add != null : "The identity function should never be updated";
+            if (this.add == null) {
+                throw new IllegalArgumentException("The identity function should never be updated");
+            }
             updatedADD = this.add.monadicApply(new DiamondOperationDeadlock<>(atomicPropositions, currentBlock));
         } else {
             final XDD<BooleanVector> firstAdd = compositions.get(0).add;
-            assert firstAdd != null : "The identity function should never be updated";
-            updatedADD = preserveUpdatedTransformer(firstAdd, currentBlock);
+
+            if (this.add == null || firstAdd == null) {
+                throw new IllegalArgumentException("The identity function should never be updated");
+            }
+
+            updatedADD = this.add.apply((booleanVectorBeforeUpdate, booleanVectorRight) -> {
+                boolean[] result = booleanVectorBeforeUpdate.data().clone();
+                for (FormulaNode<?, AP> node : currentBlock.getNodes()) {
+                    result[node.getVarNumber()] = booleanVectorRight.data()[node.getVarNumber()];
+                }
+                return new BooleanVector(result);
+            }, firstAdd);
 
             for (ADDTransformer<L, AP> composition : compositions) {
-                assert composition.add != null : "The identity function should never be updated";
-                updatedADD = updatedADD.apply(diamondOp, composition.add);
+                XDD<BooleanVector> nextAdd = composition.add;
+                if (nextAdd == null) {
+                    throw new IllegalArgumentException("The identity function should never be updated");
+                }
+                updatedADD = updatedADD.apply(diamondOp, nextAdd);
             }
         }
 
         return new ADDTransformer<>(xddManager, updatedADD);
     }
 
-    private XDD<BooleanVector> preserveUpdatedTransformer(XDD<BooleanVector> rightDD,
-                                                          EquationalBlock<L, AP> currentBlock) {
-        assert this.add != null : "The identity function should never be updated";
-        /* We create a new XDD where the information of this.add (the add before the update) is 'injected'
-        into rightDD, the first composition DD, such that the bits corresponding to subformulas outside the current
-        block are preserved */
-        return this.add.apply((booleanVectorBeforeUpdate, booleanVectorRight) -> {
-            boolean[] result = booleanVectorBeforeUpdate.data().clone();
-            for (FormulaNode<?, AP> node : currentBlock.getNodes()) {
-                result[node.getVarNumber()] = booleanVectorRight.data()[node.getVarNumber()];
-            }
-            return new BooleanVector(result);
-        }, rightDD);
-    }
-
     /**
      * Returns the ADD which represents the property transformer.
      *
diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/ExternalSystemDeserializer.java b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/ExternalSystemDeserializer.java
index 1cb2a7dca..fd2a1ed82 100644
--- a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/ExternalSystemDeserializer.java
+++ b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/solver/ExternalSystemDeserializer.java
@@ -35,6 +35,7 @@
 import net.automatalib.ts.modal.transition.ModalEdgeProperty.ModalType;
 import net.automatalib.ts.modal.transition.MutableProceduralModalEdgeProperty;
 import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty.ProceduralType;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 import org.w3c.dom.Node;
@@ -91,8 +92,8 @@ private static Element getRoot(InputStream is) throws ParserConfigurationExcepti
     }
 
     private static Element getFirstElementByTagName(Element elem, String tagName) {
-        final Node node = elem.getElementsByTagName(tagName).item(0);
-        assert node != null;
+        @SuppressWarnings("nullness")
+        final @NonNull Node node = elem.getElementsByTagName(tagName).item(0);
         return (Element) node;
     }
 
diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformerTest.java b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformerTest.java
index 550d08d38..45c2038f2 100644
--- a/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformerTest.java
+++ b/modelchecking/m3c/src/test/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformerTest.java
@@ -15,6 +15,7 @@
  */
 package net.automatalib.modelchecker.m3c.transformer;
 
+import java.util.Arrays;
 import java.util.BitSet;
 import java.util.Collections;
 import java.util.HashSet;
@@ -262,4 +263,27 @@ void testUpdateException() throws FormatException {
         transformer.createUpdate(atomicPropositions, Collections.singletonList(transformer), block);
     }
 
+    @Test
+    void testUpdateIdentityException() throws FormatException {
+        final String formulaWithNegatedAP = "mu X.(<b><b>!'a' || <>X)";
+        DependencyGraph<String, String> dependencyGraph = new DependencyGraph<>(M3CParser.parse(formulaWithNegatedAP));
+        ADDTransformer<String, String> transformer = new ADDTransformer<>(xddManager, dependencyGraph);
+        ADDTransformer<String, String> id = new ADDTransformer<>(xddManager);
+        Set<String> atomicPropositions = new HashSet<>();
+        atomicPropositions.add("a");
+
+        Assert.assertThrows(IllegalArgumentException.class,
+                            () -> id.createUpdate(atomicPropositions,
+                                                  Collections.emptyList(),
+                                                  dependencyGraph.getBlock(0)));
+        Assert.assertThrows(IllegalArgumentException.class,
+                            () -> transformer.createUpdate(atomicPropositions,
+                                                           Collections.singletonList(id),
+                                                           dependencyGraph.getBlock(0)));
+        Assert.assertThrows(IllegalArgumentException.class,
+                            () -> transformer.createUpdate(atomicPropositions,
+                                                           Arrays.asList(transformer, id),
+                                                           dependencyGraph.getBlock(0)));
+    }
+
 }
diff --git a/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java
index 7979a4491..ca5d2d3e9 100644
--- a/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java
+++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java
@@ -43,6 +43,7 @@
 import net.automatalib.visualization.VisualizationHelper.EdgeAttrs;
 import net.automatalib.visualization.VisualizationHelper.MMLTEdgeAttrs;
 import net.automatalib.visualization.VisualizationHelper.MMLTNodeAttrs;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * Parses a DOT file that defines an {@link MMLT}.
@@ -192,10 +193,11 @@ private Mapping<S, String> parseNodesAndEdges(InternalDOTParser parser, MutableM
                     if (!m.matches()) {
                         continue;
                     }
-                    String g1 = m.group(1);
-                    String g2 = m.group(2);
 
-                    assert g1 != null && g2 != null;
+                    @SuppressWarnings("nullness") // if the pattern matches, we have two groups
+                    @NonNull String g1 = m.group(1);
+                    @SuppressWarnings("nullness")
+                    @NonNull String g2 = m.group(2);
 
                     String timerName = g1.trim();
                     int value = Integer.parseInt(g2);
diff --git a/serialization/fsm/src/main/java/net/automatalib/serialization/fsm/parser/FSM2MealyParserAlternating.java b/serialization/fsm/src/main/java/net/automatalib/serialization/fsm/parser/FSM2MealyParserAlternating.java
index 1bbe0783d..6e27d3901 100644
--- a/serialization/fsm/src/main/java/net/automatalib/serialization/fsm/parser/FSM2MealyParserAlternating.java
+++ b/serialization/fsm/src/main/java/net/automatalib/serialization/fsm/parser/FSM2MealyParserAlternating.java
@@ -38,6 +38,7 @@
 import net.automatalib.serialization.ModelDeserializer;
 import net.automatalib.word.Word;
 import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -186,8 +187,8 @@ private void makeTransitions(Integer currentState,
         // check if we need to compute an undefined output.
         if (inputTrans != null && targets.isEmpty()) {
             if (wb != null) {
-                assert output != null;
-
+                @SuppressWarnings("nullness") // wb is null iff output is null
+                @NonNull Output<I, Word<O>> output = this.output;
                 final O o = output.computeOutput(wb).lastSymbol();
 
                 // create an actual Mealy machine transition
diff --git a/util/src/main/java/net/automatalib/util/automaton/ads/ADSUtil.java b/util/src/main/java/net/automatalib/util/automaton/ads/ADSUtil.java
index 38dc2c55e..b69bdf24a 100644
--- a/util/src/main/java/net/automatalib/util/automaton/ads/ADSUtil.java
+++ b/util/src/main/java/net/automatalib/util/automaton/ads/ADSUtil.java
@@ -86,7 +86,11 @@ public static <S, I, T, O, N extends RecursiveADSNode<S, I, O, N>> Pair<N, N> bu
             final N nextNode = creator.apply(tempADS, nextInput);
 
             final T trans = automaton.getTransition(tempState, tempInput);
-            assert trans != null;
+
+            if (trans == null) {
+                break;
+            }
+
             final O oldOutput = automaton.getTransitionOutput(trans);
 
             tempADS.getChildren().put(oldOutput, nextNode);
diff --git a/util/src/main/java/net/automatalib/util/automaton/ads/BacktrackingSearch.java b/util/src/main/java/net/automatalib/util/automaton/ads/BacktrackingSearch.java
index d1cdf8635..3d137999f 100644
--- a/util/src/main/java/net/automatalib/util/automaton/ads/BacktrackingSearch.java
+++ b/util/src/main/java/net/automatalib/util/automaton/ads/BacktrackingSearch.java
@@ -420,8 +420,9 @@ private static <S, I, T, O> ADSNode<S, I, O> constructADS(MealyMachine<S, I, T,
 
         for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {
             final S current = entry.getKey();
-            final T trans = automaton.getTransition(current, i);
-            assert trans != null;
+            @SuppressWarnings("nullness") // we only construct ADSs from valid search states
+            final @NonNull T trans = automaton.getTransition(current, i);
+
             final S nextState = automaton.getSuccessor(trans);
             final O nextOutput = automaton.getTransitionOutput(trans);
 
diff --git a/util/src/main/java/net/automatalib/util/automaton/ads/LeeYannakakis.java b/util/src/main/java/net/automatalib/util/automaton/ads/LeeYannakakis.java
index b39a66a50..13f0ca084 100644
--- a/util/src/main/java/net/automatalib/util/automaton/ads/LeeYannakakis.java
+++ b/util/src/main/java/net/automatalib/util/automaton/ads/LeeYannakakis.java
@@ -38,6 +38,7 @@
 import net.automatalib.util.graph.ShortestPaths;
 import net.automatalib.util.graph.traversal.GraphTraversal;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * Algorithm of Lee and Yannakakis for computing adaptive distinguishing sequences (of length at most n^2) in O(n^2)
@@ -400,11 +401,11 @@ private static <S, I, O> Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> c
                 final Integer successor = iter.next();
                 final Validity successorValidity = partitionToClassificationMap.get(successor);
                 if (successorValidity == Validity.A_VALID || successorValidity == Validity.B_VALID) {
-                    final Path<Integer, CompactEdge<I>> path = ShortestPaths.shortestPath(implicationGraph,
-                                                                                          pendingPartition,
-                                                                                          implicationGraph.size(),
-                                                                                          successor);
-                    assert path != null; // by construction should never be null
+                    @SuppressWarnings("nullness") // by construction should never be null
+                    final @NonNull Path<Integer, CompactEdge<I>> path = ShortestPaths.shortestPath(implicationGraph,
+                                                                                                   pendingPartition,
+                                                                                                   implicationGraph.size(),
+                                                                                                   successor);
                     final Word<I> word = path.stream().map(CompactEdge::getProperty).collect(Word.collector());
 
                     result.get(Validity.C_VALID).add(Pair.of(word, pendingC));
diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/Covers.java b/util/src/main/java/net/automatalib/util/automaton/cover/Covers.java
index 8e8bf757b..9703688df 100644
--- a/util/src/main/java/net/automatalib/util/automaton/cover/Covers.java
+++ b/util/src/main/java/net/automatalib/util/automaton/cover/Covers.java
@@ -29,6 +29,7 @@
 import net.automatalib.common.util.mapping.Mapping;
 import net.automatalib.common.util.mapping.MutableMapping;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 public final class Covers {
@@ -231,8 +232,8 @@ public static <S, I> void cover(DeterministicAutomaton<S, I, ?> automaton,
         S curr;
 
         while ((curr = bfsQueue.poll()) != null) {
-            Word<I> as = reach.get(curr);
-            assert as != null;
+            @SuppressWarnings("nullness") // in a breadth-first traversal the predecessors are always defined
+            @NonNull Word<I> as = reach.get(curr);
 
             for (I in : inputs) {
                 S succ = automaton.getSuccessor(curr, in);
diff --git a/util/src/main/java/net/automatalib/util/automaton/equivalence/CharacterizingSets.java b/util/src/main/java/net/automatalib/util/automaton/equivalence/CharacterizingSets.java
index 1c846028a..6f214d6de 100644
--- a/util/src/main/java/net/automatalib/util/automaton/equivalence/CharacterizingSets.java
+++ b/util/src/main/java/net/automatalib/util/automaton/equivalence/CharacterizingSets.java
@@ -124,7 +124,7 @@ public static <S, I> void findCharacterizingSet(UniversalDeterministicAutomaton<
             }
 
             if (suffix == null) {
-                return;
+                throw new IllegalArgumentException("equivalent states detected, model must be minimal");
             }
 
             result.add(suffix);
diff --git a/util/src/main/java/net/automatalib/util/automaton/equivalence/DeterministicEquivalenceTest.java b/util/src/main/java/net/automatalib/util/automaton/equivalence/DeterministicEquivalenceTest.java
index 3e84f8ad1..aee309c15 100644
--- a/util/src/main/java/net/automatalib/util/automaton/equivalence/DeterministicEquivalenceTest.java
+++ b/util/src/main/java/net/automatalib/util/automaton/equivalence/DeterministicEquivalenceTest.java
@@ -26,6 +26,7 @@
 import net.automatalib.automaton.concept.StateIDs;
 import net.automatalib.word.Word;
 import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 @SuppressWarnings("PMD.TestClassWithoutTestCases") // not a traditional test class
@@ -87,8 +88,9 @@ private DeterministicEquivalenceTest() {
             S refState = currPair.ref;
             S2 otherState = currPair.other;
 
-            lastPred = reg.getPred(refStateIds.getStateId(refState), otherStateIds.getStateId(otherState));
-            assert lastPred != null;
+            @SuppressWarnings("nullness") // in a breadth-first traversal the predecessors are always defined
+            @NonNull Pred<I> pred = reg.getPred(refStateIds.getStateId(refState), otherStateIds.getStateId(otherState));
+            lastPred = pred;
 
             for (I in : inputs) {
                 lastSym = in;
diff --git a/util/src/main/java/net/automatalib/util/automaton/transducer/SubsequentialTransducers.java b/util/src/main/java/net/automatalib/util/automaton/transducer/SubsequentialTransducers.java
index c27f59ee3..f31b7a679 100644
--- a/util/src/main/java/net/automatalib/util/automaton/transducer/SubsequentialTransducers.java
+++ b/util/src/main/java/net/automatalib/util/automaton/transducer/SubsequentialTransducers.java
@@ -155,14 +155,15 @@ public static <S, I, T, O, A extends MutableSubsequentialTransducer<S, I, T, O>>
                 for (Pair<S, I> trans : incomingTransitions.get(s)) {
                     final S src = trans.getFirst();
                     final T t = out.getTransition(src, trans.getSecond());
-                    assert t != null;
 
-                    final Word<O> oldTransitionProperty = out.getTransitionProperty(t);
-                    final Word<O> newTransitionProperty = oldTransitionProperty.concat(lcp);
+                    if (t != null) {
+                        final Word<O> oldTransitionProperty = out.getTransitionProperty(t);
+                        final Word<O> newTransitionProperty = oldTransitionProperty.concat(lcp);
 
-                    out.setTransitionProperty(t, newTransitionProperty);
-                    if (!queue.contains(src)) {
-                        queue.add(src);
+                        out.setTransitionProperty(t, newTransitionProperty);
+                        if (!queue.contains(src)) {
+                            queue.add(src);
+                        }
                     }
                 }
             }
diff --git a/util/src/main/java/net/automatalib/util/automaton/vpa/OneSEVPAs.java b/util/src/main/java/net/automatalib/util/automaton/vpa/OneSEVPAs.java
index a3f8c219a..2268d2495 100644
--- a/util/src/main/java/net/automatalib/util/automaton/vpa/OneSEVPAs.java
+++ b/util/src/main/java/net/automatalib/util/automaton/vpa/OneSEVPAs.java
@@ -473,7 +473,7 @@ public static <L, I> List<L> findReachableLocations(OneSEVPA<L, I> sevpa, VPAlph
      * @param alphabet
      *         the input symbols to consider
      *
-     * @return a separating word for the two locations, or {@code null} if no such word could be found.
+     * @return a separating word for the two locations, or {@code null} if no such word could be found
      */
     public static <L, I> @Nullable Pair<Word<I>, Word<I>> findSeparatingWord(OneSEVPA<L, I> sevpa,
                                                                              L init1,
@@ -504,7 +504,9 @@ public static <L, I> List<L> findReachableLocations(OneSEVPA<L, I> sevpa, VPAlph
                 final L succ1 = sevpa.getInternalSuccessor(l1, i);
                 final L succ2 = sevpa.getInternalSuccessor(l2, i);
 
-                assert succ1 != null && succ2 != null;
+                if (succ1 == null || succ2 == null) {
+                    throw new IllegalArgumentException("Only total models are supported");
+                }
 
                 if (sevpa.isAcceptingLocation(succ1) != sevpa.isAcceptingLocation(succ2)) {
                     lastPair = pair;
@@ -534,7 +536,9 @@ public static <L, I> List<L> findReachableLocations(OneSEVPA<L, I> sevpa, VPAlph
                         final L rSucc1 = sevpa.getReturnSuccessor(l1, r, sym);
                         final L rSucc2 = sevpa.getReturnSuccessor(l2, r, sym);
 
-                        assert rSucc1 != null && rSucc2 != null;
+                        if (rSucc1 == null || rSucc2 == null) {
+                            throw new IllegalArgumentException("Only total models are supported");
+                        }
 
                         final Pair<Word<I>, Word<I>> pair =
                                 Pair.of(Word.fromWords(as.get(sevpa.getLocationId(l)), cWord), rWord);
@@ -562,7 +566,9 @@ public static <L, I> List<L> findReachableLocations(OneSEVPA<L, I> sevpa, VPAlph
                         final L rSucc1 = sevpa.getReturnSuccessor(l, r, sym1);
                         final L rSucc2 = sevpa.getReturnSuccessor(l, r, sym2);
 
-                        assert rSucc1 != null && rSucc2 != null;
+                        if (rSucc1 == null || rSucc2 == null) {
+                            throw new IllegalArgumentException("Only total models are supported");
+                        }
 
                         final Pair<Word<I>, Word<I>> pair =
                                 Pair.of(Word.epsilon(), Word.fromWords(cWord, as.get(sevpa.getLocationId(l)), rWord));
@@ -608,7 +614,7 @@ public static <L, I> List<L> findReachableLocations(OneSEVPA<L, I> sevpa, VPAlph
 
     /**
      * Computes a characterizing set for the given SEVPA. Note that the characterizing words consist of a prefix and a
-     * suffix since locations are typically distinguished in regard to the syntactical
+     * suffix since locations are typically distinguished in regard to the syntactical congruence.
      *
      * @param <L>
      *         location type
@@ -656,7 +662,10 @@ public static <L, I> Collection<Pair<Word<I>, Word<I>>> findCharacterizingSet(On
             final L l2 = blockIter.next();
 
             final Pair<Word<I>, Word<I>> sepWord = findSeparatingWord(sevpa, l1, l2, alphabet);
-            assert sepWord != null;
+
+            if (sepWord == null) {
+                throw new IllegalArgumentException("Equivalent states detected, model must be minimal");
+            }
 
             result.add(sepWord);
 
diff --git a/util/src/main/java/net/automatalib/util/graph/sssp/DijkstraSSSP.java b/util/src/main/java/net/automatalib/util/graph/sssp/DijkstraSSSP.java
index b857f6fb8..246e7b64d 100644
--- a/util/src/main/java/net/automatalib/util/graph/sssp/DijkstraSSSP.java
+++ b/util/src/main/java/net/automatalib/util/graph/sssp/DijkstraSSSP.java
@@ -26,6 +26,7 @@
 import net.automatalib.graph.Graph;
 import net.automatalib.graph.concept.EdgeWeights;
 import net.automatalib.util.graph.Graphs;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.PolyNull;
 
@@ -160,8 +161,9 @@ public float getShortestPathDistance(N target) {
         E edge;
         while ((edge = rec.reach) != null) {
             result.add(edge);
-            rec = rec.parent;
-            assert rec != null;
+            @SuppressWarnings("nullness") // reach is null iff parent is null
+            @NonNull Record<N, E> tmp = rec.parent;
+            rec = tmp;
         }
 
         Collections.reverse(result);
diff --git a/util/src/main/java/net/automatalib/util/partitionrefinement/Hopcroft.java b/util/src/main/java/net/automatalib/util/partitionrefinement/Hopcroft.java
index d3c973095..9dd048d00 100644
--- a/util/src/main/java/net/automatalib/util/partitionrefinement/Hopcroft.java
+++ b/util/src/main/java/net/automatalib/util/partitionrefinement/Hopcroft.java
@@ -21,6 +21,7 @@
 import java.util.Spliterator;
 import java.util.Spliterators;
 
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -222,8 +223,9 @@ private void addToWorklist(Block b) {
         if (worklistHead == null) {
             worklistHead = b;
         } else {
-            assert worklistTail != null;
-            worklistTail.nextInWorklist = b;
+            @SuppressWarnings("nullness") // worklistTail is null iff worklistHead is null
+            @NonNull Block tail = worklistTail;
+            tail.nextInWorklist = b;
         }
         worklistTail = b;
     }
diff --git a/util/src/main/java/net/automatalib/util/ts/modal/ModalConjunction.java b/util/src/main/java/net/automatalib/util/ts/modal/ModalConjunction.java
index d4c3b17be..ff966d973 100644
--- a/util/src/main/java/net/automatalib/util/ts/modal/ModalConjunction.java
+++ b/util/src/main/java/net/automatalib/util/ts/modal/ModalConjunction.java
@@ -34,6 +34,7 @@
 import net.automatalib.util.ts.traversal.TSTraversal;
 import net.automatalib.util.ts.traversal.TSTraversalAction;
 import net.automatalib.util.ts.traversal.TSTraversalVisitor;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 final class ModalConjunction<A extends MutableModalTransitionSystem<S, I, T, ?>, S, S0, S1, I, T, T0, T1, TP0 extends ModalEdgeProperty, TP1 extends ModalEdgeProperty>
         implements WorksetMappingAlgorithm<Pair<S0, S1>, S, A> {
@@ -84,9 +85,9 @@ public Collection<Pair<S0, S1>> initialize(Map<Pair<S0, S1>, S> mapping) {
 
     @Override
     public Collection<Pair<S0, S1>> update(Map<Pair<S0, S1>, S> mapping, Pair<S0, S1> currentStatePair) {
-        S mappedState = mapping.get(currentStatePair);
-        assert mappedState != null;
-
+        // workset is explored in breadth-first style and we update the fringe states as necessary
+        @SuppressWarnings("nullness")
+        @NonNull S mappedState = mapping.get(currentStatePair);
         ArrayList<Pair<S0, S1>> discovered = new ArrayList<>();
 
         for (I sym : mts0.getInputAlphabet()) {
diff --git a/util/src/main/java/net/automatalib/util/ts/traversal/SimpleDFRecord.java b/util/src/main/java/net/automatalib/util/ts/traversal/SimpleDFRecord.java
index 355ac9f6a..0365da7bc 100644
--- a/util/src/main/java/net/automatalib/util/ts/traversal/SimpleDFRecord.java
+++ b/util/src/main/java/net/automatalib/util/ts/traversal/SimpleDFRecord.java
@@ -23,6 +23,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.RequiresNonNull;
 import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 
 class SimpleDFRecord<S, I, T> {
 
@@ -50,6 +51,7 @@ public boolean start(TransitionSystem<S, ? super I, T> ts) {
         return true;
     }
 
+    @SideEffectFree // while fields are updated, they never change regarding nullability
     private void findNext(TransitionSystem<S, ? super I, T> ts) {
         if (transitionIterator != null && transitionIterator.hasNext()) {
             return;
@@ -72,7 +74,6 @@ public boolean hasNextTransition(TransitionSystem<S, ? super I, T> ts) {
         if (!transitionIterator.hasNext()) {
             findNext(ts);
         }
-        assert transitionIterator != null;
         return transitionIterator.hasNext();
     }
 
@@ -94,8 +95,8 @@ public I input() {
         return input;
     }
 
-    @Pure
     @RequiresNonNull("transitionIterator")
+    @SideEffectFree // while state changes, never does nullability
     public T transition() {
         return transitionIterator.next();
     }
diff --git a/visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTImageComponent.java b/visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTImageComponent.java
index 011edfa18..b1f904316 100644
--- a/visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTImageComponent.java
+++ b/visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTImageComponent.java
@@ -36,6 +36,7 @@
 import javax.swing.event.MouseInputAdapter;
 
 import net.automatalib.common.util.IOUtil;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -195,9 +196,8 @@ public void mouseReleased(MouseEvent e) {
         @Override
         public void mouseDragged(MouseEvent e) {
             final Point dragEventPoint = e.getPoint();
-            final JViewport viewport = (JViewport) cmp.getParent();
-
-            assert viewport != null;
+            @SuppressWarnings("nullness") // the DOTImageComponent is always embedded in a parent frame
+            final @NonNull JViewport viewport = (JViewport) cmp.getParent();
 
             final Point viewPos = viewport.getViewPosition();