College of Computer and Information Science
Northeastern University
360 Huntington Avenue
Boston, Massachusetts 02115

Office: 202 West Village H, room 344
Phone: ++1-617-373-3100
Email: wahl–ät–ccs.neu.edu
                                      Thomas Wahl                   
Northeastern University

NEWS: (as of late summer 2017)




Brief bio:

  • 2011–present: Full-time 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
  • 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



Current projects:

  • Parameter-aware 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:
    1. the number of physical components of a certain functional type,
    2. the number of clients that simultaneously request a service from a server,
    3. the capacity of the communication channel between components,
    4. the number of context switches permitted among concurrent processes,
    5. 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 k0, i.e. whether it stops increasing after reaching k0. 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 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.

    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 "left-to-right", and to ignore any preision or efficiency optimization features, such as contracted operations, special floating-point 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 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. [FMCAD 2016]

  • 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.



Research sponsors:

National Science
                                      Foundation Draper Labs



Conference program or organizing committees:




Awards:


Design borrowed in part from Domagoj Babic