=Paper= {{Paper |id=Vol-2987/paper11 |storemode=property |title=On the Parameterized Verification of Abstract Models of Contact Tracing Protocols |pdfUrl=https://ceur-ws.org/Vol-2987/paper11.pdf |volume=Vol-2987 |authors=Sylvain Conchon,Giorgio Delzanno,Arnaud Sangnier |dblpUrl=https://dblp.org/rec/conf/gandalf/ConchonDS21 }} ==On the Parameterized Verification of Abstract Models of Contact Tracing Protocols== https://ceur-ws.org/Vol-2987/paper11.pdf 
On the Parameterized Verification of Abstract
Models of Contact Tracing Protocols
Sylvain Conchon1 , Giorgio Delzanno2 and Arnaud Sangnier3
1
  LRI, Universitè Paris, France
2
  DIBRIS, University of Genova, Italy
3
  IRIF, Universitè Paris Denis Diderot


                                         Abstract
                                         We present an automata-based formal model of distributed systems specifically devised to formalise
                                         abstractions of Contact Tracing Protocols that combine Bluetooth and network communication. The
                                         model combines pure names, read/write operations on first-order and higher-order variables and syn-
                                         chronous communication primitives. The transition system models the interaction between devices in
                                         the same physical location and between a single device and a notification server. To automatically vali-
                                         date protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model
                                         checker, in which the monotonic abstraction applied during the predecessor computation is strengthen
                                         by introducing abstract predicates obtained via Counting Abstraction.




1. Introduction
Contact tracing protocols, e.g., smartphone apps, are aimed at investigating who could have
been contaminated by a positively diagnosed person and alert them, see e.g. [1]. After the
COVID-19 pandemic, several protocols have been proposed as an automated support for this
task su as PEPP-PT, DP3T, ROBERT4 and NTK5. In general the system architecture is based on
a smart app, a notification server as in Publish/Subscribe architectures, and a possibly trusted
server. In order to reduce the risk of a malicious use of user data (see e.g. the attacks described
in [2, 1]), the protocols are based on frequent rotations of identifiers emitted via bluetooth.
In centralized versions of the protocol ephemeral identifiers are downloaded from a trusted
server. In decentralized versions ephemeral identifiers are generated by user apps. The user
app installed on the user device (e.g. Immuni in Italy) broadcasts the currently valid ephemeral
identifier. The same user app also collects all identifiers emitted in the same bluetooth range
and stores them locally. When users are diagnosed to be infected, they release a report to the
server. One possible implementation consists in sending the report to a central log database.
Users can then consult the database to check if they crossed their way with infected users, i.e.,
they share some ephemeral identifier with one of them.
   Based on a preliminary study present at Overlay 2020 [3], in this paper we present an automata-
based formal model of distributed systems specifically devised to formalise abstractions of
Contact Tracing Protocols that combine Bluetooth and network communication. The model

OVERLAY 2021: 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis,
September 22, 2021, Padova, Italy
                                       Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)
combines pure names, read/write operations on first-order and higher-order variables and
synchronous communication primitives. The transition system models the interaction between
devices in the same physical location and between a single device and a notification server.
Violations of safety properties for this kind of protocols typically require universally quantified
conditions on global configurations (e.g. one user detects a contact while no user is positive).
   To automatically validate protocols in our formalism, we resort to an extension of the Cubicle
SMT-based infinite-state model checker. Cubicle is a model checker that can be applied to
verify safety properties of array-based systems, a syntactically restricted class of parameterized
transition systems with states represented as arrays indexed by an arbitrary number of processes
[4, 5]. Cubicle integrates the SMT solver Alt-Ergo [6]. Cubicle input language is a typed version
of Murπœ‘ [7]. A system is describe in Cubicle by: a set of type, variable, and array declarations;
a formula for the initial states; and a set of transitions. A system execution is defined by an
infinite loop that at each iteration non-deterministically chooses a transition instance whose
guard is true in the current state; and updates state variables according to the action of the fired
transition instance.
   To validate instances of our model, we will exhibit a general encoding in the Cubicle array-
based language and propose to refine the overapproximation of universally quantified precondi-
tions applied in the Cubicle backward procedure by introducing abstract predicates obtained
via Counting Abstraction.


2. Contact Tracing Systems
In this section we introduce a possible general formal model for contact tracing protocol. To
specify the protocol rules and behavior (computation), we will use a transition system defined
on configurations consisting of a set of states of individual users. User configurations contain a
local memory needed to store the list of emitted and received identifiers. System configurations
contain a global memory that can be used to gather and a set of user states that corresponds to
the current number of registered indivuals.
   We will use the following general definitions: ℐ is a denumerable set of pure names (identifiers)
containing the undefined label βŠ₯; 𝑀 is a finite set of message labels (π‘Ž, 𝑏, 𝑐, . . . ); 𝑉 is a finite set
of first order variables (identifiers) that are part of the local state of users (π‘₯, 𝑦, . . . ); 𝑆 is a finite
set of second order variables (set of identifiers) that are part of the local state of users (𝑠, 𝑑, . . . ).
We then define Act(𝑀, 𝑉, 𝑆) the set of actions defined as follows: π‘’π‘ž(π‘₯, 𝑦) and π‘›π‘œπ‘‘π‘’π‘ž(π‘₯, 𝑦),
where π‘₯, 𝑦 ∈ 𝑉 , 𝑖𝑛(π‘₯, π‘š) and π‘›π‘œπ‘‘π‘–π‘›(π‘₯, π‘š), where π‘₯ ∈ 𝑉 and π‘š ∈ 𝑀 (Conditions); π‘™π‘œπ‘π‘Žπ‘™,
𝑛𝑒𝑀(π‘₯), where π‘₯ ∈ 𝑉 , π‘π‘π‘Žπ‘ π‘‘(π‘š, π‘₯) and π‘Ÿπ‘’π‘(π‘š, π‘₯), where π‘š ∈ 𝑀, π‘₯ ∈ 𝑉 ; π‘Žπ‘‘π‘‘(π‘₯, 𝑠), where
π‘₯ ∈ 𝑉, 𝑠 ∈ 𝑆, π‘Ÿπ‘’π‘ π‘’π‘‘(𝑠), where 𝑠 ∈ 𝑆, π‘Ÿπ‘’π‘”(π‘š, 𝑠), where π‘š ∈ 𝑀, 𝑠 ∈ 𝑆 (Operations).
   A protocol is defined as a Data Automaton 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩, where π‘ž0 ∈ 𝑄 and
𝑅 βŠ† 𝑄 Γ— Act(𝑀, 𝑆, 𝑉 ) Γ— 𝑄. We assume here that π‘π‘π‘Žπ‘ π‘‘ and π‘Ÿπ‘’π‘” actions are always defined
on distinct labels in 𝑀 . Consider a protocol 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩. A process configuration
of 𝑃 is a triple 𝑝𝑐 = βŸ¨π‘ž, 𝛿, π›ΎβŸ© where: π‘ž ∈ 𝑄 is the current user state; 𝛿 : 𝑉 β†’ ℐ is the current
evaluation of first order variables; 𝛾 : 𝑆 β†’ 𝒫(ℐ) is the current evaluation of second order
variables. We denote by π’«π’ž the set of process configurations. A global configuration of 𝑃 is then
a pair (𝐾, Θ), where 𝐾 ∈ Nπ’«π’ž is a finite multiset of process configurations and Θ : 𝑀 ↦→ 𝒫(ℐ)
corresponds to a centralized memory. π’’π’ž denotes the set of global configurations. For 𝜎 ∈ π’’π’ž,
we will use 𝑖𝑑𝑠(𝜎) to denote the set of pure names occurring in 𝜎. The operational semantics is
then defined as the minimal relation β†’βŠ† 𝒒 Γ— 𝒒 that satisfies the following property definitions
in which will use ⊎ to denote multiset union:
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ if one of the following conditions is satis-
fied: βŸ¨π‘ž, π‘™π‘œπ‘π‘Žπ‘™, π‘ž β€² ⟩ ∈ 𝑅, βŸ¨π‘ž, π‘’π‘ž(π‘₯, 𝑦), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿(π‘₯) = 𝛿(𝑦) [for π‘›π‘œπ‘‘π‘’π‘ž(π‘₯, 𝑦),𝛿(π‘₯) ΜΈ= 𝛿(𝑦)],
βŸ¨π‘ž, 𝑖𝑛(π‘₯, π‘š), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿(π‘₯) ∈ Θ(π‘š) [for π‘›π‘œπ‘‘π‘–π‘›(π‘₯, 𝑦) 𝛿(π‘₯) ̸∈ Θ(π‘š)].
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿 β€² , π›ΎβŸ©} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, 𝑛𝑒𝑀(π‘₯), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿 β€² (π‘₯) = 𝑖𝑑 ̸∈
𝑖𝑑𝑠(𝜎), 𝑖𝑑 ΜΈ= βŠ₯, and 𝛿 β€² (𝑦) = 𝛿(𝑦) for π‘₯ ΜΈ= 𝑦.
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, 𝛾 β€² ⟩} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, π‘Žπ‘‘π‘‘(π‘₯, 𝑠), π‘ž β€² ⟩ ∈ 𝑅 and 𝛾 β€² (𝑠) =
𝛾(𝑠) βˆͺ {𝛿(π‘₯)} and 𝛾 β€² (𝑑) = 𝛾(𝑑) for 𝑑 ΜΈ= 𝑠.
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, 𝛾 β€² ⟩} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, π‘Ÿπ‘’π‘ π‘’π‘‘(𝑠), π‘ž β€² ⟩ ∈ 𝑅 and 𝛾 β€² (𝑠) = βˆ… and
𝛾 β€² (𝑑) = 𝛾(𝑑) for 𝑑 ΜΈ= 𝑠.
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©} ⊎ 𝐾, Ξ˜β€² ⟩ if βŸ¨π‘ž, π‘Ÿπ‘’π‘”(π‘š, 𝑠), π‘ž β€² ⟩ ∈ 𝑅 and Ξ˜β€² (π‘š) =
Θ(π‘š) βˆͺ 𝛾(𝑠) and Ξ˜β€² (𝑛) = Θ(𝑛) for 𝑛 ΜΈ= π‘š.
- 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©, βŸ¨π‘ž1 , 𝛿1 , 𝛾1 ⟩, . . . , βŸ¨π‘žπ‘˜ , π›Ώπ‘˜ , π›ΎβŸ©π‘˜ } ⊎ 𝐾, Θ⟩ β†’ ⟨𝐾 β€² , Θ⟩ where
𝐾 β€² = {βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©, βŸ¨π‘ž1β€² , 𝛿1β€² , 𝛾1 ⟩, . . . , βŸ¨π‘žπ‘˜β€² , π›Ώπ‘˜β€² , π›Ύπ‘˜ ⟩} ⊎ 𝐾 if π‘˜ β‰₯ 0 and βŸ¨π‘ž, π‘π‘π‘Žπ‘ π‘‘(π‘š, π‘₯), π‘ž β€² ⟩ ∈ 𝑅 and
for all 𝑖 ∈ [1, π‘˜], we have βŸ¨π‘žπ‘– , π‘Ÿπ‘’π‘(π‘š, π‘₯𝑖 ), π‘žπ‘–β€² ⟩ ∈ 𝑅 and 𝛿𝑖′ (π‘₯𝑖 ) = 𝛿(π‘₯) and 𝛿𝑖′ (𝑦) = 𝛿𝑖 (𝑦) for
𝑦 ΜΈ= π‘₯𝑖 .
   For the resulting model, we are interested in safety properties for parameterized version
of a protocol instance. More specifically, given a protocol definition 𝑃 and a given process
state π‘žπ‘’ ∈ 𝑄 that denotes an error state, we would like to verify that global configurations that
contain occurrences of π‘žπ‘’ are unreachable starting from any possibile initial configuration (i.e.
independently from the number of process instances). A similar property can be formulated
by adding an error flags to the server state instead of selecting a special error state in 𝑄. We
are also interested in properties expressed by violations in which global configurations contain
a process in state π‘žπ‘’ while all other processes are in states contained in These properties are
referred to as control state reachability and constrained control state reachabiliy, respectively.
Violations of this kind of properties can be defined using quantified assertions, such as there
exists a process 𝑖 in control state π‘žπ‘’ and, for constrained properties, universally quantified
conditions on the control states of other processes. In the rest of the paper we will illustrate
how to encode our formalism in Cubicle and how to verify control state reachability problems
using the corresponding symbolic exploration procedure provided by the tool.


3. Case Studies: Contact Tracing Protocols
We present below a formal specifications of the protocol scheme of Contact Tracing applications
abstracting away identifier creation, i.e., assuming that user app generate fresh identifiers, and
reasoning within the validity epoch of identifiers, i.e., those maintained in local memory. The
system is composed of a finite but arbitrary number of user apps and of a server modeled via
a centralized memory. Each user apps has local variables 𝑉 = {π‘₯, 𝑦, 𝑧} and 𝑆 = {𝑖𝑛, π‘œπ‘’π‘‘}.
Furthermore, 𝑀 = {𝑏, π‘š} where 𝑏 denotes beacon messages broadcasted by user apps, and
π‘š denotes report messages sent to the centralized memory. The user app starts their part of
protocol in state π‘ž0 and operate in three different modes.
   In emitter mode the app generates and emits fresh beacons: βŸ¨π‘ž0 , 𝑛𝑒𝑀(π‘₯), π‘ž1 ⟩, the user app
generates a fresh identifier and stores it in the local variable π‘₯; βŸ¨π‘ž1 , π‘Žπ‘‘π‘‘(π‘₯, π‘œπ‘’π‘‘), π‘ž2 ⟩, in π‘ž1 the
fresh identifier stored in π‘₯ is added to the local memory π‘œπ‘’π‘‘; βŸ¨π‘ž2 , π‘π‘π‘Žπ‘ π‘‘(𝑏, π‘₯), π‘ž2 ⟩, βŸ¨π‘ž2 , π‘™π‘œπ‘π‘Žπ‘™, π‘ž0 ⟩,
in π‘ž2 the user app either emits the message (𝑏, π‘₯) or returns to the initial state in order to apply
a rotation scheme for the beacon identifiers or perform other steps. In reception mode the app,
while in any state 𝑙0 ∈ 𝑄 βˆ– {π‘Ÿ1 , 𝑠2 }, receives a beacon, stores it in the local memory 𝑖𝑛, and
then returns to the current state: βŸ¨π‘™0 , π‘Ÿπ‘’π‘(𝑏, 𝑦), 𝑙1 ⟩ in state 𝑙0 the user is always ready to receive
beacons; βŸ¨π‘™1 , π‘Žπ‘‘π‘‘(𝑦, 𝑖𝑛), 𝑙0 ⟩, in state 𝑙1 the beacon is stored in the local memory 𝑖𝑛. In report
mode, enabled only in state π‘Ÿ0 = π‘ž0 , the app sends its local memory π‘œπ‘’π‘‘ to the server and
moves to the halt state π‘Ÿ1 : βŸ¨π‘ž0 , 𝑠𝑒𝑛𝑑(π‘š, π‘œπ‘’π‘‘), π‘Ÿ1 ⟩. In query mode, enabled only in state 𝑠0 = π‘ž0 ,
the user app selects a beacon 𝑧 from the local memory 𝑖𝑛, i.e., βŸ¨π‘ 0 , 𝑠𝑒𝑙(𝑖𝑛, 𝑧), 𝑠1 ⟩, sends it to
the server to check whether it has been reported by another app or not. In the former case it
moves to the halting state 𝑠2 , i.e, βŸ¨π‘ 1 , 𝑖𝑛(π‘š, π‘₯), 𝑠2 ⟩. In the latter case it returns to state 𝑠0 , i.e,
βŸ¨π‘ 1 , π‘›π‘œπ‘‘π‘–π‘›(π‘š, π‘₯), 𝑠0 ⟩.


4. From Data Automata to Cubicle
Let us now discuss how to model a protocol definition 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩ in Cubicle. A
global configuration is a pair (𝐾, Θ), where 𝐾 is a finite multiset of process configurations
and Θ corresponds to a centralized memory. The encoding if Θ is quite immediate since we
can represent the global memory as a finite set of unbounded arrays π΄π‘š1 , . . . , π΄π‘šπ‘› with cells
of Boolean type one for each π‘šπ‘– ∈ 𝑀 . The array π΄π‘š is such that π΄π‘š [π‘₯] = 𝑇 π‘Ÿπ‘’π‘’ if and only
if π‘₯ ∈ Θ(π‘š) for each pair π‘₯, π‘š. For the encoding of 𝐾 we can proceed in several different
ways. Remember that a process configuration is a triple 𝑝𝑐 = βŸ¨π‘ž, 𝛿, π›ΎβŸ©, in which π‘ž ∈ 𝑄 but is
the current user state, 𝛿 is the current evaluation of first order variables; and 𝛾 is the current
evaluation of second order variables. One possible encoding is defined as follows: To represent
control states, we introduce an unbounded array π‘ π‘‘π‘Žπ‘‘π‘’ that associates an enumerative type
associated to 𝑄 to represent the current state of each process, i.e., π‘ π‘‘π‘Žπ‘‘π‘’[𝑖] = π‘ž if process 𝑖 is in
state π‘ž. To represent the current state of a first order variable 𝑣 we can introduce an unbounded
array π‘£π‘Žπ‘™π‘£ such that π‘£π‘Žπ‘™π‘£ [𝑖] = 𝑑 if 𝛿(𝑣) = 𝑑 holds in 𝑝𝑐𝑖 (in process 𝑖). To represent the current
state of a second order variable 𝑠 we can introduce an unbounded bidimensional array π‘£π‘Žπ‘™π‘  such
that π‘£π‘Žπ‘™π‘  [𝑖, 𝑑] = 𝑇 π‘Ÿπ‘’π‘’ if and only if 𝑑 ∈ 𝛾(𝑠) holds in 𝑝𝑐𝑖 (in process 𝑖). Transition rules can
then be expressed via Cubicle transition rules. In particular, to model send operation involving
second order variables, we can use global operations on arrays, in which all cells of an arrays
are copied into another one (whole-place operations in Petri net languages).
   The Cubicle verification engine is based on symbolic backward exploration. Cubicle operates
over sets of existentially quantified formulas called cubes. Formulas containing universally
quantified formulas (generated during the computation of predecessors) are over-approximated
by existentially quantified formulas. In other words Cubicle applies monotone abstraction [8]
and over-approximates predecessors via upward-closed sets of configurations. Infinite sets of
unsafe states (bad configurations) are symbolically defined by using π‘’π‘›π‘ π‘Žπ‘“ 𝑒 constraints in
which all variables are implicitly existentially quantified. In our case studies we are interested
in checking the consistency between local and global information. More specifically, when user
π‘ˆ queries the server, she/he supposed to receive a notification only in presence of at least one
positive user who emitted a beacon that has been received by π‘ˆ . The server does not maintain
any association between identities and beacons collected in the log. Consistency of global and
local states combined with the privacy preservation property of the protocol can be tested by
adding an Error state and a special rule in which we only compare local states of different users.
Namely, the rule generates an error whenever there exist a user π‘ˆ in the Contact state without
any positive user in the global system. If this happens the protocol does not trace physical
contacts in correct way. The property is expressed by adding a global Error flag
Error: bool

together with the following rule:
transition bad(v)
requires { Contact[v] = True && forall_other u. (Pos[u] = False) }
{ Error := True; }

To validate the considered properties, we define the following assertion that specifies bad
configurations in the sense of control state reachability,
unsafe () { Error = True }

i.e., configurations of any size in which Error is True. Due to the presence of universally
quantified conditions both in the protocol rule and in the precondition of the error rule, there
is no termination guarantee on the execution of the verification task in Cubicle. Furthermore,
when terminating the tool may return spurious traces as in our case study. Indeed , Cubicle,
after visiting 41 cubes, detects a spurious trace of the form: start(#3, #2) -> in(#1, #2) -> end(#1,
#2) -> report(#3) -> query(#1, #2) -> bad(#1) -> unsafe.
   The imprecision here is due to the over-approximation introduced via monotone abstraction.
Preconditions with universally quantified guards are transformed into post-conditions, and
thus they are not propagated through different steps of predecessor computations. Since in the
correctness property of the protocol local states are put in relation via hidden data (not explicitly
mentioned in control states) stored in the server memory, it seems necessary to strengthen
the symbolic reasoning procedure with some form of propagation of universally quantified
conditions. One solutions comes from the combination of the existentially quantified formulas
used to represent sets of states in Cubicle (cubes) with other forms of constraints on the global
configuration e.g. constraints inspired to counting abstraction used in Petri nets. More in detail,
we enrich our assertions by adding counters that keep track of the number of users in a given
state. For our purposes, we will focus only on a counter associated to the Pos flag. We now
add a global variable Count whose initial state is defined as Count=0. The counter is updated
in the report rule (πΆπ‘œπ‘’π‘›π‘‘ β‰₯ 0 is added to the guard and πΆπ‘œπ‘’π‘›π‘‘ := πΆπ‘œπ‘’π‘›π‘‘ + 1 is added to the
body off the transition) and used as precondition in the error rule as specified below.
transition bad(v)
requires { Pos[v] = False             && Contact[v] = True && Count = 0 }
{ Error := True; }
The enriched assertional language combining array formulas (for expressing precise properties
of individual processes and of global variables) and Presburger constraints (for expressing global
constraints via the counting abstraction) is the key point in order to enforce termination and
prove correctness for the desired property. When executed on the refined model, Cubicle proves
the model SAFE after visiting 10 cubes and performing 138 fixpoint tests and 41 SMT solver
calls.
   Although not yet implemented, the above mentioned strategy could be incorporated into
the Cubicle algorithm for instance by associating counters to specific control states and by
generating counter manipulation operations in each transition rule via a preliminary static
analysis of the Cubicle specification as done in our example via human ingenuity.


References
[1] S. Vaudenay, Centralized or decentralized? the contact tracing dilemma, IACR Cryptol.
    ePrint Arch. 2020 (2020) 531. URL: https://eprint.iacr.org/2020/531.
[2] G. Avitabile, V. Botta, V. Iovino, I. Visconti, Towards defeating mass surveillance and sars-
    cov-2: The pronto-c2 fully decentralized automatic contact tracing system, IACR Cryptol.
    ePrint Arch. 2020 (2020) 493.
[3] P. A. Abdulla, M. F. Atig, G. Delzanno, M. Montali, A. Sangnier, On the formalization of
    decentralized contact tracing protocols, in: Proceedings of the 2nd Workshop on Artificial
    Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano
    Summer of Knowledge 2020 (BOSK 2020), September 25, 2020, volume 2785 of CEUR
    Workshop Proceedings, CEUR-WS.org, 2020, pp. 65–70.
[4] S. Conchon, A. Goel, S. Krstic, A. Mebsout, F. ZaΓ―di, Cubicle: A parallel smt-based model
    checker for parameterized systems - tool paper, in: Computer Aided Verification - 24th
    International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012,
    pp. 718–724.
[5] A. Mebsout, InfΓ©rence d’invariants pour le model checking de systΓ¨mes paramΓ©trΓ©s. (Invari-
    ants inference for model checking of parameterized systems), Ph.D. thesis, University of
    Paris-Sud, Orsay, France, 2014.
[6] https://alt-ergo.ocamlpro.com/, 2021.
[7] D. L. Dill, The murphi verification system, in: Computer Aided Verification, 8th International
    Conference, CAV ’96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings,
    volume 1102 of Lecture Notes in Computer Science, 1996, pp. 390–393.
[8] P. A. Abdulla, G. Delzanno, N. B. Henda, A. Rezine, Monotonic abstraction: on efficient
    verification of parameterized systems, Int. J. Found. Comput. Sci. 20 (2009) 779–801. doi:10.
    1142/S0129054109006887.