Home
Welcome to the BASIL wiki!
BASIL generates semantically correct Boogie source files (.bpl) from AArch64/ARM64 binaries, with the intent of reasoning about concurrent programs through a rely-guarantee framework.
We use a lifter (currently BAP) to take a binary to an intermediate representation, BASIL's IR (IR). We then perform a series of conservative analyses on this to obtain an accurate representation of the program's structure. This is then translated into Boogie's IVL.
Copyright 2022 The University of Queensland
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at:
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.