HolBA
HolBA copied to clipboard
kth-step
Binary analysis in HOL
The following code is not built/tested in CI, there should probably be a decision on what to do with it (e.g., moving to `attic`): - [src/tools/exec/examples/example-toy.sml](https://github.com/kth-step/HolBA/blob/master/src/tools/exec/examples/example-toy.sml) - [src/tools/cfg/examples/example-aes.sml](https://github.com/kth-step/HolBA/blob/master/src/tools/cfg/examples/example-aes.sml) - [src/tools/cfg/examples/example-old-simple.sml](https://github.com/kth-step/HolBA/blob/master/src/tools/cfg/examples/example-old-simple.sml)...
SMT interface and symbolic execution stuff is left in the `support` and `support2` directories of the tutorial. We need to decide where to place these things.
Currently, there exists multiple ways to interface with the lifter. We should choose one standard interface to the lifter. Concretely, this would mean looking at `bir_lifter_simple_interfaceLib.sml` and `bir_lifter_interfaceLib.sml` and merging...
Currently there exists multiple ways to interface with the WP generator and prover. We should choose one standard interface for it. Concretely, this would mean looking at `bir_wp_interfaceLib.sml` and `easy_noproof_wpLib.sml`...
In PR #135 we encapsulate the library inclusions in the lifter libraries to put an end to the era of its binding pollution throughout HolBA (i.e., everything that happens to...
In PR #130 we remove the dependency graph from README.md because it is stale and we don't have a script to update it quickly. We need to either fix the...
`bir_wm_instTheory` contains the theorem `bir_map_prog_comp_thm`, which allows for enlarging the program upon which the contract is stated. Together with the other composition theorems, this means that contracts for BIR subprogram...
The BIR language and its semantics could be worth specifying and documenting standalone, most directly using [Lem](https://github.com/rems-project/lem). Encoding BIR in Lem would also allow porting it to other proof assistants...
Many kinds of documentation of a project like this are useful. Here is an attempt to break down different kinds of documentation and provide hints about how they can be...
To make the library easier to use for others, one option is to do explicit tags/releases in the repo that are guaranteed to work with a certain combination of versions...