Programme‎ > ‎

Talks


Speaker: Francesco Alberti (University of Lugano)
Title: Array-based systems and parameterized verification
(Joint work with Natasha Sharygina, Roberto Bruttomesso,Silvio Ghilardi, Silvio Ranise)

Abstract: 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

Abstract: 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

Abstract: 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)

Abstract: 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

Abstract: 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)

Abstract: 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)

Abstract: 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

Abstract: 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 transition systems. 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

Abstract: 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

Abstract: 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

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