Sound Reasoning for Trustworthy User Interaction
Program analysis, verification, and neuro-symbolic reasoning
Research vision
My research comprises different aspects of software quality, with a particular focus on using sound reasoning to provide useful information to users. In the past years, I have worked on static error detection, fault localization, lightweight verification of object and API protocols, and neuro-symbolic reasoning over rule engines. The analyzed artifacts range from Java programs and cloud configurations to pricing agreements and executable legal rules.
Driven by the wish for verified software, program analysis has been an active field of research for decades. Despite major achievements, usability remains an open problem. Analysis tools either require extensive specifications and user interaction, or produce warnings whose relevance a developer has to establish independently. My work studies analyses with a more limited scope, but with a result usable directly. For inconsistent code, the result is a proof that no execution through a statement terminates successfully. For fault localization, it is an invariant that identifies which parts of an error trace do not need to be considered when fixing the observed error. For object construction and API use, it is a type-state property that holds without an annotation at each client use. The limitation of each analysis is part of its result: an abstraction suppresses a warning, but does not establish a property outside the modeled behavior.
Recent work considers the same problems for systems that use language models. A language model translates a question into a constraint, infers a candidate rule from documentation, or proposes an action for an agent. However, the model does not establish that the resulting formalization is complete or correct. In The Question Is a Region, a symbolic execution engine enumerates the outcomes of an under-specified question, and an SMT solver proves that the returned conditions cover the corresponding region. The language model lifts the question and presents the result; the rule engine decides each verdict. This separation makes the remaining unverified step explicit. The sections below describe the corresponding research areas, beginning with static error detection.
Sound Detection of Inconsistent Code
Inconsistent code refers to a statement that does not occur on a successful execution. The statement is either unreachable, or every execution through it leads to an error. This property requires no functional specification. Its detection reduces to proving that none of the paths through the statement is feasible and successfully terminating.
In my early work, we used a sound over-approximation of successful executions to detect inconsistent code. If the over-approximation contains no path through a statement, no concrete successful execution contains that statement. A coarse abstraction invents successful paths and therefore misses inconsistencies; it does not justify a false inconsistency report under the modeled semantics.
VC ∧ at(L6) is UNSAT because every execution through
L6 fails; hence L6 has no execution that terminates successfully.
Some inconsistent statements are deliberate or harmless. For example, compilers introduce unreachable code, and developers use unreachable branches for debugging. We therefore distinguish code whose reachability is not disproved and whose executions lead to an error from code that is unreachable for other reasons. Experiments on open-source programs showed that the former category yielded patchable bugs. Bixie findings led to accepted fixes in Tomcat, Soot, Bouncy Castle, and WildFly. The implementation approximated exceptions, reflection, threads, and integer semantics unsoundly. Consequently, its reports did not inherit the theoretical guarantee for behaviors outside this model.
Proof-Based Fault Localization
Static checkers report errors as an initial state and a trace that leads to an assertion violation. The source location of the violation does not identify its cause. Two traces ending at the same location need not depend on the same facts, and two traces ending at different locations need not have different causes. Semantic classification therefore abstracts from syntax and retains the facts relevant to the failure.
We use verification proofs for this abstraction. An error invariant follows from a trace prefix and contradicts the remaining suffix together with the expected outcome. It describes the states that necessarily lead to the error at a given program point. Craig interpolation computes such invariants from the proof using only symbols shared across the cut. If the same invariant holds before and after a block, the block does not contribute to this failure and is removed from the explanation.
y = 1 holds before
and after lines 5–7, so we replace them with havoc n without
changing this failure. The explanation is sufficient, not necessarily
minimal.
Flow-sensitive fault localization retains conditions introduced by branches and joins. Concolic fault abstraction applies the same reasoning backward from a concrete breakpoint. The proof also provides a signature for classifying error messages: invariant Hoare triples are removed, and the remaining state-changing triples characterize the cause. On our benchmarks, more than half of the error messages from procedures with multiple reports shared a signature with another message.
Lightweight Type-State Analysis
Type-state properties constrain the sequence of operations on an object. For example, a request must be configured before it is sent. Standard type-state analyses rely on explicit state annotations and precise alias information. These requirements make them difficult to apply to existing industrial code.
We studied special cases in which the analysis retains soundness without a complete alias analysis. Accumulation analysis records the set of methods that have been called on an object. Ignoring an alias loses evidence that a required method was called. It therefore produces an additional warning, not an unsound acceptance. This permits a modular type system that infers the relevant state from ordinary program statements.
new to configured
to sent; an early send has no legal transition.
Verifying Object Construction applies accumulation analysis to builders, dependency injection, and factory methods. Flow-sensitive refinement determines which setters were invoked without annotations at each client use. For common builder generators, the checker also infers which logical arguments are required. The analysis found 16 security vulnerabilities with 3 false positives in more than 9 million lines of industrial and open-source code.
Continuous Compliance applies lightweight verification to source-code audit controls. Five checkers enforce requirements for cryptographic algorithms, key lengths, credentials, HTTPS, and cloud storage. At AWS, the checkers scanned more than 68 million lines of code and required 23 annotations. External auditors accepted their output as evidence for seven services. RAPID applies related techniques to temporal cloud API protocols using value flow and guarded automata.
Neuro-Symbolic Reasoning for User Interaction
Rule engines map a fully specified set of typed inputs to an output. In a chat setting, users leave inputs open because they do not know them or do not consider them relevant. The question then denotes a region of the input space, not one point. The correct answer is a partition of that region into the conditions that produce each output.
Neither a language model nor symbolic enumeration solves this problem alone. A language model gives no completeness guarantee. Symbolic enumeration covers every path, but a large partition is difficult to present faithfully. In The Question Is a Region, a language model lifts the question to typed constraints, CUTECat enumerates paths through the rules, the unmodified rule engine evaluates one witness per output category, and Z3 proves that the resulting partition covers the lifted region. If the partition exceeds a fixed budget, guard structure selects one input for a follow-up question.
The same combination applies to other interactions with learned models. Why Is This on My Bill? uses a model to infer candidate eligibility rules from documentation, validates them against observed billing behavior, and keeps a link to the supporting text. Proof-of-Policy evaluates actions proposed by cooperating agents before execution. Policy miners approve, constrain, modify, defer, or reject each proposal, and an append-only record preserves the decision.
The lift from a natural-language question to a symbolic region remains unverified. A wrong lift yields a complete answer to the wrong question. Related translation steps occur when a model infers a billing rule or interprets an agent action. My current work studies checks for these translations and separates claims proved by the symbolic engine from claims inferred by the language model.