College of Computer and Information Science
360 Huntington Avenue
Boston, Massachusetts 02115
Office: 202 West Village H, room 344
Email: wahl[ – ät – ]ccs.neu.edu
NEWS: (as of Summer 2016)
- 2011 – present: Assistant Professor, 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, such as using predicate abstraction, SAT- and SMT solvers, decision procedures, interpolation
- Infinite-state system verification, such as modeling and analyzing arbitrarily-threaded programs via counter systems and Petri nets
- Stability, robustness, reliability of numeric computations; floating-point arithmetic decision procedures
- Predicate abstraction for concurrent software:
Predicate abstraction is a technique for overapproximating system-level software by programs over Boolean-valued variables. It has proved to be a success story in sequential program verification, especially for control-intensive programs. My work with colleagues from Oxford University has targeted extending this technique to multi-threaded programs. We have investigated the requirements for shared-variable 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 high-level 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 bounded-thread case.
For information on the implementation and on some benchmarks, see our CProver website.
- Reachability analysis for abstract unbounded-thread software models:
Our abstract unbounded-thread 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 explicit-state reachability techniques for such models. [TOPLAS 2014]
A project website can be found here.
Symbolic analysis for such (infinite-state) 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.
- Analyzing floating-point programs for lack of portability due to compiler and hardware dependencies:
The precise semantics of floating-point arithmetic programs depends on the execution platform, including the compiler and the target hardware. Platform dependencies are particularly pronounced for arithmetic-intensive 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 floating-point 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. [EURO-PAR 2015]
A project website can be found here.
- Deciding floating-point formulas via proxy theories:
We are working on an approach to reasoning about floating-point arithmetic (FPA) that reduces solving an FPA formula f to reasoning over a related but easier-to-solve proxy theory T, such as real arithmetic, or reduced-precision 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 T-agnostic: 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.
This is ongoing work.
Conference program or organizing committees:
- upcoming: CAV 2016, ICFEM 2016