Context-Free Language Analysis

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

• CFL Reachability Components
  • Classical CFL Reachability
  • Interleaved-Dyck Core
  • Exact Unary Interleaved Dyck
  • Interleaved-Dyck Staged Bounds
  • Multiple Context-Free Language Reachability
  • Guarantee Summary
  • CSIndex (Context-Sensitive Indexing)
  • Interleaved-Dyck Graph Reduction
  • Mutual Refinement
• Classical Grammar-Driven CFL Reachability
  • Architecture
  • Solver backends
  • Querying compressed results
  • POCR support utilities
  • Adapters
  • Command line
  • Input formats
• POCR Migration Matrix
  • General solvers
  • Clients and preprocessing
  • Formats, relations, and controls
• Paper Engines: PEARL, Stg, and Sqid
  • Coverage summary
• Context-Sensitive Reachability Indexing
  • FLARE
  • SCS
  • Build and tools
• Exact Unary Interleaved Dyck
  • Algorithms
  • Construction and performance
  • Exactness and directed input
  • Command line
  • Build and test
• Interleaved-Dyck Staged Bounds
  • Relationship to MutualRefinement
  • Graph Model
  • Staged-Bounds Pipeline
  • Using the Solver
  • Benchmark Modes
  • Build and Test
  • Cost Considerations
• Interleaved-Dyck Graph Reduction
  • Pipeline
  • Bidirected handling
  • Implementation boundary
• Multiple Context-Free Language Reachability
  • Choosing an MCFL API
  • Generic MCFL Solver
  • Interleaved-Dyck Underapproximation
  • Shared typed graph adapter
  • Command-Line Tool
  • Validation and Complexity
• Mutual Refinement for CFL Reachability
  • Responsibility Boundary
  • Experiment workflow