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