MINA - Tool for Verification of Programs with an Unbounded Number of Threads

  1. News
  2. About
  3. Source Code
  4. Conference Papers
  5. Benchmarks
  6. Contact
  7. Related Papers
  8. Acknowledgement

News

February, 2017:The paper about MINA has been accepted to appear at EUROCAST'17.
October, 2016:The poster about MINA has been accepted to appear at MEMICS'16.


About

MINA is a tool for verification of programs with an unbounded number of threads. The method implemented in this tool is in the direction originating from or conceptually similar to backward reachability analysis [1], especially close to recent works [2, 3, 4] that are based on learning a safe inductive invariant of the similar form by a sequence of refinements learned from counterexamples. Our goal is to improve the overall efficiency of these approaches by concentrating on choosing refinements that lead to a more succinct invariants.

Note that the tool is an early prototype which handles only a very restricted subset of benchmarks.



Source Code

mina-2017-09-12.zip


Conference Papers

1.
Lukas Holik, and Lenka Turonova. Smaller Invariants for Proving Coverability of Parallel Programs. EUROCAST'17, 2017.


Benchmarks

We use a set of benchmarks which comes from the mist2 distribution. The original set of files can be retrieved from Pierre Ganty's mist2 website here.

Contact

If you have further questions, do not hesitate to contact authors:

[1]
Parosh Aziz Abdulla. Well (and better) quasi-ordered transition systems . Bulletin of Symbolic Logic, (4), 2010.
[2]
Pierre Ganty, Jean-Francois Raskin, and Laurent Van Begin. A complete abstract interpretation framework for coverability properties of WSTS . In VMCAI'06, volume 3855 of LNCS, pages 49-64. Springer, 2006.
[3]
Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient coverability analysis by proof minimization . In CONCUR'12, volume 7454 of LNCS. Springer, 2012.
[4]
Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac. Incremental, inductive coverability . In CAV'13, volume 8044 of LNCS. Springer, 2013.

Acknowledgements

This work is supported by the AQUAS: Aggregated Quality Assurance for Systems (737475), the Czech Science Foundation (projects 14-11384S, 16-24707Y, 17-12465S), the internal BUT FIT project FIT-S-17-4014, and the IT4IXS: IT4Innovations Excellence in Science (LQ1602).