College of Computer and Information Science
Northeastern University
360 Huntington Avenue
Boston, Massachusetts 02115
Office: 202 West Village H, room 344
Phone: ++16173733100
Email: wahl–ät–ccs.neu.edu



NEWS: (as of late summer 2017)
Brief bio:
 2011–present: Fulltime faculty at Northeastern University, College of Computer and Information Science
 2009–2011: Research Assistant, Oxford University, Department of Computer Science (formerly "Computing Laboratory"), UK
 2007–2009: Lecturer and Postdoc, Swiss Federal Institute of Technology (ETH), Zurich, Switzerland
 2007, 2005: Ph.D. & M.S., University of Texas, Austin
General research interests:
 Software verification techniques, such as predicate abstraction, SAT and SMT solving, decision procedures, interpolation
 Infinitestate system verification, such as modeling and analyzing arbitrarilythreaded programs via counter systems and Petri nets
 Stability, robustness, reliability of numeric computations; floatingpoint arithmetic decision procedures
Current projects:
 Parameteraware program verification:
Many system designs are naturally defined (consciously or not) over a
variable number of certain resources, by which we mean physical or
logical (= design) entities of which there are several copies in any
concrete design, but at design time that number is left unspecified.
Examples include:
 the number of physical components of a certain functional type,
 the number of clients that simultaneously request a service from a server,
 the capacity of the communication channel between components,
 the number of context switches permitted among concurrent processes,
 the recursion nesting depth (= stack size) permitted in a piece of software.
The copies of the resource are structurally identical, so we can expect
that the behavior of the instances of the parametric design family (= the
concrete designs for each parameter choice) depend on the parameter in a
smooth, "continuous" way. This enables analyses of the function that maps
the number of resource instances (= the parameter) to a concrete design
(this function goes from the natural numbers to the design space).
More concretely, suppose k is a (possibly unbounded) parameter of
the design. With the target property P to be verified in mind, we
define a function O mapping the parameter to observations
about the design of size k, such that knowledge of O(k)
enables a decision whether P holds of the instance of size k.
For example, the "observation" could simply be the set of states reachable
in the system of size k. In general, we require of function O
that it be monotone.
We now analyze the system design for increasing values of k. Due to
monotonicity of O, consecutive observations O(k) are in some
sort of ≤ relationship. This begs the question whether the
function O
converges at some parameter
point k_{0}, i.e. whether it stops increasing
after reaching k_{0}. If so, the truth value
of property P has stabilized, i.e. unless we have found a problem so
far, we have proved the property for all parameter instances.
This is ongoing work.
 Analyzing floatingpoint programs for lack of portability due to compiler and hardware dependencies:
The precise semantics of floatingpoint arithmetic programs depends on the
execution platform, including the compiler and the target hardware.
Platform dependencies are particularly pronounced for arithmeticintensive
numeric programs and infringe on the highly desirable goal of software
portability: the same program run on the same inputs on different platforms
can produce different results.
Serious doubts on the portability of numeric applications arise when these
differences are behavioral, i.e. when they lead to changes in the control
flow of a program. We have developed a method that takes a numeric
procedure and determines whether a given input may cause the procedure to
make different decisions, based merely on the floatingpoint platform on
which it is compiled and executed. This method can be used in static and
dynamic analyses of programs, to estimate their numeric
stability. [EUROPAR
2015]
A project website can be found here.
Most recently, we developed a method that can repair, or at least
ameliorate, numeric instability against platform changes, making numeric
programs more robust. This is in principle easy, by instructing the
compiler to evaluate every expression following a "strict" evaluation
model, such as "lefttoright", and to ignore any preision or efficiency
optimization features, such as contracted operations, special
floatingpoint division routines, etc., acros the whole program. But this
can lead to inefficiet code: often times numeric instability is caused only
by certain critical program fragments; we don't want to take away the
compiler's freedom to optimize the others, which do not contribute (much)
to instability.
Our method therefore first identifies what these critical program
statements are, and then stabilizes them within a small local scope. The
goal is to produce programs with a good balance between efficiency and
robustness against platform
changes. [VMCAI
2017]
 Deciding floatingpoint formulas via proxy theories:
We are working on an approach to reasoning about floatingpoint arithmetic
(FPA) that reduces solving an FPA formula f to reasoning over a
related but easiertosolve proxy theory T, such as real arithmetic,
or reducedprecision FPA. The rationale is that a satisfying proxy
assignment may directly correspond to a model for f. If it doesn't,
our approach is to lift an encountered T model to a
numerically close FPA model. Other than assuming some "proximity"
of T to FPA, our lifting procedure is Tagnostic: it is
designed to work independently of how the proxy assignment was obtained.
Should the lifting fail, our procedure gradually reduces the gap between
the FPA and the proxy interpretations
of f. [FMCAD
2016]
 Predicate abstraction for concurrent software:
Predicate abstraction is a technique for overapproximating systemlevel
software by programs over Booleanvalued variables. It has proved to be a
success story in sequential program verification, especially for
controlintensive programs. My work with colleagues from Oxford University
has targeted extending this technique to multithreaded programs. We have
investigated the requirements for sharedvariable concurrent predicate
abstraction, both for the case of a known number of
threads [FMSD
2012], as well as for the unbounded
case [IaC
2016], where the number of threads is initially unknown or may
dynamically change at runtime.
The highlevel result is that, while concurrent predicate abstraction
reduces data complexity substantially (as in the sequential case), we have
to pay for that by an increase in concurrency control complexity, even in
the boundedthread case.
For information on the implementation and on some benchmarks, see
our CProver website.
 Reachability analysis for abstract unboundedthread software models:
Our abstract unboundedthread software models (obtained using predicate
abstraction, as sketched above) are thread transition systems. This
model, described in
detail here,
is equivalent in expressive power to Petri nets, but explicitly reflects
the replicated nature of multiple threads executing a given procedure. With
colleagues from Oxford University we have developed efficient
explicitstate reachability techniques for such
models. [TOPLAS
2014]
A project website can be found here.
Symbolic analysis for such (infinitestate) systems is very hard. Inspired
by work on symbolic coverability analysis at CAV 2014, we overapproximate reachability
questions in a way that makes it expressible compactly as a Presburger
arithmetic formula. The method is very efficient and highly precise,
despite its approximative
nature. [IJCAR
2016]
The tool can be obtained
from here.
Research sponsors:
Conference program or organizing committees:

VMCAI 2018,
FMCAD 2017, CAV 2017,
CAV 2016, ICFEM 2016,
FMCAD 2015, CAV 2015,
FMCAD 2014, CAV 2014,
CAV 2013, FMCAD 2013, DATE 2013,
FMCAD 2012, VALID 2012, MemoCode 2012, SPIN 2012
Awards:

