Understanding Ghost Variables in Software Verification

Verification tools often support the use of ghost variables to help in the verification process. A ghost variable is not needed for the program to execute, and will not be compiled into object code. Typically, they are declared with a ghost modifier or similar, but are otherwise identical to normal program variables (i.e. they . . . → Read More: Understanding Ghost Variables in Software Verification

Whiley v0.3.25 Released!

Time for another release of the Whiley compiler. This is relatively low key, though includes the first steps towards an improved bytecode API (see #190). There are also a range of bug fixes for various minor issues:

Refactoring wyil.lang.Code and wyil.lang.CodeBlock.  In order to support proper nested bytecode blocks, I am refactoring the WyIL . . . → Read More: Whiley v0.3.25 Released!