There was an error while loading. Please reload this page.
Updated Making a new VerCors release (markdown)
Add some information about --check-integer-bounds
Updated PVL Syntax Reference (markdown)
Updated Specification Syntax (markdown)
Updated VerCors usage, tips & proof debugging tips (markdown)
Add link to VerCors usage & tips
Updated _Sidebar (markdown)
Add some proof debugging hints
Updated
Mention loop invariants on labels
Update explanation of pointers and arrays
Escape bar | in table
Updated Axiomatic Data Types (markdown)
Add paper reference for triggers
Add unicode syntax for assert
Add starall syntax
Update adt link
Remove pure static (only pure)
Make the lock/unlock things pass on current dev (was not passing anyway on website)
Bool to boolean in java
Fix example, add ghost
Fix not running code examples
Add a note about the 8-bit bytes assumption
Extend explanation pointer_length, add explanation of pointer_block
Updated Home (markdown)