Invited speakers

  • Stéphane Demri (LSV, CNRS & ENS de Cachan), joint with Tableaux 2013
    Witness Runs for Counter Machines
    Decision problems for counter systems are ubiquitous in formal verification. Even though, most verification problems are known to be undecidable, a lot of efforts have been put to define decidable subclasses by considering interesting restrictions. Algorithms are usually based on properties of the control graphs and on the constraints for counter values. In this talk, we present a selection of recent developments on the verification of counter systems that take advantage of decision procedures for (fragments of) Presburger arithmetic. The properties specified on counter systems span from reachability to temporal properties.
  • Konstantin Korovin (The University of Manchester)
    From resolution and DPLL to solving arithmetic constraints
    Reasoning methods based on resolution and DPLL have enjoyed many success stories in real-life applications. One of the challenges is whether we can go beyond and extend this technology to other domains such as arithmetic. In our recent work we introduced two methods for solving systems of linear inequalities called conflict resolution (CR) and bound propagation (BP) which aim to address this challenge. In particular, conflict resolution can be seen as a refinement of resolution and bound propagation is analogous to DPLL with constraint propagation, backjumping and lemma learning. There are non-trivial issues when considering arithmetic constraints such as termination, dynamic variable ordering and dealing with large coefficients. In this talk I will overview our approach and related work. This is a joint work with Ioan Dragan, Laura Kovacs, Nestan Tsiskaridze and Andrei Voronkov.
  • Joel Ouaknine (Oxford University)
    Specification and Verification of Linear Dynamical Systems: Advances and Challenges
    Dynamical systems are mathematical models in which the state of a system at any point in time is represented by a vector of variables, with a fixed rule determining the evolution of these variables over time. Continuous linear dynamical systems are governed by a multivariate linear differential equation, whereas discrete-time linear dynamical systems are governed by a linear transformation. In both cases, given initial values for the variables, the rule uniquely determines the evolution of the system over time.
    Particular instances of such systems have been studied for decades in various areas of science and engineering, often either through simulations or in terms of long-run behaviour: existence and uniqueness of attractors, fixed points, or periodic points, sensitivity to initial conditions, etc. From the point of view of computer science, it is somewhat surprising to note the relative scarcity of literature on decision problems concerning linear dynamical systems, e.g., whether a fixed point or a particular region will actually be reached in finite time, whether a variable will assume negative values infinitely often, etc. Such questions, in turn, have numerous applications in a wide array of scientific areas, such as theoretical biology (analysis of L-systems, population dynamics), microeconomics (stability of supply-and-demand equilibria in cyclical markets), software verification (termination of linear programs), probabilistic model checking (reachability and approximation in Markov chains, stochastic logics), quantum computing (threshold problems for quantum automata), as well as combinatorics, formal languages, statistical physics, etc.
    In this talk, I will describe recent advances in decision problems for linear dynamical systems, and discuss various open problems, both algorithmic in nature and in terms of defining suitable — i.e., expressive as well as tractable, or at least decidable — formalisms and frameworks for formulating requirements on linear dynamical systems.
  • Lawrence C. Paulson (University of Cambridge)
    MetiTarski's Menagerie of Cooperating Systems
    MetiTarski, an automatic theorem prover for real-valued special functions, is briefly introduced. Its architecture is sketched, with a focus on arithmetic reasoning systems that it invokes. Finally, the presentation describes some applications where MetiTarski is itself invoked by other tools.