Lotus

User Guide

  • Major Components Overview
  • Architecture Overview
  • Quick Start Guide
  • Installation Guide
  • Tutorials and Examples
  • Bug Detection with Lotus
  • PDG Query Language (Cypher)
  • Property-Based Slicing
  • Verification Backend Abstraction
  • Instrumentation Passes
  • Troubleshooting and FAQ
  • Command-Line Tools

Core Components

  • Alias Analysis
  • Analysis Framework
  • Annotations
  • Applications
  • Context-Free Language Analysis
    • CFL Reachability Components
    • CSIndex: Indexed Context-Sensitive CFL Reachability
    • Interleaved Dyck Graph Reduction
    • Mutual Refinement for CFL Reachability
  • Data Flow Analysis
  • Intermediate Representations
  • Overview
  • MemoryMLFeaturesPass
  • Features Extracted
  • Feature Output
  • Analysis Dependencies
  • Integration Notes
  • Related Components
  • Optimization
  • Solvers
  • Transforms
  • Utilities
  • Verification
  • Checker Framework

Developer Documentation

  • API Reference
  • Developer Guide
Lotus
  • Context-Free Language Analysis
  • View page source

Context-Free Language Analysis

This section covers CFL-reachability and context-free language based analyses.

  • CFL Reachability Components
    • CSIndex (Context-Sensitive Indexing)
    • InterDyckGraphReduce
    • MutualRefinement
  • CSIndex: Indexed Context-Sensitive CFL Reachability
  • Interleaved Dyck Graph Reduction
  • Mutual Refinement for CFL Reachability
Previous Next

© Copyright 2024-2025, ZJU Programming Languages and Automated Reasoning Group.

Built with Sphinx using a theme provided by Read the Docs.