The ArCA Tools

Last Releases: versions 1.0 -- Last Update: 2/12/2019

The ArCa tools handle verification tasks comprising both arrays, linear integer arithmetic and cardinality constraints (ArCA stands for "Arrays With Cardinalities"). More specifically:
  • ArCaSAT produces an SMT-LIB2 file specifying a problem equisatisfiable with the problem described in the input file, but not containing cardinality constraints (thus the proiblem in the output file can be effectively discharged by any SMT solver implementing a decision procedure for quantifier-free linear arithmetic). The tool (for Linux 64 bit architecture) can be downloaded here; experiments and bechmarks are described here.

  • ArCaSim produces a file is HORN SMT-LIB format, ready to be executed for instance by the muZ module of z3. Such a file is meant to determine the existence of an invariant certifying safety for the counter simulation of the problem given as input to ArCaSim. A "sat" answer by muZ shows that the invariant exists and an "unsafe" answer that it does not exist; an "unsafe" answer is inconclusive for the problem given as input to ArCaSim, because counter simulations are just abstractions of the original system. The tool (for Linux 64 bit architecture) can be downloaded here; experiments and bechmarks are described here.

The precise syntax accepted by the ArCa tools is described in the distribution and in the papers below. ArCaSAT (combined with an SMT solver) gives a full decision procedure for problems falling within the syntactic shape of its input language format, whereas ArCaSim supplies the best counter simulation available for its input problems.

Publications

  • F. Alberti, S. Ghilardi, E. Pagani Counting constraints in flat array fragments, Proceedings of IJCAR, Springer LNAI, vol. 9706, pp.65-81, 2016;

  • F. Alberti, S. Ghilardi, E. Pagani Cardinality Constraints for Arrays (decidability results and applications), Formal Methods in System Design, pp.545-574, 2017;

  • S. Ghilardi, E. Pagani Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems, Journal of Automated Reasoning (submitted);

  • S. Ghilardi, E. Pagani Counter Simulations via Higher Order Quantifier Elimination: a preliminary report, Proc. of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 17), EATCS;

  • S. Ghilardi, E. Pagani Second Order Quantifier Elimination: Towards Verification Applications, Proc. of the Workshop on Second Order Quantifier Elimination (SOQE 17), CEUR;

  • F. Alberti, S. Ghilardi, A. Orsini, E. Pagani Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies, Proc. of CILC 2016, CEUR, pp.102-117, 2016.