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 ## PublicationsF. 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.
| |