The paper “Evidence Extraction from Parameterised Boolean Equation Systems” by Wieger Wesselink and Tim Willemse was accepted for presentation at ARQNL (part of FLoC 2018, Oxford, UK). It provides the theoretical and practical foundations for constructing counterexamples in mCRL2 when verifying (first-order) modal mu-calculus properties.