International Workshop on Symbolic and Numerical Methods for Reachability Analysis
(SNR 2015)

SNR 2015: 1st
International Workshop on Symbolic and Numerical Methods for
Reachability Analysis 2015 in San Francisco, California, USA
Image source:


Hybrid systems model complex dynamical systems that combine discrete and con- tinuous components. Reachability questions, regarding whether a system can run into certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems.

Successful reachability analysis methods for hybrid systems requires the unification of techniques from at least two traditions:

  • Symbolic methods that operate on exact and discrete representations of systems, in the form of various model checking and theorem proving algorithms,
  • Numerical methods that operate on various forms of numerical approximations and continuous transformations of the systems, as developed in the area of continuous dynamical systems and control theory.

As concrete examples, one can observe how the two types of techniques interact in the existing approaches towards reachability analysis. Reachable set computation methods explicitly construct flow-pipes that overapproximate the reachable states over time, while efficient computation of such overapproximations requires symbolic representations such as support functions. Constraint solving methods symbolically encode reachability properties as logic formulas, while solving such formulas requires numerically-driven decision procedures. A goal of the workshop is to seek further synergies among these approaches.

Back to Top


The SNR workshop solicits papers broadly in the area of verification and synthesis of continuous and hybrid systems. One of the aims is to catalyze work on the interface of symbolic and numerical methods for the reachability analysis. The scope of the workshop includes, but is not restricted to, the following topics:

  • Flow-pipe construction
  • Representation of symbolic regions within reachability algorithm
  • Abstraction techniques for hybrid systems and numerical programs
  • Trajectory generation from symbolic paths
  • Decision procedures over real numbers
  • Reliable integration
  • Logics to reason about hybrid systems
  • Reachability analysis for planning and synthesis
  • Domain specific approaches in biology, robotics, etc

Back to Top

Call for Papers

Call for papers can be found here.

Back to Top

Program (July 19)

Session 1 (8:30-10:00)

  • Ian M. Mitchell. Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels
  • Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo. Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis
  • Yang Gao and Martin Fränzle. Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain
  • Fedor Shmarov and Paolo Zuliani. ProbReach: A Tool for Guaranteed Reachability Analysis of Stochastic Hybrid Systems

Coffee-break (10:00-10:30)

Session 2 (10:30-12:00)

  • Invited talk: Sriram Sankaranarayanan (University of Colorado Boulder, USA). Symbolic-Numeric Reachability Analysis of Hybrid Systems
  • Stanley Bak, Sergiy Bogomolov and Taylor T Johnson. HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models
  • Pavithra Prabhakar and Miriam García Soto. An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary

Back to Top

Important Dates

Paper submission April 24, 2015;Extended to May 8, 2015
Author notification May 31, 2015
Camery-ready version June 15, 2015
Workshop July 19, 2015

Back to Top

Program Committee

Matthias Althoff (TUM, Germany) Sergiy Bogomolov (IST Austria, Austria) - co-chair
Parasara Sridhar Duggirala (University of Illinois at Urbana Champaign, USA) Martin Fränzle (University of Oldenburg, Germany)
Goran Frehse (Verimag, France) Sicun Gao (Massachusetts Institute of Technology, USA)
Daniele Magazzeni (King’s College, UK) Sayan Mitra (University of Illinois at Urbana Champaign, USA)
Erion Plaku (CUA, USA) Stefan Ratschan (Academy of Sciences, Czech Republic)
Ashish Tiwari (SRI, USA) - co-chair Stavros Tripakis (Aalto University, Finnland)
Paolo Zuliani (University of Newcastle, UK)

Back to Top