Underlying Research

Machine-check is based on a novel Input-based Three-valued Abstraction Refinement framework, which allows verification of properties in branching-time logics while using model-checking with abstraction refinement, which makes it possible to verify non-trivial systems.

A preprint of the paper on the framework is available at arXiv:

  • Onderka, J., Ratschan, S. Input-based three-valued abstraction refinement (preprint). arXiv:2408.12668 [cs.LO]. 2024.

Published papers on other techniques introduced for machine-check:

  • Onderka, J. Formal verification of machine-code systems by translation of simulable descriptions. In Proceedings of the 13th Mediterranean Conference on Embedded Computing, MECO 2024. Budva, Montenegro, 2024. doi:10.1109/MECO62516.2024.10577942.
  • Onderka, J., Ratschan, S. Fast three-valued abstract bit-vector arithmetic. In Finkbeiner, B., Wies, T., editors, Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022, pages 242–262. Springer Nature Switzerland, Cham, 2022. ISBN: 978-3-030-94583-1. doi:10.1007/978-3-030-94583-1_12.

The research might be too indigestible to most people (which is fine, since the point of the tool is that you shouldn't need to perfectly know what is happening underneath). For something simpler, consider this presentation:

Also see the blogposts about machine-check.