Research Interests

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

Resume [PDF]


My Papers


Azadeh Farzan, P. Madhusudan: Monitoring Atomicity in Concurrent Programs. In proceedings of (CAV), 2008, Lecture Notes in Computer Science, volume: 5123, pages: 52 -- 65.

We study the problem of monitoring concurrent program
runs for atomicity violations. Unearthing fundamental results behind
scheduling algorithms in database control, we build space-efficient mon-
itoring algorithms for checking atomicity that use space polynomial in
the number of active threads and entities, and independent of the length
of run monitored. Second, by interpreting the monitoring algorithm as
a finite automaton, we solve the model checking problem for atomicity
of finite-state concurrent models. This remedies incorrect proofs pub-
lished in the literature. Finally, we exhibit experimental evidence that
our atomicity monitoring algorithm gives substantial time and space ben-
efits on benchmark applications.


Azadeh Farzan, Y. Chen, E. M. Clarke, Y. Tsan, B. Wang: Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2008, pages 2-17 [PDF] .

Recent studies have suggested the applicability of learning to automated compositional verification. However, current learning algorithms fall short when it comes to learning liveness properties.
We extend the automaton synthesis paradigm for the infinitary languages by presenting an algorithm to learn an arbitrary regular set of infinite sequences (an omega-regular language) over an alphabet A. Our main result is an algorithm
to learn a nondeterministic Buchi automaton that recognizes an unknown omega-regular language. This is done by learning a unique projection of it on A* using the
framework suggested by Angluin for learning regular subsets of A*.


Azadeh Farzan, José Meseguer: Partial Order Reduction for the Semantics of Programming Languages. In Electronic Notes in Theoretical Computer Science (ENTCS) 2007, volume 176(4): 61-78. [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, P. Madhusudan: Algorithms for Atomicity. manuscript, 2007. [PDF]

We study the algorithmics of checking atomicity of
in concurrent programs. Unearthing fundamental results behind
scheduling algorithms in database control, we build space-efficient
monitoring algorithms for checking atomicity. Second, by interpreting
the monitoring algorithm as a deterministic automaton, we solve
several key model checking problems for checking atomicity of finite-state
concurrent models. We establish two main results: that checking atomicity
for concurrent regular Boolean programs is PSPACE-complete, and that
checking concurrent recursive programs is decidable. The results
are based summarizing programs using profiles of runs, and checking
if the profiles witness non-serializability.


Azadeh Farzan, P. Madhusudan: Causal Dataflow Analysis for Concurrent Programs. In proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007, Lecture Notes in Computer Science, volume 4424: 102--116. [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: Making Partial Order Reduction Language Independent. 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.