ENSOFT Research

Program Analysis & Algebraic Graph Methods

ENSOFT’s research develops program analysis, graph representations, and algebraic methods for verifying and securing complex software—from operating system kernels and mobile applications to compiled binaries in safety-critical embedded systems.

XCSG / Projected Control Graph37 MLOC scale

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.

Binary

IEEE/AIAA DASC · 2026PowerPC · 4B fix → 139B patch

Efficient Binary Micro-Patching for Legacy and Safety-Critical Avionics Systems

In legacy aerospace and embedded systems, missing source code or build environments often make recompilation impossible, while traditional trampolining bloats the binary. This work introduces a Graph Intermediate Representation that models binary artifacts and reference relations to compute a minimal in-place patch. Demonstrated on PowerPC, where a 4-byte functional fix requires a 139-byte total patch without reassembly.

Payas Awadhutkar, Ahmed Tamrawi, Jeremías SaucedaIEEE/AIAA DASC 2026 · Best of Session

Computers & Security · 2022CFG Isomorphism

Control Flow Equivalence Method for Establishing Sanctity of Compiling

Rather than attempting to prove compiler correctness in the abstract, this method verifies that a compiled binary’s control flow is consistent with its source for a specific program under audit. Equivalence is established by checking control-flow graph isomorphism after semantics-preserving transformations, producing evidence suitable for manual cross-checking and tool qualification in avionics, automotive, and medical software.

Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, Suresh Kothari10.1016/j.cose.2022.102608

Cybersecurity

Winter Simulation Conference · 2017DARPA STAC

Modeling Lessons from Verifying Large Software Systems for Safety and Security

An empirical verification study of 66,609 lock instances across more than 12 million lines of the Linux kernel. High-level behavior models verified 99.3% of the instances—compared to 65.7% for the Linux Driver Verification formal verification tool—exposed flaws in prior verification results, and uncovered seven unsafe locking defects confirmed and fixed by kernel developers.

Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi, Jon Mathews10.1109/WSC.2017.8247886

99.3% vs. 65.7%Of 66,609 Linux kernel lock instances verified across 12+ MLOC, uncovering 7 unsafe locks fixed by kernel developers.

Program Analysis & Graph Representations

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

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

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