Co-termination (NuSMV)

Description of the Case Study

Co-termination asks whether two programs always agree on termination behaviour. Following Unno, Terauchi, and Koskinen [UTK21], we model two simple programs whose execution may diverge or terminate depending on their initial states. HyperQB evaluates paired runs of these programs: if one program terminates under a given initial condition, the other must terminate as well. Although co-termination is not a safety property, the tool’s optimistic bounded semantics can still confirm agreement (UNSAT) or expose a mismatch (SAT) in bounded traces.

The NuSMV model(s)

-- (adopted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)
-- 0	while (x>0){
-- 1		x = x - y
-- 2	}
MODULE main
	VAR
		x: 0..100;
		t: 0..1;
		location: 0..2;
		y: 0..5;

	ASSIGN
		init(location) := 1;
		init(x) := 100;
		init(t) := 0;
  		init(y) := 2;
		next(y) := y;

		next(location) :=
		case
			((location = 1) & (x > 0)): 1;
      		((location = 1) & (x <= 0)) : 2;
      		TRUE: location ;
    	esac;

		next(x) :=
			case
				((location = 1) & (x > 0)): x - y;
				((location = 1) & (x <= 0)) : x;
				TRUE : x;
			esac;

		next(t) :=
			case
				(location = 1): 0;
				(location = 2): 1;
				TRUE : t;
			esac;

    DEFINE
			halt := (location = 2) ;

The HyperLTL formula(s)

The property enforces that every pair of executions eventually reaches termination together. HyperQB checks the relational HyperLTL specification below; any counterexample contains two traces whose termination behaviours diverge.

\[\varphi_{\text{coterm}} = \forall \pi_A . \forall \pi_B . \left( \Diamond \mathrm{term}_{\pi_A} \leftrightarrow \Diamond \mathrm{term}_{\pi_B} \right)\]
Forall A . Forall B .
(F(halt[A])) = (F(halt[B]))

References