Speaker: Francesco Alberti (University of Lugano)
Title: Array-based systems and parameterized verification
(Joint work with Natasha Sharygina, Roberto Bruttomesso,Silvio Ghilardi, Silvio Ranise)
Transition systems working with array variables,
called array-based systems, are suitable formal models
for different heterogeneous classes of real systems,
from protocols to algorithms handling unbounded data
structures. First-order theories are used in order to
specify indexes and elements of arrays handled by the system,
thus allowing a complete declarative specification of it.
Safety properties for these systems can be checked by
means of a backward reachability procedure built on the
top of SMT-solvers. Two of the main features of this
framework - called Model Checking Modulo Theories -
are (i) the capability of handling arrays in a natural way,
and (ii) the ability to check quantified forall assertions
for these systems.
In this talk we will show how protocols and imperative
programs working on arrays can be encoded in terms of
array-based systems, and present MCMT2, a model checker
used to automatically check safety properties of array
based systems. In the end, we will introduce an ongoing
work about an abstraction-refinement technique studied
to fight against the state space explosion that arise
during the verification of real industrial-size systems.
Speaker: Alexander Rabinovich (Tel Aviv University)
(Joint work with Mark Jenkins, Joel Ouaknine and James Worrell)
Title: The Church Synthesis Problem with metric
Church's Problem asks for the construction of a procedure which, given a
logical specification φ(I,O) between input strings I and output strings
O, determines whether there exists an operator F that implements the
specification in the sense that φ(I,F(I)) holds for all inputs I. Büchi
and Landweber gave a procedure to solve Church's problem for MSO
specifications and operators computable by finite-state automata.
We consider extensions of Church's problem in two orthogonal directions:
(i) we address the problem in a more general logical setting, where not
only the specifications but also the solutions are presented in a
logical system; (ii) we consider not only the canonical discrete time
domain of the natural numbers, but also the continuous domain of reals.
We show that for every fixed bounded length interval of the reals,
Church's problem is decidable when specifications and implementations
are described in the monadic second-order logics over the reals with
order and the +1 function.
Speaker: Adrian Francalanza (University of Malta)
Title: Distributed System Contract Monitoring
The use of behavioural contracts, to specify, regulate and
verify systems, is particularly relevant to runtime monitoring of
distributed systems. System distribution poses major challenges to
contract monitoring, from monitoring-induced information leaks to
computation load balancing, communication overheads and
fault-tolerance. We present MDPi, a location-aware process calculus,
for reasoning about monitoring of distributed systems. We define a
family of Labelled Transition Systems for this calculus, which allow
formal reasoning about different monitoring strategies at different
levels of abstractions. We also illustrate the expressivity of the
calculus by showing how contracts in a simple contract language can be
synthesised into different MDPi monitors.
Speaker: Silvia Ghilezan (University of Novi Sad)
Title: Resource control calculi
(Joint work with Jelen Ivetic, Pierre Lescanne and Silvia Likavec)
We introduce and discuss the resource control cube,
a system consisting of four resource control lambda calculi
and the four corresponding resource control sequent lambda
calculi, i.e., calculi aware of resource management.
This system is constructed by parametrizing over the set of
resources (weakening/erasure or contraction/duplication),
which enables a uniform treatment of eight different calculi
of the cube. The cube of simply typed resource lambda calculi
expands the Curry-Howard correspondence to intuitionistic
natural deduction and intuitionistic sequent logic with implicit
or explicit structural rules.
Speaker: Cesar Sanchez (IMDEA Madrid)
Title: Parametrized Invariance for Fully Symmetric Systems
We study the uniform verification problem, which consists of proving
that the parallel composition of an arbitrary number of processes
running the same program satisfies a temporal property. We introduce
the parametrized invariance rule, a temporal deductive proof rule that
reduces the uniform verification problem of safety properties to the
validity of a finite collection of verification conditions. The number
of verification conditions depends only on the size of the program
description and the number of free variables in the parametrized
temporal formula, but not on the number of parallel processes. The
parametrized invariance rule relies on the full symmetry assumption,
which covers a large class of concurrent systems, including concurrent
data-types. We illustrate the use of this technique on two
parametrized systems with infinite data: a ticket based
mutual-exclusion protocol, and a lock-coupling concurrent list.
Speaker: Maria Paola Bonacina (Universita` degli Studi di Verona)
Title: Towards interpolation in an SMT solver with integrated superposition
(Joint work with Moa Johansson)
An interpolant is a formula that lies between two formulae,
meaning that it implies one, is implied by the other, and is made
only of their shared symbols. Interpolation is the operation of
extracting interpolants from proofs of implications. Dually, if the
two formulae are inconsistent, a reverse interpolant is implied by
one and is inconsistent with the other, and interpolation extracts
interpolants from refutations. Interpolation has increasing applications
in program analysis and synthesis, including abstraction refinement
and invariant generation. We study interpolation for superposition,
which is relevant to superposition-based decision procedures,
and to the DPLL(Gamma+T) method, that integrates superposition
(Gamma) into a DPLL(T) based SMT-solver. We present a complete
interpolation system for ground superposition proofs, clarifying the
requirements for interpolation with equality and connecting those for
superposition with those for equality sharing. We discuss current work
on a complete interpolation system for general superposition proofs.
We define the proofs generated by DPLL(Gamma+T), and we show how the
modular structure of this prover allows us to get its interpolation
system from those for DPLL, equality sharing and superposition.
Speaker: Bernd Finkbeiner (Universitaet des Saarlandes)
Title: Reactive Safety
(Joint work with Ruediger Ehlers)
The distinction between safety and liveness properties is a
fundamental classification with immediate implications on the
feasibility and complexity of various monitoring, model checking, and
synthesis problems. We revisit the notion of safety for reactive
systems, i.e., for systems whose behavior is characterized by the
interplay of uncontrolled environment inputs and controlled system
outputs. We show that reactive safety is a strictly larger class of
properties than standard safety. We provide algorithms for checking if
a property, given as a temporal formula or as a word or tree
automaton, is a reactive safety property and for translating such
properties into safety automata. Based on this construction, the
standard verification and synthesis algorithms for safety properties
immediately extend to the larger class of reactive safety.
Speaker: Alessandro Cimatti (FBK, Trento)
Title: From Satisfiability to Verification Modulo Theories
The field of Satisfiability Modulo Theories (SMT) has greatly
benefited from the SMT-LIB and SMT-COMP initiatives: the definition of
a standard language supported the creation of a large collection of
benchmarks, and the competition fostered tremendous progress in the
performance of SMT solvers.
Many practical problems in verification arise from the analysis of the
transition systems that can be naturally represented in symbolic form
within the SMT framework (e.g. software, timed and hybrid systems,
word-level circuits, microcode).
However, the SMT initiative does not deal directly with the sequential
nature of the transition system, where reachability is defined by
unrolling of the transition relation. To draw an analogy with the pure
boolean case, SMT is the counterpart of SAT, but there is no "modulo
theory" counterpart for Model Checking. In fact, many problems in the
SMT-LIB are (bounded horizon) verification problems for such
In this talk I will argue in favour of a Verification Modulo Theory
(VMT) initiative. The aim is to define a language, a library of
benchmarks, and to set up a competition, for verification problems
resulting from transition systems described in SMT.
The VMT initiative, while leveraging the advances of SMT, will allow
to deal natively with issues resulting from the verification of
transition systems, hopefully resulting in a new generation of model
checkers modulo theory.
Speaker: Stefano Tonetta (FBK, Trento)
Title: VMT techniques
Satisfiability-modulo-theory is the problem of checking the
satisfiability of a logical formula with a background theory. Many
solvers have been optimized for different theories and enhanced with
advanced features such as incrementality, unsat cores, interpolation.
Meanwhile, many techniques have been conceived to verify properties of
transition systems exploiting the efficiency and features of SMT
solvers. In fact, by reducing a verification problem to a possibly
infinite series of SMT problems, infinite-state systems with reals,
integers, or other data types can be verified. This
"Verification-Modulo-Theory" (VMT) has been applied to different
applications such as software, timed and hybrid systems, and microcode.
In this talk, we overview some of these techniques including bounded
model checking, interpolation-based model checking, k-induction,
predicate abstraction, and combination thereof.
Speaker: Ruzica Piskac (EPFL)
Title: Synthesis of Code Snippets using Automated Reasoning
In this talk I will describe a method that applies theorem proving
technology to synthesize code fragments. To determine candidate code
fragments, our approach takes into account polymorphic type constraints
as well as test cases. Our tool interactively displays a ranked list of
suggested code fragments that are appropriate for the current program
point. It supports polymorphic type declarations and can synthesize
expressions containing methods with any number of arguments and any depth.
Our synthesis approach is based on techniques of theorem proving in
quantified intuitionistic logic extended with the support for weights.
Weights indicate preferences to certain formulas; they guide the search
and enable the ranking of solutions. We have found our system to be useful
for synthesizing code fragments for common programming tasks, and we
believe it is a good platform for exploring software synthesis techniques.
Speaker: Radu Iosif (VERIMAG)
Title: The Numerical Transition Systems Library
Numerical Transition Systems (NTS) are simple models of computation
involving infinite (or very large) data domains, such as integers or real
numbers. The Numerical Transition Language is a common language for
describing numerical transition systems, inspired by the input language
of several existing tools for the analysis of numerical transition systems,
such as: ARMC, FAST, FLATA and INTERPROC. The aim of NTL is not that of
replacing existing languages, but rather that of providing means of
interoperability between tools developed by different groups, and based
on different principles. The language has a clearly defined semantics
(based on first-order logic) and supports (multi-dimensional) array data
types, recursive procedures and parallelism.
In this talk we present the main features of NTL and report on the
implementation of a support library for the language. The library consists
of a collection abstract syntax tree classes, a general purpose parser,
and pretty-printing routines. In parallel with the development of the
library, we are building a C front-end for NTL and a tool for the
verification of safety and termination properties for inter-procedural models.