Implement Trace Lemmas - Githubissues

gleiss / rapid

Software Verification tool, which uses superposition-based theorem proving to establish the functional correctness of array- and hyper-properties.

3 stars 6 forks source link

Implement Trace Lemmas #11

Closed gleiss closed 5 years ago

gleiss commented 5 years ago

Adopt the trace lemmas from QuIt to the new Spectre setting: We have a new syntax, but more crucially we support a much more expressive language, with multiple locations and nested program statements.