Commit a8bc648b authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added README

parent d94b7b24
# Verifying AVR multiprecision multiplication routines using Why3
## Files
1. avrmodel.mlw - WhyML model for the AVR instruction set architecture
2. avrmodel/ - Why3 session files
3. avr_code.mlw - AVR assembly translated to WhyML
4. avr_code/ - Why3 session files
These can be viewed at:
https://gitlab.science.ru.nl/sovereign/why3-avr/tree/master
## Checking the proofs
The proofs were developed using Why3 0.87.2; as well as the following theorem provers:
* Alt-Ergo 1.01
* CVC3 2.4.1
* CVC4 1.4
* Eprover 1.8
* Z3 4.4.1
Then, simply running `why3 replay -L . avr_code` should work.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment