Roberto Guanciale

**Describe the bug** A clear and concise description of what the bug is. **To Reproduce** Steps to reproduce the behavior: Change number of CharacterPosition from 4 to 3, or increase...

Running S2JSPluginRunner object scala not found

2

When I use sbt to package s2js everything goes fine and the scala dependencies are download into project/boot I manually create the bin directory, but when I execute run inside...

It would be nice to prove the example using two different approaches: - composing contracts in BIR - composing contracts in ARM

How do we compose contracts? - exec-to-label has composition problems - ?n exec-blocks is weaker and does not allow

Short term verification goals

1

Let say we fix some short term verification goals (i.e. end of August): - Addition using registers? - Addition using memory? wow - SQRT? - Binary search?

Simplified toolbox for BinaryAnalysis

1

A toolbox to use HolBA without any knowledge about HOL4 Requires a DSL to specify contracts and mechanism to compose theorems

The presence of BIR variables in predicates makes a bit complicated the definition of tautologies. The current definition states: ``` tautology(P) = ! s. init_var(s, vars(P)) ==> eval(s, P) =...

WP simplification uses definition. This has problem with the usage of free variables in the postcondition. Moreover, WP simplification introduces BIR variables. Can we use HOL4 variables?