This is a symbolic execution based automated program verifier for a toy language that I wrote one evening. I've since used it to verify an implementation of selection sort. It produces an SMT-LIBv2 script which you can feed to your solver of choice. It's quite hacky and there's no parser or CLI interface yet, I may add these when I have time.
jaspergeer/miniVerifier
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|