Enriching logic formalisms with counting capabilities is an important task in view of the needs of many application areas, ranging from database theory to formal verification. Such enrichments have been designed both in the description logics area and in the area of Satisfiability Modulo Theories (SMT), where some of the most important recent achievements were decidability and complexity bounds for BAPA - the enrichment of Presburger arithmetic with the ability of talking about finite sets and their cardinalities. BAPA constraints can be used for program analysis and verification by expressing data structure invariants, simulations between program fragments or termination conditions. The analysis of BAPA constraints was successfully extended also to formalisms encompassing multisets as well as direct/inverse images along relations and functions.
A limitation of BAPA and its extensions lies in the fact that only uninterpreted symbols (for sets, relations, functions, etc.) are allowed. On the other hand, it is well-known that a different logical formalism, namely unary counting quantifiers, can be used in order to reason about the cardinality of definable (i.e. of interpreted) sets. Unary counting quantifiers can be added to Presburger arithmetic without compromising decidability; however they might be quite problematic if combined in an unlimited way with free function symbols. In this work, we investigate the extension of Presburger arithmetic including both counting quantifiers and uninterpreted function symbols, and we isolate fragments where we can achieve decidability and in some cases also relatively good complexity bounds. The key ingredient to isolate such fragments is the notion of flatness: roughly, in a flat formula, subterms of the kind a(t) (where a is a free function symbol) can occur only if t is a variable. By itself, this naif flatness requirement is useless (any formula can match it to the price of introducing extra quantified variables); in order to make it effective, further syntactic restrictions should be incorporated in it. This is what we are going to do in this work, where suitable notions of `flat' and `simple flat' formulae are introduced in the rich context of Presburger arithmetic enriched with free function symbols and with unary counting quantifiers (we use free function symbols to model arrays).
The fragments we design are all obviously more expressive than BAPA, but they do not come from pure logic motivations, on the contrary they are suggested by an emerging application area, namely the area of verification of fault-tolerant distributed systems. Such systems are modeled as partially synchronous systems, where a finite number of identical processes operate in lock-step (in each round they send messages, receive messages, and update their local state depending on the local state at the beginning of the round and the received messages). Messages can be lost, processes may omit to perform some tasks or also behave in a malicious way; for these reasons, the fact that some actions are enabled or not, and the correctness of the algorithms themselves, are subject to threshold conditions saying for instance that some qualified majority of processes are in a certain status or behave in a non-faulty way. Verifications tasks thus have to handle cardinality constraints of the kind studied in this work.
The framework and the results underlying our implementation are described in the paper [1] by Francesco Alberti and Silvio Ghilardi and Elena Pagani, Counting Constraints in Flat Array Fragments, available here as a preliminary research report.
We implemented a prototype ArCa-Sat producing out of simple E-flat formulae the proof obbligations (written in SMT-LIB2 format), exploiting the heuristics we devised. To experiment the feasibility of our approach for concrete verification problems, we also implemented a (beta) version of a tool called ArCa producing out of the specification of a parametric distributed system and of a safety-like problem, some E-flat simple formulae whose unsatisfiability formalizes invariant-checking (IC), bounded-model checking (BMC), and safety (SAF) problems. A script executing in sequence ArCa, ArCa-Sat and z3 can then solve such problems by reporting a `sat/unsat' answer.
In the next sections (Code section and Results section) there are respectively the files used with ArCa and some experimental statistics. In the Tools section, the tools used to translate the models into models for z3 are available.
We formalized the following algorithms:
- the byzantine broadcast primitive (BBP) [8] used to simulate authenticated broadcast in the presence of malicious failures of the processes
- the one-third algorithm (OT) [3] for consensus in the presence of benign transmission failures
- the send-receive broadcast primitive (SRBP) [7] to synchronize clocks in systems where processes may fail in sending and/or receiving messages
- the Uniform Voting (UV) algorithm [4] for consensus in the presence of benign transmission failures
- the U_{T,E,α} algorithm [2] for consensus in the presence of malicious transmission failures
- the MESI [5] and MOESI [6] algorithms for cache coherence.
Algorithm | Property | Problem | ArCa model |
---|---|---|---|
BBP | Correctness with N > 3f | BMC + IC | [Download] |
BBP | Unforgeability with N > 3f | SAF_n + SAF | [Download] |
BBP | Unforgeability with N >= 3f | SAF_n | [Download] |
BBP | Relay with N > 3f -- preliminary safety | SAF_n + SAF | [Download] |
BBP | Relay with N > 3f | BMC | [Download] |
BBP | Relay with N > 3f -- Liveness-like problem | BMC (sat) | [Download] |
OT | Agreement with threshold > 2N/3 | BMC + IC | [Download] |
OT | Agreement with threshold <= 2N/3 | BMC | [Download] |
OT | Irrevocability with threshold > 2N/3 -- preliminary safety | SAF_n + SAF | [Download] |
OT | Irrevocability with threshold > 2N/3 | SAF_n + SAF | [Download] |
OT | Irrevocability with threshold > 2N/3 -- Liveness-like problem | BMC (sat) | [Download] |
OT | Irrevocability with threshold <= 2N/3 | SAF_n | [Download] |
OT | Weak Validity with threshold > 2N/3 | BMC + IC | [Download] |
OT | Weak Validity with threshold <= 2N/3 | BMC | [Download] |
SRBP | Correctness with >= (f+1) inits | BMC + IC | [Download] |
SRBP | Correctness with <= f inits | BMC | [Download] |
SRBP | Unforgeability with >= (f+1) inits | SAF_n + SAF | [Download] |
SRBP | Relay with >= (f+1) inits -- preliminary safety | SAF_n + SAF | [Download] |
SRBP | Relay with >= (f+1) inits | BMC + IC | [Download] |
SRBP | Relay with >= (f+1) inits -- Liveness-like problem | BMC (sat) | [Download] |
UV | Integrity | BMC + IC | [Download] |
UV | Agreement with P_nosplit violated | BMC | [Download] |
UV | Irrevocability with P_nosplit violated | SAF_n | [Download] |
U_{T,E;α} | Integrity with α=0 and P_safe violated | BMC | [Download] |
U_{T,E;α} | Integrity with α=0 and P_safe | BMC | [Download] |
U_{T,E;α} | Integrity with α=1 and P_safe violated | BMC | [Download] |
U_{T,E;α} | Integrity with α=1 and P_safe | BMC | [Download] |
U_{T,E;α} | Agreement with α=0 and P_safe violated | BMC | [Download] |
U_{T,E;α} | Agreement with α=0 and P_safe | BMC | [Download] |
U_{T,E;α} | Agreement with α=1 and P_safe violated | BMC | [Download] |
U_{T,E;α} | Agreement with α=1 and P_safe | BMC | [Download] |
MESI | Cache coherence | IC | [Download] |
MOESI | Cache coherence | IC | [Download] |
We have developed translators that take as input our models, and produce in output a z3 file. From this page, interested readers may download our software. Specifically, for Linux systems the needed software is:
- ArCa: takes as input an algorithm model in SMT.LIB2 format, and produces either traces or invariants.
- arca.py: script in Pyton taking as input a proof obligation in ArCa format and producing as output appropsiate data structures. [script]
- arcasat: takes as input a file produced by arca.py and produces a file with an optimized equisatisfiable problem in SMT-LIB2 format (without cardinality constraints) that can be used as input to z3 [follow this link for downloading].
- Z3 theorem prover
- onemodel.sh: shell script that allows to orderly perform all the steps above for either BMC or SAF_n tests. It takes as input two arguments, namely, the maximum length of produces traces, and a model with cardinality constraints (e.g., one of the models supplied in the Code section) without the .smt2 suffix. For example: "./onemodel.sh 10 one_third_AG". It assumes the existence of a LOG subdirectory, where a *.log file is created reporting the outcomes of the algorithm check. [script]
- whole.sh: shell script that allows to orderly perform all the steps above for all the BMC / SAF_n models available in this page (Code section). It has no input argument. It assumes the existence of a LOG subdirectory, where a *.log file is created for each model, reporting the outcomes of the algorithm check. [script]
- oneInvariant.sh: shell script that allows to orderly perform all the steps above for either IC or SAF tests. It takes as input one argument, namely, the model with invariant property (e.g., one of the models supplied in the Code section) without the .smt2 suffix. For example: "./oneInvariant.sh one_third_AG". It assumes the existence of a LOG subdirectory, where a *.log file is created reporting the outcomes of the algorithm check. [script]
- wholeInvar.sh: shell script that allows to orderly perform all the steps above for all the IC / SAF models available in this page (Code section). It has no input argument. It assumes the existence of a LOG subdirectory, where a *.log file is created for each model, reporting the outcomes of the algorithm check. [script]
Building instructions (Linux 32/64 bits)
All the supplied scripts assume that all the models, the software of ArCa, ArCa-Sat and arca.py, and the scripts *.sh themselves, stay in the same directory; z3 must be installed and executable from command line (i.e., the PATH environment variable must be appropriately set to this purpose).
Warning: the shell scripts remove all previously created traces before running. The whole.sh and wholeInvar.sh scripts also remove the current content of the LOG subdirectory. The onemodel.sh and oneInvariant.sh scripts remove the previously produced log file for the model under verification.
ArCa-Sat: Instructions for executing arcasat as a stand-alone solver can be found here; an example of a problem specification is available here.
No warranty disclaim: this software is free and, as such, it comes with no warranty. By using this software, you are accepting the terms stated here. Because the program is licensed free of charge, there is no warranty for the program, to the extent permitted by applicable law. The entire risk as to the quality and performance of the program is with you. Should the program prove defective, you assume the cost of all necessary servicing, repair or correction directly or indirectly derived from its use.
Algorithm | Property | Problem | Result | Time (seconds)* | Max Depth | ||||||
---|---|---|---|---|---|---|---|---|---|---|---|
*Timings have been obtained on an Intel Core i7 running Linux Ubuntu 14.04 64 bits. | |||||||||||
BBP | Correctness with N > 3f | BMC | SAFE | 6.17 | 10 | ||||||
BBP | Correctness with N > 3f | IC | SAFE | 0.46 | - | ||||||
BBP | Unforgeability with N > 3f | SAF_n | SAFE | 0.25 | 10 | ||||||
BBP | Unforgeability with N > 3f | SAF | SAFE | 0.46 | - | ||||||
BBP | Unforgeability with N >= 3f | SAF_n | UNSAFE | 0.25 | 10 | ||||||
BBP | Relay with N > 3f (preliminary safety) | SAF_n | SAFE | 0.37 | 10 | ||||||
BBP | Relay with N > 3f (preliminary safety) | SAF | SAFE | 0.36 | - | ||||||
BBP | Relay with N > 3f | BMC | SAFE | 1.01 | 10 | ||||||
BBP | Relay with N > 3f (Liveness-like problem) | BMC | sat | 0.51 | 10 | ||||||
OT | Agreement with threshold > 2N/3 | BMC | SAFE | 278.95 | 10 | ||||||
OT | Agreement with threshold > 2N/3 | IC | SAFE | 14.27 | - | ||||||
OT | Agreement with threshold <= 2N/3 | BMC | UNSAFE | 17.75 | 10 | ||||||
OT | Irrevocability with threshold > 2N/3 (preliminary safety) | SAF_n | SAFE | 8.72 | 10 | ||||||
OT | Irrevocability with threshold > 2N/3 (preliminary safety) | SAF | SAFE | 1.39 | - | ||||||
OT | Irrevocability with threshold > 2N/3 /td> | SAF_n | SAFE | 0.32 | 10 | ||||||
OT | Irrevocability with threshold > 2N/3 /td> | SAF | SAFE | 1.32 | - | ||||||
OT | Irrevocability with threshold > 2N/3 (Liveness-like problem) | BMC | sat | 8.84 | 10 | ||||||
OT | Irrevocability with threshold <= 2N/3 | SAF_n | UNSAFE | 9.51 | 10 | ||||||
OT | Weak Validity with threshold > 2N/3 | BMC | SAFE | 0.45 | 10 | ||||||
OT | Weak Validity with threshold <= 2N/3 | IC | SAFE | 2.25 | - | ||||||
OT | Weak Validity with threshold <= 2N/3 | BMC | UNSAFE | 0.59 | 10 | ||||||
SRBP | Correctness with >= (f+1) inits | BMC | SAFE | 0.82 | 10 | ||||||
SRBP | Correctness with >= (f+1) inits | IC | SAFE | 0.32 | - | ||||||
SRBP | Correctness with <= f inits | BMC | UNSAFE | 2.21 | 10 | ||||||
SRBP | Unforgeability with >= (f+1) inits | SAF_n | SAFE | 0.85 | 10 | ||||||
SRBP | Unforgeability with >= (f+1) inits | SAF | SAFE | 1.46 | - | ||||||
SRBP | Relay with >= (f+1) inits (preliminary safety) | SAF_n | SAFE | 0.66 | 10 | ||||||
SRBP | Relay with >= (f+1) inits (preliminary safety) | SAF | SAFE | 1.42 | - | ||||||
SRBP | Relay with >= (f+1) inits | BMC | SAFE | 1.93 | 10 | ||||||
SRBP | Relay with >= (f+1) inits | IC | SAFE | 0.31 | - | ||||||
SRBP | Relay with >= (f+1) inits (Liveness-like problem) | BMC | sat | 1.19 | 10 | ||||||
UV | Integrity | BMC | SAFE | 1.02 | 10 | ||||||
UV | Integrity | IC | SAFE | 22.79 | - | ||||||
UV | Agreement with P_nosplit violated | BMC | UNSAFE | 4.18 | 10 | ||||||
UV | Irrevocability with P_nosplit violated | SAF_n | UNSAFE | 2.04 | 10 | ||||||
U_{T,E;α} | Integrity with α=0 and P_safe violated | BMC | UNSAFE | 0.83 | 10 | ||||||
U_{T,E;α} | Integrity with α=0 and P_safe | BMC | SAFE | 1.16 | 10 | ||||||
U_{T,E;α} | Integrity with α=1 and P_safe violated | BMC | UNSAFE | 4.93 | 10 | ||||||
U_{T,E;α} | Integrity with α=1 and P_safe | BMC | SAFE | 5.20 | 10 | ||||||
U_{T,E;α} | Agreement with α=0 and P_safe violated | BMC | UNSAFE | 7.78 | 10 | ||||||
U_{T,E;α} | Agreement with α=0 and P_safe | BMC | SAFE | 59.80 | 10 | ||||||
U_{T,E;α} | Agreement with α=1 and P_safe violated | BMC | UNSAFE | 31.94 | 10 | ||||||
U_{T,E;α} | Agreement with α=1 and P_safe | BMC | SAFE | 179.67 | 10 | ||||||
MESI | Cache coherence | IC | SAFE | 0.11 | - | ||||||
MOESI | Cache coherence | IC | SAFE | 0.08 | - |
- Francesco Alberti
- Silvio Ghilardi (reference author)
- Elena Pagani