ENSOFT Research · Algebra & Graphs

Algebra & Graph Representations

Path Algebra models execution behavior as a non-commutative ring, where products, sums, and factorizations stand in for paths, branches, and loops. The eXtensible Common Software Graph (XCSG), Projected Control Graphs (PCG), and Event Flow Graphs (EFG) are homomorphic projections of that behavior, queried on the Atlas platform without enumerating every path.

e1(e2 + e3)e4 · ab ≠ bah: XCSG → PCG
Path Algebra factorizationXCSG → PCG

Path Algebra

19 November 2025

A High School Algebra Solution for the Shortest Path Problem

An algebraic framework for graph problems, demonstrated on the shortest-path problem as an alternative to traversal algorithms such as Dijkstra and Bellman–Ford. Path segments are modeled as algebraic expressions, and shortest paths—including in graphs with negative edge weights and negative cycles—are derived through equation solving and factorization rather than iterative state updates. The paper also examines “all-paths” problems where explicit graph traversal becomes intractable.

Suresh C. Kothari, Payas AwadhutkarRead the paper →

Algebraic FactorizationSolves shortest-path and all-paths formulations—including negative edge weights and negative cycles—without iterative graph traversal.
15 July 2023Path Algebra · Soft Infinity

Path Algebra for Scalable and Transparent Software Security

Introduces Path Algebra, a non-commutative ring built on SymPy and integrated into Atlas to represent the “soft infinity” of execution behaviors without enumerating paths. Execution paths are modeled as products of variables, branches as sums, and loops as divisions with loop bodies represented once—enabling scalable, transparent verification and vulnerability analysis across C, C++, Java, Simulink, bytecode, and binaries.

Suresh KothariRead the paper →

Non-Commutative RingCompactly represents the “soft infinity” of execution paths across branches, loops, and inter-procedural calls while preserving direct CFG correspondence.

Program Graphs, Projections & Platform

13 August 202437 MLOC · 8 Bugs

A Humane, Graph-Based Representation of Programs and Analyses

Introduces the eXtensible Common Software Graph (XCSG), a semantic graph representation and query language designed for human-machine collaboration on verification problems where standalone automation does not scale. A verification tool built on XCSG has been used to audit safety and security properties across 37 million lines of code, uncovering eight confirmed bugs.

Jon Mathews, Theodore Murdock, Jeremías Sauceda, Ahmed Tamrawi, Suresh KothariRead the paper →

Science of Computer Programming · 2018DARPA STAC

Projected Control Graph for Computing Relevant Program Behaviors

Defines a mathematical foundation for isolating the program behaviors relevant to a safety or security property and introduces the Projected Control Graph (PCG) to compute that projection directly, avoiding full-program path enumeration. Evaluated on Linux kernel lock verification and on interactive detection of side-channel vulnerabilities in Java bytecode.

Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003

ICSE · 2018DARPA STAC · PCG Toolbox

COMB: Computing Relevant Program Behaviors

Presents COMB, a multi-language interactive program comprehension and verification tool that uses the Projected Control Graph (PCG) abstraction to derive relevant execution behaviors directly without enumerating all program paths. Demonstrated on C and Java case studies including Linux kernel verification.

Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/3183440.3183476

IEEE ICSME DOCGEN Challenge · 2018DARPA STAC · Best Tool Award

DynaDoc: Automated On-Demand Context-Specific Documentation

An on-demand documentation engine built on Atlas and XCSG that extracts control flow, call, and data-flow graphs alongside issue and commit history from multi-million-line codebases. Demonstrated on Apache POI, where data-flow projections exposed undocumented parameter constraints and uncovered a previously unreported defect.

Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009

APSEC · 2016DARPA STAC · Path-Sensitive Analysis

Projected Control Graph for Accurate and Efficient Analysis of Safety and Security Vulnerabilities

Introduces the Projected Control Graph (PCG) abstraction to overcome exponential path growth and path-feasibility complexity in path-sensitive analysis. Evaluates CFG-to-PCG reduction across three versions of the Linux kernel (66,609 lock instances), revealing synchronization bugs missed by the Linux Driver Verification (LDV) tool.

Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026

ICSE · 2014DARPA APAC

Atlas: A New Way to Explore Software, Build Analysis Tools

Presents the Atlas software analysis platform, which decouples program indexing from domain-specific analysis: polynomial-time static analyzers build an attributed graph database of the program, which engineers then query interactively or through analysis scripts. Validated on Linux kernel synchronization verification and Android malware detection.

Tom Deering, Suresh Kothari, Jeremías Sauceda, Jon Mathews10.1145/2591062.2591065

4 April 201499% Path Reduction · EFG

Event-Flow Graphs for Efficient Path-Sensitive Analyses

Partitions control-flow graph paths into equivalence classes via a linear-time transformation into an Event-Flow Graph (EFG), a compact CFG derivative whose paths preserve all property-relevant event traces. Evaluated on the Linux kernel (v3.12) for spin safe-synchronization, achieving close to 99% reduction for CFGs with a large number of paths and demonstrating human comprehensibility in a controlled experiment.

Ahmed Tamrawi, Suresh KothariRead the paper →

12 November 2013Order-Preserving CFG Reductions

Reduction-Based Transformations on Control Flow Graphs

Models software vulnerabilities—including unsafe thread synchronization, memory leaks, and smartphone data exfiltration—as ordered occurrences of event nodes along control-flow paths, and defines size-reducing graph transformations that collapse exponential CFGs while preserving vulnerability-relevant ordering.

Akshay Deepak, Ahmed Tamrawi, Suresh KothariRead the paper →