# Symbolic Execution

Smart contract auditing is a crucial step in ensuring the security and reliability of blockchain applications. Accelchain employs Symbolic Execution as a powerful technique for auditing contracts, identifying vulnerabilities, and adhering to the guidelines specified by the Ethereum.org SWC (Smart Contract Weaknesses and Common Vulnerabilities) Registry.

#### **Symbolic Execution Overview**

* *Definition:* Symbolic Execution involves systematically exploring possible program states by running contract bytecode and its dependencies through a compiler.
* *Process:* The contract is executed symbolically, and the analysis encompasses multiple transactions and potential states.

#### **Compiler Integration**

* *Comprehensive Analysis:* Accelchain integrates with a compiler to analyze contract bytecode thoroughly.
* *Dependency Consideration:* The process includes all dependencies, such as imported contracts, ensuring a holistic approach to auditing.

#### **Test Case Generation:**

* *SWC IDs and Test Cases:* Test cases are designed with a focus on SWC IDs specified by the Ethereum.org registry.\
  <https://swcregistry.io/>
* *Exploration of States:* Test cases systematically explore various program states, identifying potential vulnerabilities.

#### **Audit Report Generation:**

* *Detailed Information:* The resulting audit report provides detailed information on identified vulnerabilities.
* *Report Components:* SWC Error ID, Error Title, Function with the error, lines containing the error, and severity are included.
* *Severity Levels:* Issues are categorized by severity, allowing prioritization based on the criticality of each vulnerability.

{% hint style="info" %}
Note that Accelchain's symbolic execution is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

To overcome this, Accelchain provides users with a combined comprehensive Audit Report based on findings generated from multiple features like ['AI Audits'](/docs/audit/ai-static-analysis.md) for static analysis, Symbolic execution etc.
{% endhint %}


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://accelchain.gitbook.io/docs/audit/symbolic-execution.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.