ARMC

• ARMC is a tool for the verification of reachability and termination properties.
• Download ARMC for Linux/x86: armc (version 12-Apr-2007), and example input files
  • svd-with-error-labels.armc automatically translated from singular value decomposition program from the "numerical recipes" book, augmented with array bound checks. Please be patient, ARMC needs 2 min. on this example. If your tool can do it faster, please let me know. Please send me a mail to get the original svd-with-error-labels.c file.
  • filter-simple.armc
  • evader-pursuer.armc
  • vagrant-robot.armc
  (In case of memory problems try the statically linked armc-static.)
• When proving reachability, try -nopredpc option to switch off predicate partitioning.
• Use -noverbose to switch off printing of the abstract fixpoint.
• Use -dotcfg to print the control-flow graph of the input program in dot-format.
• Use -straight to print compressed transition relation where "straight-line" code between cut-points is composed to single transition.
• CIL-based translator from a subset of C to ARMC input linux x86 native binary c2armc.asm.exe and linux x86 bytecode binary c2armc.byte.exe Error location in C source should be marked by the label ERROR:. Multiple error labels are possible. The translator also creates the control-flow graph in dot format.
• This webpage is under active development. Feel free to communicate your feedback, links, requests for features, case studies, info about ARMC usage.
• Next item to come: example of using ARMC for proving termination.

Applications of ARMC

• Ales Smrcka, Tomas Vojnar. Verifying Parameterised Hardware Designs via Counter Automata. HVC 2007.
• Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook: Arithmetic Strengthening for Shape Analysis. SAS 2007: 419-436.
• Johannes Faber and Roland Meyer. Model checking data-dependent real-time properties of the european train control system. In Formal Methods in Computer Aided Design, pages 76-77. IEEE Computer Society, 2006.
• Roland Meyer, Johannes Faber, and Andrey Rybalchenko. Model checking duration calculus: A practical approach. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 332-346, Berlin / Heidelberg, 2006. Springer-Verlag.
• Johannes Faber. Verifying real-time aspects of the European Train Control System. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 67-70. University of Copenhagen, Denmark, October 2005.
• Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005.
• more to come soon

Contact

Andrey Rybalchenko