issues
search
TikhonJelvis
/
imp
Some scripts for analyzing IMP programs with the Z3 automatic theorem prover, originally written for my Compose 2016 talk.
http://jelv.is/talks/compose-2016
BSD 3-Clause "New" or "Revised" License
16
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Proofs of (non-looping) non-termination and associated pattern synthesis
#4
void4
opened
5 months ago
0
Does an alternative to loop unrolling exist?
#3
void4
opened
5 months ago
0
Feature request: IMP Array support
#2
void4
opened
5 months ago
3
backwardsExample: How to rewrite gcd.imp to let Z3 find initial variable assignments?
#1
void4
closed
5 months ago
0