Home

BASIL Wiki

This Wiki is no longer updated, for current documentation see: /docs

What is BASIL?

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.

Wiki Contents

Developing

• Intellij
• VSCode

Program Structure

• ADT to BASIL IR translating
• BASIL IR
• CFG
• Analyses

Misc

• .dot files for this Wiki
• Verification status of examples

Open Source Licence

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.