09.08.2019 Open Access
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
 Zeitschrift:
 Journal of Automated Reasoning
Publisher's Note
1 Introduction
2 Programs and Assertions
3 A Cyclic Proof System for Verifying CTL Properties

the formula \(\varphi _i\) is of the form \(AG \psi \) (\(EG \psi \)) or \(\Box AG \psi \) (\(\Diamond EG \psi \)); and

\(\varphi _{i+1} = \varphi _i\) whenever \(J_i\) is the conclusion of (Cons).
4 Fairness
5 Implementation and Evaluation

Examples discussed in the paper are named Exmp;

FinLock  a finite program that acquires a lock and, once obtained, proceeds to free from memory the elements of a list and reset the lock;

InfLock wraps the previous program inside an infinite loop;

NdInLock is an infinite loop that nondeterministically acquires a lock, then proceeds to perform a nondeterministic number of operations before releasing the lock;

InfList is an infinite loop that nondeterministically adds a new element to the list or advances the head of the list by one element on each iteration;

InsertList has a nondeterministic if statement that either adds a single elements to the head of the list or deletes all elements but one, and is followed by an infinite loop;

AppendList appends the second argument to the end of the first argument;

CyclicList is a nonterminating program that iterates through a nonempty cyclic list;

InfBinTree is an infinite loop that nondeterministically inserts nodes to a binary three or performs a random walk of the three;

The programs named with Branch define a somewhat arbitrary nesting of nondeterministic if and while statements, aimed at testing the capability of the tool in terms of lines of code and nesting of cycles;

Finally we also cover sample programs taken from the Windows Update system (Win Update), the backend infrastructure of the PostgreSQL database server (PostgreSQL) and an implementation of the acquirerelease algorithm taken from the aforementioned benchmarks (AcqRel).
Program  Precondition  Property  Fairness  Time (s) 

Exmp
 ls(x,nil)  AGEF emp  No  2.43 
Exmp
 ls(x,nil)  AGAF emp  Yes  4.29 
Exmp
 ls(x,nil)  AGAF (ls(x,nil))  No  0.26 
Exmp
 ls(x,nil)  AGEG (ls(x,nil))  No  0.44 
Exmp
 ls(x,nil)  AF emp  Yes  0.77 
Exmp
 ls(x,nil)  AFEG emp  Yes  0.86 
Exmp
 ls(x,nil)  AGAF emp  No  TO 
FinLock
 l \(\mapsto \)0 * ls(x,nil)  AF (l \(\mapsto \)1 * emp)  No  0.20 
FinLock
 l \(\mapsto \)0 * ls(x,nil)  AGAF(l \(\mapsto \)1 * emp)  No  0.62 
FinLock
 l \(\mapsto \)0 * ls(x,nil)  AGAF(l \(\mapsto \)1 * emp \(\wedge \)\(\Diamond \)l \(\mapsto \)0)  No  0.24 
FinLock
 l \(\mapsto \)0 * ls(x,nil)  AF (l \(\mapsto \)1 * ls(x,nil))  No  TO 
InfLock
 l \(\mapsto \)0 * ls(x,nil)  AGAF(l \(\mapsto \)1 * emp)  No  1.52 
InfLock
 l \(\mapsto \)0 * ls(x,nil)  AGAF(l \(\mapsto \)1 * emp \(\wedge \)\(\Diamond \)l \(\mapsto \)0))  No  3.26 
InfLock
 d = f : l \(\mapsto \)0 * ls(x,nil)  AG(d! = t \(\vee \) AF (l \(\mapsto \)1 * emp))  No  3.87 
NdInfLock
 l \(\mapsto \)0  AF(l \(\mapsto \)1)  Yes  0.15 
NdInfLock
 l \(\mapsto \)0  AGAF(l \(\mapsto \)1)  Yes  0.25 
NdInfLock
 l \(\mapsto \)0  AF(l \(\mapsto \)1)  No  TO 
InfList
 ls(x,nil)  AG ls(x,nil)  No  0.21 
InfList
 ls(x,nil)  AGEF x = nil  No  4.39 
InfList
 ls(x,nil)  AGAF x = nil  Yes  8.10 
InsertList
 ls(three,zero)  EF ls(five,zero)  No  0.14 
InsertList
 ls(three,zero)  AF ls(five,zero)  Yes  0.26 
InsertList
 ls(n,zero)  AGAF n! = zero  Yes  17.21 
AppendList
 ls(y,x) * ls(x,nil)  AF (ls(y,nil))  No  12.67 
CyclicList
 cls(x,x)  AG cls(x,x)  No  0.88 
CyclicList
 cls(x,x)  AGEG cls(x,x)  No  0.34 
InfBinTree
 x! = nil : bintree(x)  AGEG x! = nil  No  0.72 
InfBinTree
 x! = nil : bintree(x)  AGAF bintree(x)  No  TO 
AFAG Branch
 x\(\mapsto \)zero  AFAG x\(\mapsto \)one  No  1.80 
EGAG Branch
 x\(\mapsto \)zero  EGAG x\(\mapsto \)one  No  0.23 
EGAF Branch
 x\(\mapsto \)zero  EGAF x\(\mapsto \)one  No  15.48 
EG
\(\Rightarrow \)
EF Branch
 p = z \(\wedge \) q = z : ls(z,n)  EG(p! = one \(\vee \) EF q = one)  No  1.60 
EG
\(\Rightarrow \)
AF Branch
 p = z \(\wedge \) q = z : ls(z,n)  EG(p! = one \(\vee \) AF q = one)  Yes  5.33 
AG
\(\Rightarrow \)
EG Branch
 p = z \(\wedge \) q = one : ls(z,n)  AG(p! = one \(\vee \) EG q = one)  No  0.36 
AG
\(\Rightarrow \)
EF Branch
 p = z \(\wedge \) q = one :u ls(z,n)  AG(p! = one \(\vee \) EF q = one)  No  1.53 
Acqrel
 ls(zero,three)  AG(acq = 0 \(\vee \) AF rel! = 0)  No  1.25 
Acqrel
 ls(zero,three)  AG(acq = 0 \(\vee \) EF rel! = 0)  No  1.25 
Acqrel
 ls(zero,three)  EF acq! = 0 \(\wedge \) EF AG rel = 0  No  0.33 
Acqrel
 ls(zero,three)  AF AG rel = 0  Yes  0.42 
Acqrel
 ls(zero,three)  EF acq! = 0 \(\wedge \) EF EG rel = 0  No  0.25 
Acqrel
 ls(zero,three)  AF EG rel = 0  Yes  0.33 
PostgreSQL
 w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  AGAF w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  No  0.27 
PostgreSQL
 w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  AGEF w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  No  0.26 
PostgreSQL
 w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  EFEG w = false \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  No  0.44 
PostgreSQL
 w = true \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  EFAG w = false \(\wedge \) s = s\(^{\prime }\)\(\wedge \) f = f\(^{\prime }\)  No  0.77 
Win Update
 W! = nil : ls(W,nil)  AGAF W! = nil : ls(W,nil)  No  1.50 
Win Update
 W! = nil : ls(W,nil)  AGEF W! = nil : ls(W,nil)  No  1.00 
Win Update
 W! = nil : ls(W,nil)  EFEG W = nil : emp  No  3.60 
Win Update
 W! = nil : ls(W,nil)  AFEG W = nil : emp  Yes  3.70 
Win Update
 W! = nil : ls(W,nil)  EFAG W = nil : emp  No  3.15 
Win Update
 W! = nil : ls(W,nil)  AFAG W = nil : emp  Yes  4.16 