Research
Interests
Software
Engineering, Programming Languages, Software Verification,
Formal Methods, Security (all with an emphasis on
concurrency)
My
Papers
Azadeh
Farzan,
P. Madhusudan,
Francesco Sorrentino:
Meta Analysis of Concurrent Program Runs With Nested
Locking For Atomicity Violations.
In Proceedings of
CAV
2009, Lecture Notes in Computer Science, volume: 5643,
pages: 248 -- 262
[PDF]
.
We
study the problem of determining, given a run of a
concurrent program, whether there is any alternate
execution of it that violates atomicity, where atomicity is
defined using marked blocks of local runs. We show that if
a concurrent program adopts nested locking, the problem of
predicting atomicity violations is efficiently solvable,
without exploring all interleavings. In particular, for the
case of atomicity violations involving only two threads and
a single variable, which covers many of the atomicity
errors reported in bug databases, we exhibit efficient
algorithms that work in time that is linear in the length
of the runs, and quadratic in the number of threads.
Moreover, we report on an implementation of this algorithm,
and show experimentally that it scales well for benchmark
concurrent programs and is effective in predicting a large
number of atomicity violations even from a single
run.
Azadeh
Farzan,
P. Madhusudan:
The Complexity of Predicting Atomicity
Violations.
In Proceedings
TACAS
2009, Lecture Notes in Computer Science, volume: 5505,
pages: 31 -- 45
[PDF]
.
We
study the prediction of runs that violate atomicity
from
a single run, or from a regular or pushdown model of a
concurrent program. When prediction ignores all
synchronization, we show predicting
from a single run (or from a regular model) is solvable in
time
O(n
+k.ck)
where
n
is the length of the run (or the size of the regular
model),
k
is
the number of threads, and
c
is a constant. This is a significant improvement from the
simple
O(nk
·
2k2)
algorithm that results from building a
global automaton and monitoring it. We also show that,
surprisingly, the
problem is decidable for model checking recursive
concurrent programs
without synchronizations. Our results use a novel notion of
a
profile
: we
extract profiles from each thread locally and
compositionally combine
their effects to predict atomicity violations.
For threads synchronizing using a set of locks
L, we show that prediction
from runs and regular models can be done in time
O(nk
·
2|L|· log k+k2).
Notice that we are unable to remove the factor
k
from the exponent on
n
in this case. However, we show that a faster algorithm
is
unlikely
: more
precisely, we show that prediction for regular programs is
unlikely to
be fixed-parameter tractable in the parameters (k,
|L|) by proving it is
W
[1]-hard. We also show, not surprisingly, that prediction
of atomicity
violations on recursive models communicating using locks is
undecidable.
Y.
Chen, Azadeh Farzan,
E. M. Clarke,
Y. Tsan,
B. Wang:
Extending AutomatedLearning Minimal Separating DFAs for
Compositional Verification.
In Proceedings
TACAS
2009, Lecture Notes in Computer Science, volume: 5505,
pages: 155 -- 169
[PDF]
.
Algorithms
for learning a minimal separating DFA of two
disjoint
regular languages have been proposed and adapted for
different
applications.
One of the most important applications is learning
mini-
mal
contextual assumptions in automated compositional
verification. We
propose
in this paper an efficient learning algorithm,
called
LSep
, that
learns
and generates a minimal separating DFA. Our algorithm has
a
quadratic
query complexity in the product of sizes of the minimal
DFA's
for
the two input languages. In contrast, the most recent
algorithm of
Gupta
et al.
has an exponential query complexity in the sizes of the
two
DFA's.
Moreover, experimental results show that our learning
algorithm
significantly
outperforms all existing algorithms on
randomly-generated
example
problems. We describe how our algorithm can be adapted
for
automated
compositional verification. The adapted version is
evaluated
on
the LTSA benchmarks and compared with other automated
com-
positional
verification approaches. The result shows that our
algorithm
surpasses
others in 30 of 49 benchmark problems.
Azadeh Farzan,
P. Madhusudan:
Monitoring Atomicity in Concurrent
Programs.
In proceedings of (CAV),
2008, Lecture Notes in Computer Science, volume: 5123,
pages: 52 -- 65
[PDF]
.
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:
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.