Symbolic Abstractions
| Layer | Target | Availability* | |||||||
|---|---|---|---|---|---|---|---|---|---|
| System | Hardware | OS | Application | Function | Type† | ISA(s) | Binary? | Source code | Data Set |
| FIE |
|
— |
|
|
3 | MSP430 | ✔️ | ||
| Firmalice |
|
|
|
|
1, 2 | ARM, PPC | ✔️ | ||
| FirmUSB |
|
— |
|
|
3 | 8051/52 | ✔️ | ✔️ | |
| Laelaps |
|
|
|
|
2, 3 | ARM | ✔️ | ✔️ | ~ |
Legend:
: Passed through
: Emulated
: Not modified
: Replaced
: Symbolic model
~: Partial Availability
* When available, source code and data sets can be found by clicking on the checkmarks.
† Target types are described in our faq.