pate
pate copied to clipboard
GaloisInc
Patches Assured up to Trace Equivalence
The Weakest Precondition solver had differential summaries. This notion doesn't necessarily translate cleanly to the Strongest Postcondition solver. We still need some way to tell users where divergence in traces...
This was developed for the Weakest Precondition verifier. We should be able to integrate its results for specific regions in the Strongest Postcondition verifier
To define `Pate.Ground.groundMacawEndCase` as a pure function, the abstraction boundary of `'MacawBlockEndType` is partially violated. We would like to abstract away the specific encoding of 'MacawBlockEndType', but the only function...
Currently there is a somewhat clumsy process of encoding and decoding the representation of the original block exits when slicing up the CFG into a Crucible struct. Now that the...
There is a fair amount of duplication in the code that pretty-prints the proof (for console output) and the web front end. Ideally we should be able to remove some...
Currently the equivalence of blocks containing function calls is proven compositionally, by performing three separate equivalence proofs for each function call site, computing intermediate equivalence relations for: * before the...
Currently the conditional equivalence check tries to compute a predicate that is sufficient to imply equality on two block slices. This works if the condition is confined to a single...
Currently all solver timeouts are treated identically from the perspective of reporting. Some timeouts are more significant to the verifier and therefore should be reported differently. For example, during pre-condition...
Many of our slices overlap. I don't think this is a huge problem, but it can be confusing for users browsing the proof. It also might imply substantial duplicated work....
In #125 we added the ability to prove that an equivalence condition is "valid" in the sense that non-equivalent branches result in the original binary aborting. Currently an "abort" is...