ARMC is a tool for the verification of reachability and termination properties.
Download ARMC for Linux/x86 and MacOS X/x86 (version August 2011),
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.
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 binary
,
and
MacOS X/x86
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.
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.