Co-termination¶
Description of the Case Study¶
This property asks whether two different programs agree on termination, which can be formalized using a \(∀∀\) HyperLTL formula:
\[\forall \pi_A.\forall \pi_B.\ \Diamond(\mathrm{term}_{\pi_A}) \leftrightarrow \Diamond(\mathrm{term}_{\pi_B}).\]
We consider two simple programs from [UTK21]. In this case, depends on their initial conditions, the programs might either diverge or agree on termination. Co-termination is a non-safety formula; however, our bounded semantics (in particular, opt), is able to give a meaningful verdict even though this is not a finitely-refutable property.
Benchmarks¶
The Model(s)
-- CO-TERMINATION
-- (adopted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)
MODULE main
-- 0 while (x>0){
-- 1 x = x - y
-- 2 }
VAR
x:-5..100;
t: 0..1;
location: 0..2;
y: 0..5;
-- FROZENVAR
-- 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 ;
-- CO-TERMINATION
-- (adopted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)
MODULE main
-- 0 while (x>0){
-- 1 x = x - (2 x y)
-- 2 }
VAR
x:-10..100;
t: 0..1;
location: 0..2;
y: 0..5;
-- FROZENVAR
-- 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 - (2 * 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 ;
Formula
forall A. forall B.
(F(halt[A]))<->(F(halt[B]))