ABSTRACT. Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce in this paper a novel and declarative way to specify privacy goals, called `privacy', and relate it to static equivalence. This new approach is based on specifying two formulae E1 and E2 in first-order logic with Herbrand universes, where E1 reflects the intentionally released information and E2 includes the actual cryptographic (`technical') messages the intruder can see.

Then E1-E2 privacy means that the intruder cannot derive any `non-technical' statement from E2 that he cannot derive from E1 already. We describe by a variety of examples how this notion can be used in practice. Even though E1-E2 privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and obtain partial tool support for E1-E2 privacy.

Joint work with Sebastian Moedersheim and Thomas Gross

ABSTRACT. Modern SAT solvers are applied in many academic and industrial fields. The used CDCL algorithm is based on resolution, but solvers also use stronger reasoning techniques in preprocessing steps. Only few attempts have been made to include stronger reasoning techniques into the search itself. The current work revisits the embedding of extended resolution into SAT solvers, and improves existing work. Experiments indicate that the approach is very promising.

ABSTRACT. We describe a hybrid system based framework for modeling gene regulation and other biomolecular networks and a method for analysis of the dynamic behavior of such models. A particular feature of the proposed framework is the focus on qualitative experimentally testable properties of the system. With this goal in mind we introduce the notion of the frame of a hybrid system, which allows for the discretisation of the state space of the network. We propose two different methods for the analysis of this state space. The result of the analysis is a set of attractors (generalizations of attractors used in Boolean models) that characterise the underlying biological system.

Whilst in the general case the problem of finding attractors in the state space is algorithmically undecidable, we demonstrate that our methods work for comparatively complex gene regulatory network model of lambda-phage. For this model we are able to identify attractors corresponding to two known biological behaviors of lambda-phage: lysis and lysogeny and also to show that there are no other stable behavior regions in state space of lambda-phage model.

ABSTRACT.  Datalog+/?  is a family of languages for knowledge representation and reasoning. These languages extend Datalog with features such as existential quantifiers, equalities, and the falsum in rule heads, and, at the same time, applies restrictions to achieve decidability and tractability. After a general overview of the Datalog+/?  family, this talk will focus on more recent issues. Among other things, I will report on the combination of the two main decidability paradigms guardedness and stickiness, yielding the Tame Fragment, and on incorporating non-monotonic negation and disjunction into Datalog+/–: . I will also report about a special version of Datalog+/?  suitable for reasoning with reverse-engineered UML class diagrams, and about the TriQ language that expresses SPARQL with entailment regimes.

ABSTRACT. Automatic device driver synthesis is one of the first real-world applications of the reactive synthesis technology to date. This talk will give an overview of an ongoing three-year project funded by Intel, aiming to develop a suite of practical device driver synthesis tools. The project is pursued jointly by researchers from the University of Toronto, University of Colorado Boulder, Imperial College London, NICTA, and IST Austria. The talk will present the key contributions made by the project so far, as well as the main remaining challenges. In particular, I will describe the first practical abstraction-refinement algorithm for games and a user-guided synthesis methodology, which combines the power of automation with the flexibility of conventional development. I will give a demo of our synthesis tool, showing its support for interactive code generation and efficient troubleshooting of synthesis failures using counterexample-guided debugging.

ABSTRACT. Consistent shareable data services supporting atomic (linearizable) objects provide convenient building blocks for dynamic distributed systems. In general it is notoriously challenging to combine provable correctness guarantees with efficiency in distributed systems subject to perturbations in the computing medium. We overview our work on specification and implementation of distributed system services. Then we focus on a general framework for dynamic consistent data services that can be tailored to yield implementations for various target network settings and that incorporates on-the-fly reconfiguration that only modestly interferes with on-going operations. Here the goal is to guarantee safety (atomicity) for arbitrary patterns of asynchrony, crashes, and message loss, while enabling practical implementations.  We describe examples of specification, rigorous reasoning about correctness, provable optimizations, and methodical implementations of consistent data services in distributed systems.

ABSTRACT. Logic programs with ordered disjunction (LPODs) \cite{Brewka02} generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including Game Theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to represent the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally reflects the reasoning procedure of LPODs. We show that under finite structures, every LPOD can be translated into a first-order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.

ABSTRACT. Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming. An important characteristic of the new paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we enhance extensional higher-order logic programming with constructive negation. We argue that the main ideas underlying constructive negation are quite close to the existing proof procedure for extensional higher-order logic programming and for this reason the two notions amalgamate quite conveniently. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas. In this way we obtain the first (to our knowledge) higher-order logic programming language supporting constructive negation and offering a new style of programming that genuinely extends that of traditional logic programming.

ABSTRACT. In the past, there have several attempts to explain logic programming under the well-founded semantics as a logic of inductive definitions. A weakness in all is the absence of an obvious connection between how we understand various types of informal inductive definitions in mathematical texts and the complex mathematics of the well-founded semantics. In this paper, we close this gap and show in a more definitive way that indeed, the well-founded semantics is a formalization of the principle of inductive definition.

ABSTRACT. Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original definition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defining the semantics of gringo programs by translating them into the language of infinitary propositional formulas. This semantics allows us to study equivalent transformations of gringo programs using natural deduction in infinitary propositional logic, so that the properties of these programs can be more precisely characterized. In this way, we aim to create a foundation on which important issues such as the correctness of gringo programs and optimization methods may be more formally studied.

ABSTRACT. We introduce dynamic causal calculus, a nonmonotonic formalism that can be viewed as a direct logical counterpart of the action description language C+ from \cite{GLMT01}. We formulate a nonmonotonic semantics of the associated causal language, and compare this semantics with the indirect, two-stage semantics for C+, given in \cite{GLMT01}. It will be shown, in particular, that the suggested semantics allows us to alleviate syntactic distinctions between propositional atoms, maintained by C+, as well as type restrictions imposed on its causal laws. We will describe also a logical formalism of dynamic causal inference that constitutes a complete description of the logic that is adequate for this dynamic calculus.

ABSTRACT. Causal models defined in terms structural equations have proved to be quite a powerful way of representing knowledge regarding causality. However, a number of authors have designed examples where it seems that the Halpern-Pearl (HP) definition of causality gives intuitively unreasonable answers. As has been pointed out by many authors, what gets counted as a cause is quite dependent on the choice of variables in the model. Here it is shown that in all the counterexamples suggested, there are two possible stories consistent with the counterexample, where intuitions regarding causality are quite different. By adding additional variables, we can disambiguate the stories; moreover, in the resulting causal models, the HP definition of causality gives the intuitively correct answer. The examples not only give insight into the modeling process, they also highlight some aspects of the definition of causality itself. Specifically, by extending one of the examples, it can be shown that a modification to the original HP definition made to deal with an example by Hopkins and Pearl may not be necessary. By extending another definition, a sequence of models can be constructed, each one a conservative extension of the one before, where the question of whether X=x is cause of Y=y alternates between being true and false.

ABSTRACT. We provide a sound and complete axiomatization for a class of logics appropriate for reasoning about the rationality of players in games. Essentially the same axiomatization applies to a wide class of decision rules.

ABSTRACT. We show that determining whether a Boolean game has an equilibrium that guarantees every player a given payoff is NEXP-hard. In the proof we encode a non-deterministic, exponential time Turing machine by having one player play a mixed strategy from which we can infer a computation history of the machine, and the other players verify that this history does in fact represent a valid, accepting run.

ABSTRACT. We revisit the AMBA AHB case study that has been a benchmark for reactive synthesis tools for a long time. Synthesizing AMBA AHB implementations that can serve a large number of masters is still a difficult problem. We demonstrate how to use parameterized synthesis in token rings to obtain an implementation for a component that serves a single master, and can be arranged in a ring of arbitrarily many components. We describe new tricks -- property decompositional synthesis, and direct encoding of simple GR1 -- that together with previously described optimizations allowed us to synthesize the model with 14 states in 1 hour.

ABSTRACT. Counterexample-guided inductive synthesis (CEGIS) is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the correct program if the space of candidate programs is finite. But the technique may or may not terminate with the correct program if the candidate space of programs is infinite. In this paper, we perform a theoretical analysis of counterexample-guided inductive synthesis technique. We investigate whether the set of candidate spaces for which the correct program can be synthesized using CEGIS depends on the counterexamples used in inductive synthesis, that is, whether there are good mistakes which would increase the synthesis power. We investigate whether the use of minimal counterexamples instead of arbitrary counterexamples expands the set of candidate spaces of programs for which inductive synthesis can successfully synthesize a correct program. We consider two kinds of counterexamples: minimal counterexamples and history bounded counterexamples. The history bounded counterexample used in any iteration of CEGIS is bounded by the examples used in previous iterations of inductive synthesis. We examine the relative change in power of inductive synthesis in both cases. We show that the synthesis technique using minimal counterexamples MinCEGIS has the same synthesis power as CEGIS but the synthesis technique using history bounded counterexamples HCEGIS has different power than that of CEGIS.

ABSTRACT. We introduce Petri games as a new foundation for the synthesis of distributed systems. The players of a Petri game consist of the system processes and the external environment, all represented as tokens on a Petri net. The players memorize their causal history and communicate it to each other during each synchronization. Petri games lead to new decidability results and algorithms for the synthesis of distributed systems. Joint work with Ernst-Ruediger Olderog.

ABSTRACT. Reformulating Artificial Intelligence Planning problems as Constraint Satisfaction Problems(CSPs) brings a number of benefits. In this reformulation process however, the structure of the original planning problem is lost. Therefore, no planning problem specific guidance may be used during the assignment of values to the CSP variables. Extending work, in which we implemented a planning-specific CSP variable and value selection heuristic, the work described here aims to make better use of the propagation inherent in a given CSP solver by using CSP meta variables. Such meta variables are used here for goal-locking and for the assignment of resources to tasks within the problem solution process, with the aim being to reduce the search space, and to better guide the search within it.

ABSTRACT. Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are discussed for different applications like argumentation theory, legal reasoning and actions in multi-agent systems. Recently there also is growing interest in modelling human reasoning and testing the models with psychological findings. Deontic logic is an obvious tool to this end, because norms and licenses in human societies can be described easily. This paper concentrates on automated reasoning in deontic logic. We show that deontic logic can be translated into the description logic ALC, for which the first oder reasoning system Hyper offers a decision procedure.

ABSTRACT. Current and future robotics and autonomous system applications will be used in highly complex environments. In such situations, automatic reconfiguration, due either to changing requirements or equipment failure, is highly desirable. By using a model of autonomy based around the Robot Operating System (ROS), and building on previous work, it is possible to use Artificial Intelligence (AI) Planning to facilitate the automatic reconfiguration. In this way, standard AI Planning machinery may be used with a suitable mathematical model of a given system. This paper reviews the background to this concept and details the initial steps taken towards the combination of AI Planning technology and a physical system, with the aim being to have the planner provide possible validated system reconfigurations which can then be implemented on the hardware.

ABSTRACT. For a given formula, a definiens in terms of a given set of predicates can be characterized quite straightforwardly with predicate quantification. Methods for second-order quantifier elimination and the closely related computation of forgetting, projection and uniform interpolants can then be applied to compute such definientia. Here we address the question, whether also definientia that are in given classes of formulas, such as Horn formulas, conjunctions of atoms or Krom formulas, can be specified with predicate quantification and can thus be computed by second-order quantifier elimination methods.

ABSTRACT. The talk is devoted to Herbrand-type theorems for an enough wide spectrum of first-order logics for both the classical and intuitionistic cases as well as for their modal extensions. A way for the construction of Herbrand theorems for first-order logics containing the ineliminable cut rule is discussed.

ABSTRACT. Synaptic plasticity depends on the interaction between electrical activity in neurons and the synaptic proteome, the collection of over 1000 proteins in the post-synaptic density (PSD) of synapses. To construct models of synaptic plasticity with realistic numbers of proteins, we aim to combine rule-based models of molecular interactions in the synaptic proteome with compartmental models of the electrical activity of neurons. Rule-based systems allow interactions between the combinatorially large number of protein complexes in the postsynaptic proteome to be expressed straightforwardly, and simulations of rule-based systems are stochastic and thus can deal with the small copy numbers of proteins and complexes in the PSD. Compartmental models of neurons are expressed as systems of coupled ordinary differential equations and solved deterministically. We present an algorithm which incorporates stochastic rule-based models into deterministic compartmental models and demonstrate an implementation of this hybrid system using the SpatialKappa and NEURON simulators.

ABSTRACT. Wet-lab experiments, in which the dynamics within living cells are observed, are usually costly and time consuming. This is particularly true if single-cell measurements are obtained using experimental techniques such as flow-cytometry or fluorescence microscopy. It is therefore important to optimize experimentswith respect to the information they provide about the system. In this paper we make a priori predictions of the amount of information that can be obtained from measurements. We focus on the case where the measurements are made to estimate parameters of a stochastic model of the underlying biochemical reactions. We propose a numerical scheme to approximate the Fisher information of future experiments at different observation time points and determine optimal observation time points. To illustrate the usefulness of our approach, we apply our method to two interesting case studies.

ABSTRACT. Reachability analysis has recently proved to be a useful technique for analyzing the behaviors of under-specified biological models. In this paper, we propose a method exploiting the eigenstructure of a linear continuous system to efficiently estimate a bound on the time the system can reach a target set from an initial set. This estimation can be then directly integrated in an existing algorithm for hybrid systems with linear continuous dynamics, to speed up reachability computations. Furthermore, it can also be used to improve time-efficiency of the hybridization technique that is based on a piecewise-linear approximation of non-linear continuous dynamics. The proposed method is illustrated on a number of examples including a biological model.

ABSTRACT. ...

ABSTRACT. Efficient and scalable concurrent data-structures are key to high-performance multicore systems. Algorithms such as stacks and queues are widely used to handle synchronisation and distribute work between cores. We present the TS stack, a new concurrent stack implementation which allows elements to remain unordered in the stack if they were pushed concurrently. We use a new proof technique to show the correctness of the TS stack according to linearizability as the common linearization point technique cannot be applied.

ABSTRACT. We show how correct, analyzable distributed programs can be implemented in Scala using our framework, FooPar. Both performance and correctness proofs can be modularized in terms of the distributed data structures and functions available in the framework. We go on to show how we can further the connection between the correctness proofs and implementation using specification testing.

ABSTRACT. Software-defined networks (SDNs) is a new type computer networks where data planes and control planes are separated from each other and a centralized controller manages a distributed set of switches. A set of commands for packet forwarding and flow-table updating was defined in the form of a protocol known as OpenFlow. SDNs can both simplify existing network applications and serve as a platform for developing new ones. The main advantage of this network architecture is that programmers are able to control the behaviour of the whole network by configuring appropriately the packet forwarding rules installed on the switches. Nevertheless, correct and safe management of SDNs is not an easy task. Every time the current load of flow tables should satisfy certain requirements: some packets have to reach their destination, although some other packets have to be dropped, certain switches are forbidden for some packets, whereas some other switches have to be obligatorily traversed. These and some other requirements constitute a Packet Forwarding Policies (PFPs). One of the aims of network engineering is to provide such a loading of switches with forwarding rules as to guarantee compliance with the PFP. The solution is to develop a toolset which could be able 1) to check correctness of a separate application operating on the controller w.r.t. a specified forwarding policy, 2) to check consistency of forwarding policies implemented by various applications, and 3) to monitor and check correctness and safety of the entire SDN. In an attempt to produce such a toolset we developed 1) a combined (relational and automata based) formal model which captures the most essential features of SDN behavior, 2) a multi-level formal language for specification of SDN forwarding policies which uses transitive closure operator to specify reachability properties of packet forwarding relation and temporal operators to specify behaviour of SDN as a whole, and 3) a BDD-based model-checking techniques for verification of SDN models against PFP specifications.

ABSTRACT. The use of preferences in query answering, both in traditional databases and in ontology-based data access, has recently received much attention, due to its many real-world applications. In this paper, we tackle the problem of query answering in Datalog+/– ontologies subject to the querying user’s preferences and a collection of subjective reports (i.e., scores for a list of features) of other users, who have their own preferences as well. All these pieces of information are combined to rank the query results. We first focus on the problem of ranking atoms in a database by leveraging reports and customizing their content according to the user’s preferences. Then, we extend this approach to deal with ontological query answering using provenance information. Though the general problem is shown to have an exponential-time data complexity upper bound, we propose a special case that has polynomial time data complexity.

ABSTRACT. Dealing with uncertainty is a very important issue in description logics (DLs). In this paper, we present PrDL-Lite N bool a new probabilistic extension of DL-Lite N bool by supporting the belief interval in a single axiom or a set of axioms connected with conjunction (by ∧) or disjunction (by ∨) operators. The PrDL-Lite N bool semantics is based on DL-Lite N bool features which are a new alternative semantics for DL-Lite N bool having a finite structure and the number of them is always finite unlike classical models. PrDL-Lite N bool supports terminological and assertional probabilistic knowledge and the reasoning  tasks: satisfiability, deciding the probabilistic axiom entailment and computing tight interval for entailment are achieved by solving linear constraints system. A prototype of the approach is implemented using OWLAPI for knowledge base creation, Pellet for reasoning and LpSolve for solving the linear programs.

ABSTRACT. In a relational setting, the maximum entropy model of a set of probabilistic conditionals can be defined referring to the full set of ground instances of the conditionals. The logic FO-PCL uses the notion of parametric uniformity to ensure that the full grounding of the conditionals can be avoided, thereby greatly simplifying the maximum entropy model computation. In this paper, we describe a system that realises an approach transforming an FO-PCL knowledge base consisting of relational probabilistic conditionals into a knowledge base having the same maximum entropy model that is parametrically uniform. The implemented system provides different execution and evaluation modes, including the generation of all possible solutions, and is available within an integrated development environment for relational probabilistic logic.

ABSTRACT. Terminating procedures for the generation of models minimal modulo subset-simulation for normal modal logics have recently been presented. In this abstract we explain what are the challenges to generalise those procedures to more expressive modal logics, and discuss possible solutions.

ABSTRACT. We present a prototype tool for automated reasoning for multimodal normal logics where combinations of the axioms K, T, D, B, 4, and 5 hold. The theorem prover is based on previous work on resolution calculi for such logics. We briefly present the syntax, the semantics, and the calculus for the basic normal logic together with the inference rules for dealing with each specific axiom. We then give details of the implementation of the prover and discuss future work.

ABSTRACT. Uniform interpolation is a technique to restrict the concept and roles symbols used in an ontology to a specified subset, while preserving all logical entailments that can be expressed using that subset. We propose the notion of relative uniform interpolation, where knowledge from a second ontology is taken into account, and present a method for the description logic ALCH. Relative uniform interpolation of ontologies corresponds to strongest necessary conditions of formulae studied in classical logics.

ABSTRACT. We present a novel approach to the automated design of large scale biological systems. Our model connects multiple levels of cellular organisation through a hybrid continuous/discrete and deterministic/stochastic approach. At the core of our model, a hybrid dynamical system represents interactions between gene expression and DNA topology. Gene expression then influences the metabolic level of the cell by affecting the flux distribution in a genome-scale metabolic model of {\it Escherichia coli}. We implement a Bayesian optimisation strategy to select optimal parameters which maximally satisfy a temporal logic formula specifying the desired behaviour of the system. Finally, we show preliminary results of a study on the interaction of the master regulator FIS with supercoiling.

ABSTRACT. We present RKappa, a framework for the development and analysis of rule-base models within a mature statistically empowered R environment. The infrastructure allows model editing, modification, parameter sampling, simulation, statistical analysis and visualisation without leaving the R environment. We demonstrate its effectiveness through its application to Global Sensitivity Analysis, exploring it in “parallel” and “concurrent” implementations. The pipeline was designed for high- performance computing platforms and aims to facilitate analysis the behaviour of the large-scale systems with limited knowledge of exact mechanisms and respectively sparse availability of parameter values, which we illustrate here with two biological model examples. Package is available on github: https://github.com/lptolik/R4Kappa

ABSTRACT. In this talk I argue that progress in Biology requires, among other things, a more modern approach to modeling and analysis of dynamical models. Such models should not be  restricted to classical dynamical systems but also involve concepts and ideas from discrete-event dynamical systems (automata) and hybrid (discrete-continuous) systems. I will present some recent techniques for exploring the dynamics of under-determined systems, that is, systems that admit uncertainty in initial conditions, parameters and  environmental conditions. These techniques, inspired by formal verification, can be used to assess the robustness of proposed models and increase our confidence in their plausibility.

ABSTRACT. Fault-tolerant distributed algorithms are central to ensuring reliability and availability of many on-line services that we use on a daily basis. However, they are difficult to build correctly. On top of the usual implementation challenges, one has to consider non-determinism in the scheduling of the participants and faults such as machine failures, and dropped messages. Using round models as a layer of abstraction simplify the design of such systems. Rounds are communication-closed and have a deterministic schedule. From a theoretical perspective, those models are justified by partial synchrony assumptions and simulation relations that map non-determinism to faults. From a practical perspective, many asynchronous algorithms are structured around logical rounds. For instance, in the Paxos algorithm, a replica becomes a leader in the first round and proposes its value during the second round. However, rounds are an abstraction and real systems are asynchronous. Therefore, such models are popular in theoretical publications, but less so in system ones. This talk will describe ongoing efforts in the automated verification of round-based algorithms and the synthesis of asynchronous implementations from round-based descriptions.

ABSTRACT. Recent advances in Distributed Computing highlights models and algorithms for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithm and correctness proofs.

This paper is the first to propose a formal framework to automatically design distributed algorithms that are dedicated to autonomous mobile robots evolving in a discrete space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. Our contribution is threefold. First, we propose an encoding of the gathering problem as a reachability game. Then, we automatically generate an optimal distributed algorithm for three robots evolving on a fixed size uniform ring. Finally, we prove by induction that the generated algorithm is also correct for any ring size except when an impossibility result holds (that is, when the number of robots divides the ring size).

ABSTRACT. I propose a framework for the automatic verification of autonomous mobile agents (robot protocols), moving on unknown finite graphs. The framework reduces the parameterised verification problem (i.e., does a given set of robots solve a given task on all graphs from a given infinite set of graphs) to questions in automata theory and monadic second order logic. I will provide some preliminary results, discuss the limitations of this approach, and suggest future research directions.

ABSTRACT. In this paper, we describe a synthesis algorithm for safety specifications described as circuits. Our algorithm is based on fixpoint computations, abstraction and refinement, it uses binary decision diagrams as symbolic data structure. We evaluate our tool on the benchmarks provided by the organizers of the synthesis competition organized within the SYNT’14 workshop.

ABSTRACT. In reactive synthesis, we automatically construct implementations for reactive systems from their specifications. To make the approach feasible in practice, a system engineer needs to have effective and efficient means to debug a specification.

In this paper, we provide techniques for report-based specification debugging, where a specification's properties are analyzed and the result is presented to the user as report. This provides a low-effort way to debug specifications and complements simulating a synthesized implementation as a more high-effort technique. We show the usefulness of our report-based specification debugging tool set by providing examples in the context of generalized reactivity(1) synthesis.

ABSTRACT. We report on the recently started Leo-III project, in which we design and implement a state-of-the-art Higher-Order Logic Theorem Prover, the successor of the well known LEO-II prover. Leo-III will be based on ordered paramodulation/superposition. In constrast to LEO-II, we replace the internal term representation (the commonly used simply typed lambda calculus) by a more expressive system supporting type polymorphism. In the course of the project, we plan to further enhance the type system with type classes and type constructors similar to System F ω . In order to achieve a substantial performance speed-up, the architecture of Leo-III will be based on massive parallelism (e.g. And/Or-Parallelism, Multisearch). The current design is a multi-agent blackboard archi- tecture that will allow to independently run agents with our proof calculus as well as agents for external (specialized) provers. Leo-III will focus right from the start on compatibility to the widely used TPTP infrastructure . Moreover, it will offer built-in support for specialized external prover agents and provide external interfaces to interactive provers such as Isabelle/HOL . The implementation will excessively use term sharing and several indexing techniques . Leo-III will also offer special support for reasoning in various quantified non-classical logics by exploiting a semantic embedding approach.

ABSTRACT. This paper presents a calculus of Socratic proofs for Propositional Linear-Time Logic (PLTL) and discuss potential automation of its proof search.

ABSTRACT. We provide a mathematical model for unbounded parallel compositions of structurally similar linear hybrid automata, whose topology and flows are described using parametrized formulas. We study how the analysis of safety properties for the overall system can be performed hierarchically, using quantifier elimination to derive conditions on the parameters of individual components.

ABSTRACT. In this talk, I will present our recent work on the synthesis of self-stabilizing, Byzantine fault-tolerant distributed algorithms for the synchronous counting problem.

We have examined two types of SAT solver-based techniques for synthesis. In the first approach, we have encoded the search problems into CNF SAT instances. This allows us to use highly-optimized, off-the-shelf SAT solvers. The second approach is inspired by CEGAR-style bounded model checking techniques. We have developed a search algorithm based on incremental SAT solving using assumptions on top of MiniSAT.

Both techniques have yielded novel algorithms for the synchronous counting problem. During the talk, I will present these results, discuss the trade-offs between the techniques for synthesis, and highlight open problems for future research.

This is joint work with Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Ulrich Schmid, Jukka Suomela and Siert Wieringa.

ABSTRACT. The implementation of distributed algorithms is error-prone, and manually constructed programs may not be optimal with respect to desired properties like size or stabilisation time. We propose to use computational methods to synthesise distributed algorithms from formal specifications, with guaranteed correctness and optimality. We present novel synthesis approaches for two general classes of specifications, and show that they are complete for realisable specifications and guaranteed to terminate for given bounds on certain parameters of the desired implementation. The resulting system components are correct by construction for distributed systems of arbitrary size, and have strong failure-resilience properties.

ABSTRACT. We present our work on the synthesis of finite-state component implementations for concurrent systems with a parametric number of components. We show how the parameterized synthesis problem can be reduced to a synthesis problem for a fixed number of components, using cutoff results from parameterized model checking. To make the approach practical for synthesis, we both extend the existing cutoff results, and optimize the synthesis method for the class of systems and specifications under consideration. With this approach, we have recently solved a parameterized version of a well-known industrial case study for the first time: we synthesize a component implementation for a (simplified) AMBA bus controller, such that copies of this component can be composed to obtain correct controllers for an arbitrary number of clients.