Research Interests

Software Engineering, Programming Languages, Software Verification, Formal Methods, Security (with an emphasis on concurrency)

Resume [PDF]


My Papers


Azadeh Farzan, P. Madhusudan: Causal Dataflow Analysis for Concurrent Programs. To appear in proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007. [PDF]

We define a novel formulation of dataflow analysis for concurrent programs,
where the flow of facts is along the causal dependencies of events.
We capture the control flow of concurrent programs using a Petri net
(called the control net), develop algorithms based on partially-ordered
unfoldings, and report experimental results for solving causal dataflow analysis problems.
For the subclass of distributive problems,
we prove that complexity of checking data flow is linear in the number of facts
and in the unfolding of the control net.

Azadeh Farzan, P. Madhusudan: Causal Dataflow Analysis for Concurrent Programs. Technical Report UIUCDCS-R-2007-2806, Computer Science Department, University of Illinois at Urbana-Champaign, 2007 (full version). [PDF]

We define a novel formulation of dataflow analysis for concurrent programs,
where the flow of facts is along the causal dependencies of events.
We capture the control flow of concurrent programs using a Petri net
(called the control net), develop algorithms based on partially-ordered
unfoldings, and report experimental results for solving causal dataflow analysis problems.
For the subclass of distributive problems,
we prove that complexity of checking data flow is linear in the number of facts
and in the unfolding of the control net.

Azadeh Farzan, José Meseguer: State Space Reduction of Rewrite Theories Using Invisible Transitions. In proceedings of Algebraic Methodology and Software Technology (AMAST) 2006, Lecture Notes in Computer Science, volume 4019: 142--157. [PDF]

State space explosion is the hardest challenge to the effective application of model checking methods. We present a new technique for achieving drastic state space reductions that can be applied to a very wide range of concurrent systems, namely any system specifiable as a rewrite theory. Given a rewrite theory R = (Σ, E, R) whose equational part (Σ, E) specifies some state predicates P, we identify a subset S ⊆ R of rewrite rules that are P-invisible, so that rewriting with S does not change the truth value of the predicates P. We then use S to construct a reduced rewrite theory R/S in which all states reachable by S-transitions become identified. We show that if R/S satisfies reasonable executability assumptions, then it is in fact stuttering bisimilar to R and therefore both satisfy the same ACTL*-X formulas. We can then use the typically much smaller R/S to verify such formulas. We show through several case studies that the reductions achievable this way can be huge in practice. Furthermore, we also present a generalization of our construction that instead uses a stuttering simulation and can be applied to an even broader class of systems.


Azadeh Farzan, P. Madhusudan: Causal Atomicity. In Proceedings of Computer Aided Verification (CAV) 2006, Lecture Notes in Computer Science, volume 4144: 315--328. [PDF]

Atomicity is an important generic specification that many correct concurrent programs adhere to. Intuitively, atomicity of a program block assures the programmer can pretend that the block occurs sequentially in any execution. Our main contribution is a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally captures the independence of threads, the interactions between them, and the abstraction of data. The partially ordered executions of the Petri net are then endowed with a causality relation between events; we exploit this to define our notion of causal atomicity. We show that causal atomicity is a robust notion that many programs follow, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.


Azadeh Farzan, José Meseguer: Partial Order Reduction for Rewriting Semantics of Programming Languages. In proceedings of WRLA 2006: 56-75. [PDF]

Partial order reduction (POR) capabilities are typically added by extending a model checking algorithm supporting analysis of programs in a given programming language. In this paper we propose a generic method to generate a model checker with POR capabilities for any programming language of interest. The method is based on giving a formal executable specification of the semantics of a programming language L as a rewrite theory RL , and then exploiting the efficient execution, search, and LTL model checking capabilities of the Maude rewriting logic language to generate a model checker for L essentially for free. The key idea is to achieve the desired POR reduction by means of a theory transformation that transforms the theory RL into a semantically equivalent theory which is then used to explore the POR-reduced state space. This can be done for a language L with relatively little effort (a few man-weeks in total, including defining the language semantics, for a language like Java) and has the advantage of not requiring any changes in the underlying model checker. Our experiments with the JVM and with a Promela-like language indicate that significant state space reductions and time speedups can be gained for the tools generated this way.


Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu: JavaFAN: A Rewriting Logic Approach to Formal Analysis of Multithreaded Java Programs. Technical Report UIUCDCS-R-2005-1523, Computer Science Department, University of Illinois at Urbana-Champaign, 2005. [PDF]

JavaFAN (Java Formal ANalysis) is a multithreaded program analysis framework based on rewriting logic specifications of Java. It can perform several types of analysis, including symbolic execution of Java programs, detection of safety violations searching through the potentially unbounded state space of a multithreaded program, and explicit state model checking of programs whose state space is finite. Both Java source-code and byte-code analyses are possible. The former is user-friendly, with counter-examples directly related to familiar Java source-code, and the latter affords a more precise analysis of the running code, not depending on the correctness of the compiler, and can be used even when the Java source-code of the program is not available.


Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu: Formal Analysis of Java Programs in JavaFAN. In proceedings of Computer Aided Verification (CAV) 2004, Lecture Notes in Computer Science, volume 3114: 501--505. [PDF]
JavaFAN uses a Maude rewriting logic specification of the JVM semantics as the basis of a software analysis tool with competitive performance. It supports formal analysis of concurrent JVM programs by means of symbolic simulation, breadth-first search, and LTL model checking. We discuss JavaFAN’s executable formal specification of the JVM, illustrate its formal analysis capabilities using several case studies, and compare its performance with similar Java analysis tools.


Azadeh Farzan, José Meseguer, Grigore Rosu: Formal JVM Code Analysis in JavaFAN. In proceedings of Algebraic Methodology and Software Technology (AMAST) 2004, Lecture Notes in Computer Science, volume 3116: 132--147. [PDF]


JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN’s implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories.