Verification Backend Abstraction

Lotus provides a unified interface to multiple verification backends, allowing you to switch between different tools seamlessly.

Overview

The verification backend abstraction layer provides:

Unified interface: Same API for all verification tools
Automatic backend selection: Choose backend based on property type
Result normalization: Consistent result format across backends
Easy integration: Add new backends without changing client code

Supported Backends

seahorn: SeaHorn CHC-based verification (supports all properties)
sifa: Sifa symbolic abstraction (reachability)
symabs_ai: SymAbsAI framework (reachability, memsafety, overflow)
clam: CLAM abstract interpretation (memsafety, overflow, reachability)

Property Classes

reachability: Target location is reachable/unreachable
memsafety: Memory safety (null pointer, use-after-free, etc.)
overflow: Integer overflow detection
termination: Program termination

Usage

Basic usage with lotus-verify:

# Auto-select backend
lotus-verify input.bc --property unreach-call --backend auto --run

# Specify backend explicitly
lotus-verify input.bc --property memsafety --backend seahorn --run

# With timeout
lotus-verify input.bc --property overflow --backend clam --timeout 60 --run

# Pass extra arguments to backend
lotus-verify input.bc --property unreach-call --backend seahorn \
  --backend-arg --horn-cex --run

Result Format

All backends normalize results to a standard format:

true: Property holds (no error found)
false: Property violated (error found)
unknown: Could not determine
error: Verification tool error
timeout: Verification timed out

Example Output

backend: seahorn
property: unreach-call
command: seahorn input.bc
result: true
message: Property holds (no error found)
exit-code: 0

Programmatic Usage

#include "Verification/Backend/Backend.h"

using namespace lotus::verification::backend;

BackendRegistry &reg = BackendRegistry::instance();
auto backend = reg.create("seahorn");

VerificationTask task;
task.inputBitcode = "input.bc";
task.property = PropertyClass::Reachability;
task.timeoutSeconds = 60;

auto cmd = backend->buildCommand(task);
// Execute command...
VerificationResultInfo result = backend->parseResult(output, exitCode);

if (result.isSafe()) {
  // Property holds
} else if (result.hasError()) {
  // Property violated
}

Adding New Backends

To add a new backend, implement the IBackend interface:

class MyBackend final : public IBackend {
public:
  const char *name() const override { return "mybackend"; }

  bool supports(PropertyClass property) const override {
    return property == PropertyClass::Reachability;
  }

  std::vector<std::string>
  buildCommand(const VerificationTask &task) const override {
    return {"mybackend", task.inputBitcode};
  }

  VerificationResultInfo parseResult(const std::string &output,
                                     int exitCode) const override {
    VerificationResultInfo info;
    // Parse output and set info.result, info.message, etc.
    return info;
  }
};

Then register it in BackendRegistry::create().