4 papers
Kleene Algebra with Transitive Commutativity Conditions
Han Xu, Chenyu Zhou, Zachary Kincaid +1
Kleene algebra (KA) provides a foundational algebraic framework for reasoning about program structure and control flow. To capture equivalences arising from reordering or independe…
Efficient Symbolic Execution of Software under Fault Attacks
Yuzhou Fang, Chenyu Zhou, Jingbo Wang +1
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware…
Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Jacqueline L. Mitchell, Brian Hyeongseok Kim, Chenyu Zhou +1
Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In th…
An Incremental Algorithm for Algebraic Program Analysis
Chenyu Zhou, Yuzhou Fang, Jingbo Wang +1
We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that cons…