View: session overviewtalk overview
08:45  Presentation of Three Neat Tricks in Coq 8.5 SPEAKER: Jason Gross ABSTRACT. Coq 8.5 has a number of new features. It has more powerful universe polymorphism support. It allows tactics to be run at interpretation to construct other terms. The ability to switch from Gallina to Ltac in arbitrary locations nicely complements the constr: notation permitting the switch from Ltac to Gallina in tactics, and opens up many new possibilities. I propose to present three tricks involving these new features: tactics in terms allows the construction of tactics that recurse under binders; tactics in terms together with typeclasses allows overloading notations based on the type of their arguments; and there is a way to talk about universe levels explicitly, helped along by tactics in terms. 
09:15  Towards a betterbehaved unification algorithm for Coq SPEAKER: Beta Ziliani ABSTRACT. The unification algorithm is at the heart of a proof assistant like Coq. In particular, it is a key component in the refiner (the algorithm who has to fill implicit terms and missing type annotations), and the application of lemmas. Despite of being so important, however, the current unification algorithm of Coq is not properly documented, and implements certain heuristics that makes unification hard to understand and unpredictable. In this talk we are going to present a new unification algorithm, built from scratch, which focuses on it being simple, easy to understand, sound, and configurable to adapt to the different needs. 
09:45  Proofrelevant rewriting strategies in Coq SPEAKER: Matthieu Sozeau ABSTRACT. We introduce various enhancements of the generalized rewriting system of Coq. First, we show how the framework can be lifted to proofrelevant relations using the newly introduced universe polymorphic definitions in Coq. Second, we introduce rewriting strategies as a monadic combinator library on top of this framework, ressembling the LogicT monad for proofsearch (i.e., with backtracking, wellbehaved choice and composition). These new features combine to provide a general tool for finetuned automated rewriting applicable not only to propositional relations but also general computational typevalued relations. Last, we will also present an idea to handle dependent rewriting, e.g. the ability to rewrite in the domain of a dependent product and get corresponding transportation obligations. 
08:45  How do we get inductive invariants? (Part A) SPEAKER: David Monniaux ABSTRACT. Verifying the correctness of loopfree programs (or of general programs, up to bounded depth) is difficult: the state space explodes exponentially as the depth increases. Yet, the difficulty increases as we allow unboundedly many execution steps; proof approaches then generally rely on finding inductive invariants (properties shown to hold initially, then to remain true by induction). Abstract interpretation attempts finding inductive invariants within a given domain, e.g. conjunctions of linear inequalities. The classical approach iterates a transformer until the property becomes inductive. In general, this approach may not terminate; thus termination is often enforced with a “widening” operator, which attempts at generalizing the iterates into an inductive property. Unfortunately, widening operators are brittle, with nonmonotonic behaviors (supplying more information about a system may result in worse analysis outcomes!). Therefore, other approaches have been developed (policy iteration,…), which avoid this pitfall. Finally, we shall discuss possible combinations of abstract interpretation and SMTsolving. 
08:45  Summer School Opening SPEAKER: Gopal Gupta 
08:50  Probabilistic Logic Programming I SPEAKER: C.R. Ramakrishnan 
08:45  Fairness for InfiniteState Systems SPEAKER: Heidy Khlaaf ABSTRACT. In this paper we introduce the first known tool for symbolically proving fairCTL properties of (infinitestate) integer programs. Our solution is based on a reduction to existing techniques for fairnessfree CTL model checking. The key idea is to use prophecy variables in the reduction for the purpose of symbolically partitioning fair from unfair executions. 
09:15  Reducing Deadlock and Livelock Freedom to Termination SPEAKER: Thomas Stroeder ABSTRACT. In this paper we introduce a general method for proving deadlock and livelock freedom of concurrent programs with shared memory. Our goal in this work is to support programs which use locks stored in mutable data structures. The key to our technique is the observation that dependencies between locks can be abstracted using recursion and nondeterminism in a sequential logic program such that termination of the abstraction implies deadlock and livelock freedom of the original program. 
09:45  Specifying and verifying liveness properties of QLOCK in CafeOBJ SPEAKER: unknown ABSTRACT. We provide an innovative development of algebraic specifications and proof scores in CafeOBJ of QLOCK's safety and liveness properties. The particular interest of the development is twofold: Firstly, it extends base specifications in ordersorted and rewriting logics to a metalevel, which requires behavioral logic, thus using the three logics together to achieve the proofs. Secondly, we use a search predicate and covering state patterns that allow us to prove the validity of a property over all possible one step transitions, by which safety and liveness properties in the base and meta level can be proven. 
08:45  Store Buffer Reduction with MMUs SPEAKER: Geng Chen ABSTRACT. A fundamental problem in concurrent system design is to identify flexible programming disciplines under which weak memory models provide sequential consistency. For x86TSO, a suitable reduction theorem for threads that communicate only through shared memory was given by Cohen and Schirmer [ITP2010]. However, this theorem cannot handle programs that edit their own page tables (e.g. memory mangers, hypervisors, and some device drivers). The problem lies in the interaction between a program thread and the hardware MMU that provides its address translation: the MMU cannot be treated as a separate thread (since it implicitly communicates with the program thread), nor as part of the program thread itself (since MMU reads do not snoop the store buffer of the program thread). We generalize the CohenSchirmer reduction theorem to handle programs that edit their page tables. The added conditions prevent the MMU of a thread from walking page table entries owned by other threads. 
09:10  Separation Kernel Verification: the XtratuM Case Study SPEAKER: unknown ABSTRACT. The separation kernel concept was developed as an architecture to simplify formal kernel security verification, and is the basis for many implementations of integrated modular avionics in the aerospace domain. This paper reports on a feasibility study conducted for the European Space Agency, to explore the resources required to formally verify the correctness of such a kernel, given a reference specification and a implementation of same. The study was part of an activity called Methods and Tools for OnBoard Software Engineering (MTOBSE) which produced a natural language Reference Specification for a TimeSpace Partitioning (TSP) kernel, describing partition functional properties such as health monitoring, interpartition communication, partition control, resource access, and separation security properties, such as the security policy and authorisation control. An abstract security model, and the reference specification were both formalised using Isabelle/HOL. The C sources of the opensource XtratuM kernel were obtained, and a Isabelle/HOL model of the code was semiautomatically produced. Refinement relations were written manually and some proofs were explored. We describe some of the details of what has been modelled and report on the current state of this work. We also make a comparison between our verification explorations, and the circumstances of NICTA's successful verification of the sel4 kernel. 
09:35  Separation algebras for C verification in Coq SPEAKER: Robbert Krebbers ABSTRACT. Separation algebras are a wellknown abstraction to capture common structure of both permissions and memories in programming languages, and form the basis of models of separation logic. As part of the development of a formal version of an operational and axiomatic semantics of the C11 standard, we present a variant of separation algebras that is well suited for C verification. Our variant of separation algebras has been fully formalized using the Coq proof assistant, together with a library of concrete implementations. These instances are used to build a complex permission model, and a memory model that captures the strict aliasing restrictions of C. 
10:00  Automatically verified implementation of data structures based on AVL trees (SHORT) SPEAKER: Martin Clochard ABSTRACT. I propose verified implementations of several data structures, including randomaccess lists and ordered maps. They are derived from a common parametric implementation of selfbalancing binary trees in the style of AdelsonVelskii and Landis trees. The development of the specifications, implementations and proofs is carried out using the Why3 environment. The originality of this approach is the genericity of the specifications and code combined with a high level of proof automation. 
08:45  LaSh and QUANTIFY Openings SPEAKER: Lash 
09:00  Instantiationbased reasoning, EPR encodings and all that SPEAKER: Konstantin Korovin ABSTRACT. Instantiationbased reasoning aims to combine the expressivity of firstorder logic with the efficiency of propositional and SMT reasoning. Most instantiation based methods are complete for firstorder logic and are especially efficient for the effectively propositional fragment (EPR). It turns out that many problems such as model checking, bitvector reasoning, finite model finding and QBF solving can be succinctly encoded into the EPR fragment. In this talk I will discuss recent developments in instantiationbased reasoning, EPR based encodings and related challenges.

08:45  Tutorial (tentative): TBA SPEAKER: Enrico Giunchiglia 
09:45  SAT Compilation for Constraints over Finite Structured Domains SPEAKER: Alexander Bau ABSTRACT. Due to the availability of powerful SAT solvers, propositional encoding is a successful technique of solving constraint systems over finite domains. As these domains are often flat and nonstructured, we aim to extend this concept by enriching the underlying domain with userdefined product types and sum types. The co4 language is a syntactically subset of Haskell and allows to specify constraint systems over such enriched domains using algebraic data types, patternmatching, higherorder functions and polymorphism. This paper gives an overview over the transformation into propositional logic and illustrates examples and usecases for co4. 
08:45  Relatively filtral quasivarieties SPEAKER: James Raftery ABSTRACT. Improving a recent result of the author, it is shown here that, when a quasivariety K algebraizes a finitary sentential logic L, then L has a classical inconsistency lemma iff K is relatively filtral and its nontrivial members have only nontrivial subalgebras. In the process, the theory of uniform congruence schemes, ideal varieties and filtrality is extended from varieties to quasivarieties, and it is proved that a quasivariety is relatively filtral iff it is relatively semisimple and has equationally definable principal relative congruences. 
09:15  On logics of varieties and logics of semilattices SPEAKER: Josep Maria Font ABSTRACT. This contribution addresses a general problem of abstract algebraic logic and its instantiation for the variety of semilattices, which is the underlying structure of a host of nonclassical logics, in particular fuzzy logics. The general problem is how to associate a logic with a given variety. Since the general theory of abstract algebraic logic provides three procedures to associate a class of algebras with a given logic, our original problem gives rise to three different questions. We show that one of them cannot be answered affirmatively in general, while the other two always can. We determine and study the weakest solution. This leads to a natural definition of the notion of "the logic of a variety". We obtain some results on the poset of all logics of a variety generated by a primal algebra. In the second part we study the poset of the logics of the variety of semilattices, showing that it has a minimum and two maximals and is atomless, among other results. 
09:45  Congruential deductive systems associated with equationally orderable varieties SPEAKER: Ramon Jansana ABSTRACT. We introduce the notion of the deductive system of the order of an equationally orderable quasivariety and we prove that for equationally orederable varieties this deductive system is congreuntial (fully selfextensional). We compare the result with previous results on deductive systems with the congruece property (selfextensional)and the deductiondetachment property or the property of conjunction. 
08:45  Semantial and syntactial charaterisation of some extensions of the class of MValgebras SPEAKER: Krystyna MruczekNasieniewska 
09:15  The space of directions of a polyhedron SPEAKER: Andrea Pedrini ABSTRACT. We study the StonePriestley dual space SpecSubP of the lattice of subpolyhedra of a compact polyhedron P, with motivations coming from geometry, topology, orderedalgebra, and nonclassical logic. From the perspective of algebraic logic, our contribution is a geometric investigation of lattices of prime theories in Łukasiewicz logic, possibly extended with real constants. The main result we announce here is that SpecSubP has a concrete description in terms of a nonHausdorﬀ completion of the space P which holds great geometric interest. If time allows, we discuss selected consequences of our main result, including compactness of the subspace of minimal primes of SpecSubP, and the fundamental property of SubP of being a coHeyting algebra. 
09:45  Interpreting Lukasiewicz logic into Intuitionistic logic SPEAKER: Daniel Mcneill ABSTRACT. Fixing countable sets of propositional variables X and Y, we write Form(X) for the set of formulæ of Łukasiewicz (infinitevalued propositional) logic L, and Form(Y) for the set of formulæ of Intuitionistic (propositional) logic Int. 
08:45  Invited Talk SPEAKER: unknown 
08:45  Cryptosense: Formal Analysis of Security APIs from Research to SpinOff SPEAKER: Graham Steel ABSTRACT. In this talk I'll describe how our research project into adapting formal analysis technqiues for cryptographic protocols to security APIs turned into an industry collaboration and finally a spinoff company, Cryptosense, that was created in September 2013. Though the company is still in its early stages, we've already learned a lot about the journey from academic results to commercial product. I'll talk about what we're doing now, what we're developing for the future, and what its like to transition from full time researcher to startup CEO. 
08:45  Invited Talk: Fragments of Logic, Language, and Computation SPEAKER: Patrick Blackburn ABSTRACT. Amsterdamstyle logicians view modal logic as a fragment of classical logic, and description logicians view their own formalisms in much the same way. Moreover, firstorder logic itself can be viewed as a modest fragment of the higherorder logics of Frege and Russell, a fragment with useful modeltheoretic properties. All in all, the fine structure of logic is a key topic in contemporary research, as the intensive study of (say) the 2variable and various guarded fragments attest. In this talk I want to consider the role of logical fragments in applications. I will focus on applications in natural language, as this is an area rich in nonmonotonic and defeasible inference. Moreover, as my perspective is that of computational (rather than theoretical) linguistics, I am interested in efficient solutions to computational tasks  that is, in fragments of computation. Drawing on a running example involving applications of description logic and classical planning to a dialogue system, I will discuss the role of computation to provide 'pragmatic glue' that lets us work with small wellexplored logical fragments, while simultaneously providing the dynamics required to model various forms of nonmonotonicity. 
09:45  On the NonMonotonic Description Logic ALC+Tmin SPEAKER: Oliver Fernandez Gil ABSTRACT. In the last 20 years many proposals have been made to incorporate nonmonotonic reasoning into description logics, ranging from approaches based on default logic and circumscription to those based on preferential semantics. In particular, the nonmonotonic description logic ALC+Tmin uses a combination of the preferential semantics with minimization of a certain kind of concepts, which represent atypical instances of a class of elements. One of its drawbacks is that it suffers from the problem known as the property blocking inheritance, which can be seen as a weakness from an inferential point of view. In this paper we propose an extension of ALC+Tmin, namely ALC+T+min, with the purpose to solve the mentioned problem. In addition, we show the close connection that exists between ALC+T+min and conceptcircumscribed knowledge bases. Finally, we study the complexity of deciding the classical reasoning tasks in ALC+T+min. 
09:00  Coherent Logic and Applications SPEAKER: Marc Bezem ABSTRACT. Coherent logic (CL) is a fragment of firstorder logic that is more expressive than resolution logic in that it allows a restricted form of existential quantification. Consequently, many theories can be formulated directly in CL, for example, without skolemization. CL has a simple proof theory yielding readable proofs. Thus it strikes a balance beween expressivity and efficiency of automated reasoning. In the talk we give an overview of CL and its application in automated reasoning, proof assistents, model finding, and constraint handling. 
09:00  Decision Problems for Linear Recurrence Sequences SPEAKER: Joel Ouaknine ABSTRACT. Linear recurrence sequences (LRS), such as the Fibonacci numbers, permeate vast areas of mathematics and computer science. In this talk, we consider three natural decision problems for LRS, namely the Skolem Problem (does a given LRS have a zero?), the Positivity Problem (are all terms of a given LRS positive?), and the Ultimate Positivity Problem (are all but finitely many terms of a given LRS positive?). Such problems (and assorted variants) have applications in a wide array of scientific areas, such as theoretical biology (analysis of Lsystems, population dynamics), economics (stability of supplyanddemand equilibria in cyclical markets, multiplieraccelerator models), software verification (termination of linear programs), probabilistic model checking (reachability and approximation in Markov chains, stochastic logics), quantum computing (threshold problems for quantum automata), discrete linear dynamical systems (reachability and invariance problems), as well as combinatorics, statistical physics, formal languages, etc. 
09:00  Satisfiability Solvers SPEAKER: Marijn Heule ABSTRACT. Satisfiability (SAT) solvers have become powerful tools to solve a wide range of applications. In case SAT problems are satisfiable, it is easy to validate a witness. However, if SAT problems have no solutions, a proof of unsatisfiability is required to validate that result. Apart from validation, proofs of unsatisfiability are useful in several applications, such as interpolation and extracting a minimal unsatisfiable set and in tools that use SAT solvers such as theorem provers. We discuss the two main approaches for unsatisfiability proofs: resolution proofs and clausal proofs. Resolution proofs are used for several application, but they are hard to produce. Clausal proofs are easy to emit, but more costly to check. We compare both approaches, present how to produce and validate proofs, and provide some challenges regarding unsatisfiability proofs. 
09:30  Proofs in Satisfiability Modulo Theories SPEAKER: unknown ABSTRACT. We discuss history, techniques, and challenges in producing and checking proofs from SMT solvers. 
09:00  Interpolation in Description Logic: A Survey SPEAKER: Frank Wolter ABSTRACT. We discuss the role of (variants of) Craig interpolation in description logic research. We start by considering Craig interpolation itself and how it is related to the structure of ontologies and the rewritability of queries in ontologybased data access. We then briefly discuss the role of parallel interpolation (introduced more recently by Parikh et al) for decomposing ontologies. Finally, we consider uniform interpolation  an extension of Craig interpolation in which the interpolant is independent from the formula on the righthand side. Uniform interpolation has been the focus of significant research activity in Description Logic, with many theoretical results and first implemented systems. I will not assume any background knowledge about Description Logics but will introduce the relevant notions as required. 
09:00  Machine Translation: Green, Yellow, and Red (abstract) SPEAKER: Aarne Ranta ABSTRACT. The main stream in machine translation is to build systems that are able to translate everything, but without any guarantees of quality. An alternative to this is systems that aim at precision but have limited coverage. Combining wide coverage with high precision is considered unrealistic. Most widecoverage systems are based on statistics, whereas precisionoriented domainspecific systems are typically based on grammars, which guarantee translation equality by some kind of formal semantics. This talk introduces a technique that combines wide coverage with high precision, by embedding a highprecision semantic grammar inside a widecoverage syntactic grammar, which in turn is backed up by a chunking grammar. The system can thus reach good quality whenever the input matches the semantics; but if it doesn't, the user will still get a rough translation. The levels of confidence can be indicated by using colours, whence the title of the talk. The talk will explain the main ideas in this technique, based on GF (Grammatical Framework) and also inspired by statistical methods (probabilistic grammars) and the Apertium system (chunkbased translation), boosted by freely available dictionaries (WordNet, Wiktionary), and built by a community of over 50 active developers. The current system covers 11 languages and is available both as a web service and as an Android application. Demo system: http://www.grammaticalframework.org/demos/translation.html

09:00  Tackling the AwarenessBehaviour Divide in Security: (step 1) Understand the User SPEAKER: Lynne Coventry ABSTRACT. Various factors influence user's behaviour and interactions with technology. This means security has a sociotechnical element, that continues to present a challenge in research and attempts to improve security behaviour. Users may not be the enemy but their (un)intentional (mis)use of technology is certainly part of the problem in security. To solve this problem, we must do more than simply pay lip service to the need to address the human element; we need to systematically explore the environmental, social and personal influencers of behaviour within the context of cybersecurity. Those who seek to ensure cybersecurity must learn to utilise such influencers as efficiently as those who seek to exploit them. Awareness training is touted as the solution, awareness may be necessary but it is seldom sufficient. Psychological research and organisational reports suggest that increased user awareness alone is insufficient when it comes to changing actual behaviour. This may make users' behaviours seem irrational, but they are understandable if you appreciate the cognitive biases people are prone to and the heuristics they use when the time, effort and knowledge required to follow a "rational" decision making process outweighs the benefits perceived by the user. This talk provides a short overview of the issues worthy of exploration in security research and suggests several strategies on how to tackle the security awareness  behaviour divide. 
09:00  QED: a grand unified theory? SPEAKER: John Harrison 
09:35  How to prove the odd order from the four color theorem SPEAKER: Georges Gonthier 
09:15  TradeOff Analysis Meets Probabilistic Model Checking SPEAKER: Christel Baier ABSTRACT. Probabilistic model checking (PMC) is a wellestablished and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMCapproaches focus on computing probabilities and expectations inMarkovian models annotated with numerical values for costs and utility, such as energy and performance. Usually, the utility gained and the costs invested are dependent and a tradeoff analysis is of utter interest. In this paper, we provide an overview on various kinds of nonstandard multiobjective formalisms that enable to specify and reason about the tradeoff between costs and utility. In particular, we present the concepts of quantiles, conditional probabilities and expectations as well as objectives on the ratio between accumulated costs and utility. Such multiobjective properties have drawn very few attention in the context of PMC and hence, there is hardly any tool support in stateoftheart model checkers. Furthermore, we broaden our results towards combined quantile queries, computing conditional probabilities those conditions are expressed as formulas in probabilistic computation tree logic, and the computation of ratios which can be expected on the longrun.

09:15  Intersection Types, Game Semantics and HigherOrder Model Checking SPEAKER: Luke Ong ABSTRACT. Higherorder model checking is the model checking of infinite trees generated by simplytyped lambda calculus with recursion. Although the original decidability proof was based on game semantics, intersection types have played a prominent role in the subsequent development of algorithms for higherorder model checking. In this talk, I will introduce the approach to higherorder model checking based on intersection types, present connections with game semantics, and discuss recent applications of intersection types and game semantics to problems in higherorder computation. 
09:15  Synthesis for monadic logic over the reals SPEAKER: Mark Reynolds ABSTRACT. We say that a firstorder monadic logic of order (FOMLO) sentence is satisfiable over the reals if there is some valuation for the monadic predicates which makes the formula true. Burgess and Gurevich showed that satisfiability for this logic is decidable. They built on pioneering work by Lauchli and Leonard who, in showing a similar result for linear orders in general, had presented some basic operations for the compositional building of monadic linear structures. We look at some recent work in using these basic operations to give a synthesis result. That is, we present an algorithm which given a FOMLO sentence which is satisfiable over the reals, outputs a specific finite description of a model. 
09:15  TestInput Generation using Computational Real Algebraic Geometry SPEAKER: Hoon Hong 
09:15  Does WaitFreedom Matter? SPEAKER: Kapil Vaswani ABSTRACT. Algorithms that guarantee systemwide progress and throughput have seen significant research interest over the last few decades. Systemwide progress becomes even more critical in the context of distributed storage systems, where process failures and network partitions can introduce arbitrary delays. In this talk, we consider the problem of designing waitfree distributed data structures. Recent research shows that certain data structures can indeed be designed to guarantee waitfreedom and consistency in the presence of node failures. We can even characterize conditions under which a waitfree, strongly consistent implementation of a data structure is not possible. On the other hand, we now beginning to understand why distributed algorithms which do not guarantee waitfreedom (such as Paxos), appear to be waitfree in practice. This leads to the following open question – does systemwide progress really matter? 
09:15  Automating the verification of floatingpoint algorithms SPEAKER: Guillaume Melquiond 
09:15  CSPs and fixedparameter tractability SPEAKER: Dániel Marx ABSTRACT. We survey fixedparameter tractability results appearing in the context of satisfiability and constraint satisfaction. The focus of the talk is on explaining the different type of questions that can be asked and briefly summarizing the known results, without going into technical details. 
09:15  TBA SPEAKER: Grigore Rosu ABSTRACT. TBA 
09:45  Nuances of the JavaCard API on the cryptographic smart cards  JCAlgTest project SPEAKER: Petr Svenda ABSTRACT. The main goal of this paper is to describe the JCAlgTest project. The JCAlgTest project is designed for an automatic testing of the degree of support for algorithms listed in the JavaCard API specification by a given smart card. Discussion of the results and trends drawn from the database of 28 different cryptographic smart cards is performed. Additional information about particular algorithm or protocol obtained via timing and power analysis is also described and (partially) available in JCAlgTest database. 
10:45  Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy SPEAKER: Christoph Haase ABSTRACT. It is shown that for any fixed $i>0$, the $\Sigma_{i+1}$fragment of Presburger arithmetic, \emph{i.e.}, its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\Sigma^{\text{EXP}}_{i}$, the $i$th level of the weak EXP hierarchy. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer \& Rabin in 1974. The second part of the paper applies some techniques developed in the first part in order to establish bounds on sets of naturals definable in the $\Sigma_1$fragment of Presburger arithmetic: given a $\Sigma_1$formula $\Phi(x)$, it is shown that the set of solutions is an ultimately periodic set whose period can be doublyexponentially bounded from below and above. 
11:15  On the Discriminating Power of Passivation and HigherOrder Interaction SPEAKER: Valeria Vignudelli ABSTRACT. This paper studies the discriminating power offered by higherorder concurrent languages, and contrasts this power with those offered by higherorder sequential languages (à la lambdacalculus) and by firstorder concurrent languages (à la CCS). The concurrent higherorder languages that we focus on are HigherOrder picalculus (HOpi), which supports higherorder communication, and an extension of HOpi with passivation, a simple higherorder construct that allows one to obtain locationdependent process behaviours. The comparison is carried out by providing embeddings of firstorder processes into the various languages, and then examining the resulting contextual equivalences induced on such processes. As firstorder processes we consider both Labeled Transition Systems (LTSs) and Reactive Probabilistic Labeled Transition Systems (RPLTSs). The hierarchy of discriminating powers so obtained for RPLTSs is finer than that for LTSs; for instance, in the latter case, the additional discriminating power offered by passivation in concurrency is captured, in sequential languages, by the difference between the callbyname and callbyvalue evaluation strategies of an extended typed lambdacalculus. 
11:45  Asymptotic behaviour in temporal logic SPEAKER: Aldric Degorre ABSTRACT. We study the "approximability" of unbounded temporal operators with timebounded operators, as soon as some time bounds tend to infinity. More specifically, for formulas in the fragments PLTL$_\Diamond$ and PLTL$_\Box$ of the Parametric Linear temporal Logic of Alur et al., we provide algorithms for computing the limit entropy as all parameters tend to ∞. As a consequence, we can decide the problem whether the limit entropy of a formula in one of the two fragments coincides with that of its timeunbounded transformation, obtained by replacing each occurrence of a timebounded operator into its timeunbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discretetime timed automata and analysis of their stronglyconnected components. 
12:15  Weight Monitoring with Linear Temporal Logic: Complexity and Decidability SPEAKER: Sascha Wunderlich ABSTRACT. Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the modelchecking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA. 
10:45  On Context Semantics for Interaction Nets SPEAKER: Matthieu Perrinel ABSTRACT. Context semantics is a tool inspired by Girard' s geometry of interaction. It has had many applications from study of optimal reduction to proofs of complexity bounds. However, context semantics have been defined only on lambdacalculus and linear logic. In order to study other languages, in particular languages with more primitives (builtin arithmetics, pattern matching,…) we define a context semantics for a broader framework: interaction nets. These are a wellbehaved class of graph rewriting systems. Here, two applications are explored. First, we define a notion of weight, based on context semantics paths, which bounds the length of reduction of nets. This could be used to prove strong complexity bounds for interaction net systems. Then, we define a denotational semantics for a large class of interaction net systems. 
11:15  The Geometry of Synchronization SPEAKER: unknown ABSTRACT. We graft synchronization onto the most concrete model of Girard’s Geometry of Interaction, namely token machines. This is realized by introducing proofnets for SMLL, an extension of multiplicative linear logic with a speciﬁc construct modeling synchronization points, and a multitoken abstract machine model for it. Interestingly, a correctness criterion ensures the absence of deadlock, this way linking logical and operational properties in a novel way. 
11:45  A new correctness criterion for MLL proof nets SPEAKER: Thomas Ehrhard ABSTRACT. In Girard's original presentation, proof structures of Linear Logic are hypergraphs whose hyperedges are labeld by logical rules and vertices represent the connections between these logical rules. Presentations of proof structures based on interaction nets have the same kind of graphical flavour. Other presentations of proof structures use terms instead of graphs or hypergraphs. The atomic ingredient of these terms are variables related by axiom links. However, the correctness criteria developped so far are adapted to the graphical presentations of proof structures and not to their termbased presentations. We propose a new correctnes criterion for constantfree Multiplicative Linear Logic with Mix which applies to a coherence space structure that a termbased proof structure induces on the set of its variables in a straightforward way. 
12:15  NonElementary Complexities for Branching VASS, MELL, and Extensions SPEAKER: Ranko Lazić ABSTRACT. We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new nonelementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is nonelementary already in the affine case, and match this lower bound for the full propositional affine linear logic, proving its Towercompleteness. We also show that provability in propositional contractive linear logic is Ackermanncomplete. 
10:45  What is Homotopy Type Theory? SPEAKER: Daniel Licata ABSTRACT. The Coq proof assistant is based on MartinLoef's constructive type theory, as realized in the Calculus of Inductive Constructions. Some recent mathematical models have provided a new perspective on constructive type theory, answering some fundamental questions, and suggesting certain new principles that can be added, such as higher inductive types and Voevodsky's univalence axiom. In this talk, I will give a gentle introduction to homotopy type theory, and explain what impact it may have on developing proofs and programs in Coq. Some questions that will be answered include: How is the logic of "homotopy propositions" different from the logic of Prop in CiC? What are univalence and higher inductive types, and what can they be used for? What changes have already been made to Coq to support homotopy type theory, and what might you expect in the future? 
11:45  QuickChick: PropertyBased Testing for Coq SPEAKER: unknown ABSTRACT. Codesigning software or hardware systems and their formal proofs is an appealing idea, with the expectation that the rigor enforced by formal methods will percolate the whole design. In practice however, carrying out formal proofs while designing even a relatively simple system can be an exercise in frustration, with a great deal of time spent attempting to prove things about broken definitions, and countless iterations for discovering the correct lemmas and strengthening inductive invariants. We believe that propertybased testing (PBT) can dramatically decrease the number of failed proof attempts and reduce the overall cost of producing formally verified systems. Despite the existence of experimental tools, Coq is still lagging behind proof assistants like Isabelle, which provides several mature PBT tools. We aim to improve the PBT support in Coq, while also investigating several innovations we could add into the mix like polarized mutation testing and a languagebased approach to custom generation. We are also exploring whether PBT could bring more confidence to the implementation of Coq itself. 
12:15  ProofPattern Search in Coq/SSReflect SPEAKER: unknown ABSTRACT. ML4PG is an extension of the Proof General interface of Coq, allowing the user to invoke machinelearning algorithms and find proof similarities in Coq/SSReflect libraries. In this talk, we will show the recent ML4PG features in action, using examples from the standard SSReflect library and HoTT library. We will compare ML4PG with traditional Coq searching tools and dependency graphs. 
10:45  How do we get inductive invariants? (Part B) SPEAKER: David Monniaux ABSTRACT. Verifying the correctness of loopfree programs (or of general programs, up to bounded depth) is difficult: the state space explodes exponentially as the depth increases. Yet, the difficulty increases as we allow unboundedly many execution steps; proof approaches then generally rely on finding inductive invariants (properties shown to hold initially, then to remain true by induction). Abstract interpretation attempts finding inductive invariants within a given domain, e.g. conjunctions of linear inequalities. The classical approach iterates a transformer until the property becomes inductive. In general, this approach may not terminate; thus termination is often enforced with a “widening” operator, which attempts at generalizing the iterates into an inductive property. Unfortunately, widening operators are brittle, with nonmonotonic behaviors (supplying more information about a system may result in worse analysis outcomes!). Therefore, other approaches have been developed (policy iteration,…), which avoid this pitfall. Finally, we shall discuss possible combinations of abstract interpretation and SMTsolving. 
10:45  Probabilistic Logic Programming II SPEAKER: C.R. Ramakrishnan 
10:45  A Finite Model Property for Intersection Types SPEAKER: Richard Statman ABSTRACT. We show that the relational theory of intersection types known as BCD has the finite model property; that is, BCD is complete for its finite models. Our proof uses rewriting techniques which have as an immediate by product the polynomial time decidability of the preorder [ (although this also follows from the so called beta soundeness of BCD). 
11:15  On Isomorphism of "Functional'' Intersection and Union Types SPEAKER: Mariangiola DezaniCiancaglini ABSTRACT. Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the correct type. In presence of intersection and union types, type isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, which is quite complicated by the interference between functional and non functional types. The present paper faces this problem, by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This is done taking inspiration from the initial projection of Scott's inverse limit lambdamodel. In particular, an isomorphism preserving reduction between types is defined. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, an interesting condition assuring isomorphism between types. 
10:45  Automating Elementary Interpretations SPEAKER: Harald Zankl ABSTRACT. We report on an implementation of elementary interpretations for automatic termination proofs. 
11:15  A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion SPEAKER: Haruhiko Sato ABSTRACT. We present a general approach to encode termination in the dependency pair framework as a satisfiability problem, and include encodings of dependency graph and reduction pair processors. We use our encodings to increase the power of the completion tool Maxcomp. 
11:45  Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling SPEAKER: Alexander Bau ABSTRACT. We SATencode constraints for termination orders based on semantic labelling, argument filters, and recursive path orders, within the dependency pairs framework. We specify constraints in a highlevel Haskelllike language, and translate to SAT fully automatically by the CO4 compiler. That way, constraints can be combined easily. This allows to write a single constraint for: find a model, and a sequence of ordering constraints for the labelled system, such that at least one original rule can be removed completely. As an application, we produce a termination proof, verified by CeTA, for TRS/Aprove/JFP\_Ex31. 
12:15  A Solution to Endrullis08 and Similar Problems SPEAKER: Alfons Geser ABSTRACT. We prove the termination of the string rewriting system Endrullis08, the termination of infinitely many related systems, and even the termination of their union, an infinite string rewriting system. 
12:45  Discussion SPEAKER: Everyone 
10:45  Quantifier handling in calculi for quantified Boolean formulas SPEAKER: Uwe Egly ABSTRACT. Quantified Boolean formulas (QBFs) generalize propositional formulas 
11:30  Encoding Reachability with Quantification SPEAKER: Michael Cashmore ABSTRACT. We report on techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). The techniques exploit the binarytree structure of the QBF quantification to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. We briefly describe our experimental results, and discuss the challenging structure that is implicit in these encodings. 
12:00  EPR Encodings of BitVector Problems Even With Quantifiers SPEAKER: Gergely Kovásznai ABSTRACT. Bitprecise reasoning is essential in many applications of Satisfiability Modulo Theories (SMT). Quantifierfree resp. quantified bitvector formulas (QF_BV resp. BV) play an important role in hardware resp. software verification. In recent years, efficient approaches for solving such formulas have been developed. Most of the QF_BV solvers rely on bitblasting, while BV solvers rely on quantifier instantiation. In [Kovasznai, Froehlich, & Biere, SMT 2012], we investigated the worstcase complexity of those logics and argued that bitblasting resp. quantifier instantiation is exponential resp. doubleexponential in general. We also introduced the criterion "bitwidth boundedness" to bitvector problems, as a property that seems to hold for most practical problems, and proved it to reduce the worstcase complexity by an exponential. 
12:30  Beyond QResolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction SPEAKER: Hubie Chen ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a firstorder sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Qresolution proof system in a broader context; we will discuss how, in a sense made precise, it generalizes Qresolution and gives a clear proof of the soundness of Qresolution.
As an application, we give an algebraic, EhrenfeuchtFraïsséstyle characterization of the condition of not having boundedwidth proofs (for a QCSP instance) and show that the resulting theory can be used to obtain tractability results for the QCSP.
This talk is based on the article available at http://arxiv.org/abs/1403.0222. 
10:45  Parameterized Model Checking of Rendezvous Systems SPEAKER: unknown ABSTRACT. Distributed systems are often parameterized by the number of participating processes, and thus the parameterized model checking problem is equivalent to model checking an infinite state system. A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finitestate systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finitestate system (more precisely a Buchi word automaton), and establish tight bounds on the sizes of such automata. 
11:15  Model Checking Communicating FiniteState Machines using Local Temporal Logics SPEAKER: Roy Mennicke ABSTRACT. We investigate the complexity of the model checking problem for local temporal logics and communicating finitestate machines (CFMs). The input is a number of processes π, a temporal formula F, a CFM C, and a bound β on the maximal number of pending messages allowed. The question is whether all message sequence charts (MSCs) which are accepted by C and for which there exists an execution with βbounded channels fulfill F. We show that this problem can be solved in space polynomial in C, β, and F and exponential in π regarding temporal logics consisting of the usual modalities used in the context of concurrent systems. We also state that if the modalities of the underlying temporal logic can be defined using formulas from the nth level of the monadic quantifier alternation hierarchy, the uniform model checking problem (where the temporal logic is part of the input) is hard for (n+1)fold exponential space and can be solved in (n+3)fold exponential space. If we fix the temporal logic and the number of processes, we obtain matching upper and lower bounds. 
11:45  Unary Pushdown Automata and StraightLine Programs SPEAKER: Dmitry Chistikov ABSTRACT. We consider decision problems for deterministic pushdown automata over the unary alphabet (udpda, for short). Udpda are a simple computation model that accept exactly the unary regular languages, but can be exponentially more succinct than finitestate automata. We complete the complexity landscape for udpda by showing that emptiness (and thus universality) is Phard, equivalence and compressed membership problems are Pcomplete, and inclusion is coNPcomplete. Our upper bounds are based on a translation theorem between udpda and straightline programs over the binary alphabet (SLPs). We show that the characteristic sequence of any udpda can be represented as a pair of SLPsone for the prefix, one for the lassothat have size linear in the size of the udpda and can be computed in polynomial time. Hence, decision problems on udpda are reduced to decision problems on SLPs. Conversely, any SLP can be converted in logarithmic space into a udpda, and this forms the basis for our lower bound proofs. We show coNPhardness of the ordered matching problem for SLPs, from which we derive coNPhardness for inclusion. In addition, we complete the complexity landscape for unary nondeterministic pushdown automata by showing that the universality problem is Pi2Phard, using a new class of integer expressions. Our techniques have applications beyond udpda. We show that our results imply Pi2Pcompleteness for a natural fragment of Presburger arithmetic and coNP lower bounds for compressed matching problems with onecharacter wildcards. 
12:15  Of stacks (of stacks (...) with blind counters) with blind counters SPEAKER: Georg Zetzsche ABSTRACT. Recent work on automata with abstract storage revealed a class of storage mechanisms that proves quite expressive and amenable to various kinds of algorithmic analysis. The storage mechanisms in this class are obtained by \emph{building stacks} and \emph{adding blind counters}. The former is to construct a new mechanism that stores a stack whose entries are configurations of an old mechanism. One can then manipulate the topmost entry, pop it if empty, or start a new one on top. Adding a blind counter to an old mechanism yields a new mechanism in which the old one and a blind counter can be used simultaneously. We call the resulting model \emph{stacked counter automaton}. This talk presents results on expressivity, Parikh images, membership problems, and the computability of downward closures. 
10:45  FirstOrder Automated Theorem Provers SPEAKER: Stephan Schulz 
11:15  HigherOrder Automated Theorem Provers SPEAKER: Christoph Benzmüller 
10:45  Synthesis of Algorithms on Sets Represented as Monotone Lists SPEAKER: Isabela Dramnesc ABSTRACT. We choose to represent sets as sorted lists without duplications, which we call monotone lists. Without loss of generality, we assume that the elements of the sets are from an ordered domain, and we take increasingly sorted lists. This approach leads to more ecient algorithms then the ones for operating on sets represented as nonsorted lists. We use two functions: the function R which applied to a set returns its representation as a monotone list, and the function S which applied to a (monotone) list returns its corresponding set. These two functions are bijective and reverse to each other and represent the isomorphism between the domain of nite sets (with the usual signature) and the domain of monotone lists with the appropriate signature induced by this isomorphism. The synthesis problem consists in producing the algorithms implementing this signature. Each synthesis starts as an inductive constructive proof which applies specic strategies and inference rules. These strategies and inference rules are based on the corresponding properties of sets (as monotone lists). We synthesize (by extracting from proofs) ve algorithms among with two predicates: Member and Inclusion; and three functions: Union, Intersection, and Difference. In parallel with the process of algorithm synthesis we explore the theory of monotone lists. 
11:15  New predicate transformer for symbolic modeling SPEAKER: Alexander Letichevsky ABSTRACT. The paper presents new predicate transformer for symbolic modeling. Predicate transformer is a symbolic function that is used for computing transitions of a system with states represented by means of firstorder formulas. Systems under consideration are compositions of environments and agents inserted into these environments (insertion models). They are specified by means of basic protocols, which represent formal requirements to systems. Previous version of predicate transformer allowed only existential quantifiers in formulas. A new one allows both quantifiers but with some restriction on formulas. The use of universal quantifier is illustrated on the example of MESI protocol. 
11:45  VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel SPEAKER: unknown ABSTRACT. Operating system is a huge software with complicated functionality. The correctness of even single module cannot be proved through software test. Project seL4 has proved the correctness of each function of a microkernel operating system. The correctness of each single function of an operating system cannot prove its integrity and other security property. In this paper we proposed a OS model of finite state machine (OSMFSM). We design our VTOS(Verified Trusted Operating System), which is a microkernel operating system and aimed at being formally verified and trusted, according to this model. We define the state of the OSMFSM through the global objects in VTOS, and the transition function of the OSMFSM as a piecewise defined function through the functions in VTOS. Through establishing a domain for VTOS with the help of OSMFSM and another domain, which is isomorphic to the former, in Isabelle/HOL, we prove the correctness of some functions in the microkernel of VTOS formally. With the help of the concept of the invariability of the FSM, we propose a method of describing and proving the integrity of an OS. 
12:15  Symbolic Problem Solving With Bidirectional Executable Representations SPEAKER: Jakob Praher ABSTRACT. Programs are typically written by humans and executed by computers in order to solve problems over a specific domain. A program  a sequence of instructions executable by a computer  represents the encoded algorithm for solving the problem. The algorithm and data structures are created by the mental understanding of the problem given. This representation also addresses details such as run time efficiency, understandability, or maintainability. Conversely when a programmer tries to understand a program he/she decodes the program again into an abstract mental model. From this model the programmer can start to improve or change the program, which is again encoded and represented as a modified program. In this paper we show a problem solving process that starts with finding, enhancing or inventing a logical theory over first order predicate logic. This theory represents the concepts of the problem domain, relations between the concepts, and operations. A theory is a set of formulae. Operations on terms of the theory correspond to functionality of the solution. These operations can be characterized by partial functions from given input to expected output. Requirements formally express the functionality of the operations and are commonly defined using input/output conditions. If an operation's input satisfies the input condition then operation's output (if obtainable) satisfies the output condition. The process is incremental. It is important to capture the high level requirements. For representing the solution as a machine executable program, the theory should be sufficiently refined so that the requirements satisfy the problem and capture important properties of the execution environment. Detailed conditions make it possible to formally evaluate different design approaches. Design approach refers to the abstractions and methods used for framing the algorithms. As an example in the hash table design it is important to capture the concept of collisions in the table abstractly in order to compare different strategies how to handle collisions. 
10:45  Up and Out: Scaling Formal Analysis Using ModelBased Development and Architecture Modeling SPEAKER: Michael Whalen ABSTRACT. Complex systems are hierarchically constructed in layers, and systems are often constructed middleout rather than topdown; compatibility with existing systems and availability of specific components influences highlevel requirements. This approach leads to an interplay between requirements and design: design choices made at higher levels of abstraction levy requirements on system components at lower levels of abstraction, and design choices restrict the set of possible requirements and acceptable deployment environments. A consequence is that the designation of a "design choice" or "requirement" depends largely on one’s vantage point within the hierarchy of system components. To support iterative design, requirements and architectural design should be more closely aligned: requirements models must account for hierarchical system construction, and architectural design notations must better support specification of requirements for system components.
In this presentation, I describe tools supporting iterative development of architecture and verification based on software models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification. To describe and verify componentlevel behavior, we use Simulink and Stateflow and multiple analysis tools. 
11:45  A logical analysis of framing for specifications with pure method calls SPEAKER: unknown ABSTRACT. For specifying and reasoning about objectbased programs it is often attractive for contracts to be expressed using calls to pure methods. It is useful for pure methods to have contracts, including read effects to support local reasoning based on frame conditions. This leads to puzzles such as the use of a pure method in its own contract. These ideas have been explored in connection with verification tools based on axiomatic semantics, guided by the need to avoid logical inconsistency, and focusing on encodings that cater for first order automated provers. This paper adds pure methods and read effects to region logic, a firstorder program logic that features framebased local reasoning and a proof rule for linking of clients with modules to achieve endtoend correctness by modular reasoning. Soundness is proved with respect to a conventional operational semantics and using the extensional i.e., relationalinterpretation of read effects. The developments in this paper (a) potentially could guide the implementations of linking as used in modular verifiers and (b) should serve as basis for studying observationally pure methods and encapsulation in the setting of relational region logic. 
12:10  A certifying frontend for (sub)polyhedral abstract domains SPEAKER: Alexis Fouilhe ABSTRACT. Convex polyhedra provide a relational abstraction of numerical properties for static analysis of programs by abstract interpretation. We describe a lightweight certification of polyhedral abstract domains using the Coq proof assistant. Our approach consists in delegating most computations to an untrusted backend and checking its outputs with a certified frontend. The backend is free to implement relaxations of domain operators (i.e. a subpolyhedral abstract domain) in order to trade some precision for more efficiency, but must produce hints about the soundness of its results. Previously published experimental results show that the certification overhead with a fullprecision backend is small and that the resulting certified abstract domain has comparable performance to noncertifying stateoftheart implementations. 
12:35  Certification of Nontermination Proofs using Strategies and Nonlooping Derivations SPEAKER: Sarah Winkler ABSTRACT. The development of sophisticated termination criteria for term rewrite systems has led to powerful, complex tools to automatically obtain (non)termination proofs. While many techniques to establish termination have already been formalized, allowing to certify such proofs, this is not the case for nontermination. In particular, the proof checker CeTA was so far limited to (innermost) loops. In this paper we present an Isabelle/HOL formalization of an extended repertoire of nontermination techniques. Firstly, we formalized techniques for nonlooping nontermination. Secondly, the available strategies include (an extended version of) forbidden patterns, which does in particular cover outermost and contextsensitive rewriting. Finally, a mechanism to support partial nontermination proofs allows to further extend the applicability of our proof checker. 
10:45  Metalevel Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development SPEAKER: Joachim Jansen ABSTRACT. Declarative systems aim at solving tasks by running inference engines on a specification, to free its users from having to specify how a task should be tackled. In order to provide such functionality, declarative systems themselves apply complex reasoning techniques, and, as a consequence, the development of such systems can be laborious work. In this paper, we demonstrate that the declarative approach can be applied to develop such systems, by tackling the tasks solved inside a declarative system declaratively. In order to do this, in many cases a metalevel representation of those specifications is required. Furthermore, by using the language of the system for the metalevel representation, it opens the door to bootstrapping: an inference engine can be implemented using the inference it performs itself. One such declarative system is the IDP knowledge base system, based on the language FO(.)IDP, a rich extension of firstorder logic. In this paper, we discuss how FO(.)IDP can support metalevel representations in general and which language constructs make those representations even more natural. Afterwards, we show how metaFO(.)IDP can be applied to bootstrap its model expansion inference engine. We discuss the advantages of this approach: the resulting program is easier to understand, easier to maintain and more flexible. 
11:15  Logical Machinery of Heuristics (Preliminary Report) SPEAKER: Shahab Tasharrofi ABSTRACT. This paper is a preliminary report on a new declarative language that allows the programmer to specify heuristics (problemspecific inference methods) about the problem that is being solved. The heuristics that are defined in our language control and/or change the behavior of the underlying solver. In this way, we are able to attain problemspecific solvers that benefit from both the stateoftheart general inference methods available in generalpurpose solvers, and the problemspecific reasoning methods that are applicable only to this specific problem. 
11:45  Modeling High School Timetabling as PartialWeighted maxSAT SPEAKER: Emir Demirović ABSTRACT. High School Timetabling (HSTT) is a well known and wide spread problem. The problem consists of coordinating resources (e.g. teachers, rooms), time slots and events (e.g. lectures) with respect to various constraints. Unfortunately, HSTT is hard to solve and just finding a feasible solution for simple variants of HSTT has been proven to be NPcomplete. In addition, timetabling requirements vary from country to country and because of this many variations of HSTT exist. Recently, researchers have proposed a general HSTT problem formulation in an attempt to standardize the problem from different countries and school systems. In this paper, for the first time we provide a new detailed modeling of the general HSTT as SAT, in which all constraints are treated as hard constraints. In order to take into account soft constraints, we extend the previous model to Partial Weighted maxSAT. In addition, we present experimental results and compare to other approaches, using both artificial and realworld instances, all of which were taken from the Third International Timetabling Competition 2011 benchmark repository. Our approach gives competitive results and in some cases outperforms the winning algorithm from the competition. 
12:15  Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability SPEAKER: Matti Järvisalo ABSTRACT. Bayesian network structure learning is the wellknown computationally hard problem of finding a directed acyclic graph structure that optimally describes given data. A learned structure can then be used for probabilistic inference. While exact inference in Bayesian networks is in general NPhard, it is tractable in networks with low treewidth. This provides good motivations for developing algorithms for the NPhard problem of learning optimal bounded treewidth Bayesian networks (BTWBNSL). In this work, we develop a novel scorebased approach to BTWBNSL, based on casting BTWBNSL as weighted partial Maximum satisfiability. We demonstrate empirically that the approach scales notably better than a recent exact dynamic programming algorithm for BTWBNSL. Submitted to LaSh’14 for presentation only. Conference version of this paper appears as Jeremias Berg, Matti Järvisalo, and Brandon Malone. Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability. In Proceedings of the 17th International Conference on Artificial Intelligence and Statistics (AISTATS 2014), volume 33 of JMLR Workshop and Conference Proceedings, pages 8695. JMLR, 2014. 
12:45  Depart for Workshop Lunch SPEAKER: Lash ABSTRACT. The LaSh workshop lunch is included in the registration fee. Contact the workshop organizers if you are not registered by wish to join the lunch. 
10:45  Invited talk: MaxSat and SoftCSPs SPEAKER: Fahiem Bacchus ABSTRACT. The formalisms for MaxSat and SoftCSPs are strongly related much like SAT and CP. Both address the problem of constrained optimization. The formalism that is the 800kg gorilla of this area is Mixed Integer Programming (MIPS). Of these three formalisms the technology for solving MIPs is the most developed, although MaxSat and SoftCSP solvers have also made significant progress. All three formalisms have focused on exploiting quite distinct algorithmic methods, and empirical evidence indicates that each of these formalisms can dominate the others on particular problems. A promising research direction is to explore the hybridization of these formalisms, and in this talk I will discuss some of the work that has been done and that is yet to be done in exploiting the disparate strengths of these formalisms. 
11:45  Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms SPEAKER: El Mouelhi Achref ABSTRACT. In this paper, we investigate the complexity of algorithms for solving CSPs which are classically implemented in real practical solvers, such as Forward Checking or Bactracking with Arc Consistency (RFL or MAC).. We introduce a new parameter for measuring their complexity and then we derive new complexity bounds. By relating the complexity of CSP algorithms to graphtheoretical parameters, our analysis allows us to define new tractable classes, which can be solved directly by the usual CSP algorithms in polynomial time, and without the need to recognize the classes in advance. So, our approach allows us to propose new tractable classes of CSPs that are naturally exploited by solvers, which indicates new ways to explain in some cases the practical efficiency of classical search algorithms. 
12:15  BreakIDGlucose: on the importance of row symmetry SPEAKER: Jo Devriendt ABSTRACT. Symmetry is a topic studied by both the Satisfiability (SAT) and Constraint Programming (CP) community. However, few attempts at transferring results between both communities have been made. This paper makes the link by explaining how symmetries from Constraint Satisfiaction Problems (CSP's) transfer to their direct SATencoding. We point out that many interesting symmetry groups of CP all map to piecewise row symmetries of their CSP's SATencoding, which using a CP result can be broken completely. We then show that the standard SAT symmetry approaches do not break these symmetries completely, so we address this issue by designing a new symmetry breaking preprocessor, implemented as the BreakIDGlucose SATsolver. BreakIDGlucose's first place in the hard combinatorial track of 2013's SATcompetition proves the relevance of this approach. 
10:45  The Range of Realization Which modal logics have explicit counter parts SPEAKER: Melvin Fitting 
11:45  Tutorial: Fuzzy Description Logics (Part 1) SPEAKER: Franz Baader 
10:45  Exposing Predictive Analytics through Natural Language Dialog SPEAKER: Christina Unger ABSTRACT. In industry and academics alike, there is a renewed interest in data processing in general, and in deriving value from widely available data more specifically. The applications developed to this end often have nonexperts as audience, which has led to a lot of research into verbalizing data into natural language. However, the proposed solutions often include predictive technologies that, along with predicted future events or behaviours, also generate additional information such as probabilities and confidence scores. This gives rise to data that goes beyond future facts alone and that has to be communicated to its users in order to enable a correct interpretation of the predictions. In this paper we explore the additional natural language needed when applications offer predictive analytics technology to their users. We demonstrate how to modularly implement the grammars needed to verbalize predictive aspects, independent of (existing) conceptualizations and lexical resources available for the domain of the data. 
11:15  Natural Language Access to Data SPEAKER: Kyle Richardson ABSTRACT. Knowledge and reasoning in a specific subject domain can greatly assist in natural language processing. This is demonstrated in the context of a question answering system for accessing data for business enterprise software. 
10:45  Banking security Wish list: notes from the edge SPEAKER: George French 
11:25  Welltyped generic smartfuzzing for APIs SPEAKER: Thomas Braibant ABSTRACT. We demonstrate how to use a tiny domainspecific language for the description of APIs make it possible to perform blackbox testing of APIs. Given an API, our testing framework behaves like regular client code and combines functions exported by the API to build elements of the datatypes that are exported by the API. Once the API has been systematically exercised, the user can verify that some properties hold at the API level. In the submitted abstract, we use the running example of datastructures APIs, but the very same ideas apply to the smartfuzzing of security APIs. 
12:05  Caetus tool SPEAKER: Josef Hertl ABSTRACT. The goal of the paper is to develop a software for automated analysis of PKCS#11 tokens with focus on the security of stored cryptographic keys. The paper first outlines the PKCS#11 standard and the Cryptoki API specified by the standard, including the various components of the API. Then the paper describes the mechanics of cryptographic key protection in Cryptoki. It analyses the individual functions relevant to key protection and defines the first set of tests. Then the paper performs an analysis of the previously published attacks against keys stored on the device and also outlines the second set of tests with focus on discovering attack vulnerabilities. Afterwards the paper examines various ways to improve the security of Cryptoki by altering the standard. The discussion of the proposed restrictions takes into consideration their impact on practical usability of the tokens. In order to further evaluate the security of the tokens against possible attacks, the paper also utilizes model checker software. The results of the previously defined tests are used to compose a model that is sent to a model checker for further analysis. Since the developed software is written in Java, the paper also examines the Java PKCS#11 wrapper and discusses the advantages and disadvantages against using C for implementation. The most obvious advantage is that the software can be easily deployed on other operating systems, which is particularly useful for testing tokens that only work on Windows. The disadvantage is that the used wrapper does not implement all the Cryptoki functions, but the paper shows that all these limitations either do not matter or they can be worked around. The paper also presents the developed tool called Caetus. The tool first connects into the token, discovers the basic capabilities of the device and based on these capabilities it performs indepth testing of Cryptoki functions. First part of the tests focuses on adherence to the PKCS#11 standard, which means the discovered issues do not necessarily mean security risks. The other set of tests attempts to discover vulnerability of the token to the previously published attacks and other trivial attacks. Finally the tool can use the discovered capabilities in order to compose a model specification which is then sent to the model checker. The tool is currently optimized for analysis of software tokens. The last part of the paper consists of tables with results of token testing and discussion of the results. 
10:45  WaitFreedom Made Practical SPEAKER: Erez Petrank ABSTRACT. With the proliferation of multicore systems, the design of concurrent algorithms and concurrent data structures to support them has becomes critical. Waitfree data structures provide a very basic and natural progress guarantee, assuring that each thread always makes progress when given enough CPU cycles. However, waitfree algorithms were considered difficult to design and too costly to be used in practice. Only the weaker lockfree guarantee, which allows almost all threads to starve, was achievable in practice. In a series of recent papers, we have shown that this pessimistic belief was false and waitfreedom is actually achievable efficiently in practice. 
11:45  A new reduction for eventdriven distributed programs SPEAKER: unknown ABSTRACT. We consider the problem of provably verifying that an asynchronous messagepassing system satisfies its local assertions. We present a novel reduction scheme for asynchronous eventdriven programs that finds almostsynchronous invariants invariants consisting of global states where message buffers are close to empty. The reduction finds almostsynchronous invariants and simultaneously argues that they cover all local states. We show that asynchronous programs often have almostsynchronous invariants and that we can exploit this to build natural proofs that they are correct. We implement our reduction strategy, which is sound and complete, and show that it is more effective in proving programs correct as well as more efficient in finding bugs in several programs, compared to current search strategies which almost always diverge. The high point of our experiments is that our technique can prove the Windows Phone USB Driver written in P correct for the receptiveness property, which was hitherto not provable using stateoftheart modelcheckers. 
10:45  Leveraging Linear and Mixed Integer Programming for SMT SPEAKER: Tim King ABSTRACT. Solvers for Satisfiability Modulo Theories (SMT) combine the ability of fast Boolean satisfiability solvers to find solutions for complex propositional formulas with specialized theory solvers. Theory solvers for linear real and integer arithmetic reason about systems of simultaneous inequalities. These solvers either find a feasible solution or prove that no such solution exists. Linear programming (LP) solvers come from the tradition of optimization, and are designed to find feasible solutions that are optimal with respect to some optimization function. Typical LP solvers are designed to solve large systems quickly using floating point arithmetic. Because floating point arithmetic is inexact, rounding errors can lead to incorrect results, making these solvers inappropriate for direct use in theorem proving. Previous efforts to leverage such solvers in the context of SMT have concluded that in addition to being potentially unsound, such solvers are too heavyweight to compete in the context of SMT. In this paper, we describe a technique for integrating LP solvers that dramatically improves the performance of SMT solvers without compromising correctness. These techniques have been implemented using the SMT solver CVC4 and the LP solver GLPK. Experiments show that this implementation outperforms other stateoftheart SMT solvers on the QF_LIA and QF_LRA SMTLIB benchmarks. 
11:15  raSAT: SMT for Polynomial Inequality SPEAKER: unknown ABSTRACT. This paper presents an iterative approximation refinement, called rasat loop, which solves a system of polynomial inequalities on real numbers. The approximation scheme consists of interval arithmetic (overapproximation, aiming to decide UNSAT) and testing (underapproximation, aiming to decide SAT). If both of them fail to decide, input intervals are refined by decomposition. The rasat loop is implemented as an SMT rasat with miniSAT 2.2 as a backend SAT solver. We discuss three strategy design choices: dependency to set priority among atomic polynomial constraints, sensitivity to set priority among variables, and UNSAT core for reducing learned clauses and incremental UNSAT detection. Preliminary experimental observation on comparison with Z3 4.3, dReal, and isat3 is also discussed. 
11:45  Better Answers to Real Questions SPEAKER: unknown ABSTRACT. We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a postprocessing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by applications of our implementation to various examples from the literature, where it significantly improves the quality of the results. 
12:15  Towards ConflictDriven Learning for Virtual Substitution SPEAKER: unknown ABSTRACT. We consider SMTsolving for linear real arithmetic. Inspired by related work for the FourierMotzkin method, we combine virtual substitution with learning strategies. For the first time, we present virtual substitutionincluding our learning strategiesas a formal calculus. We prove soundness and completeness for that calculus. Some standard linear programming benchmarks computed with an experimental implementation of our calculus show that the integration of learning techniques into virtual substitution gives rise to considerable speedups. Our implementation is opensource and freely available. 
10:45  Extracting Monadic Parsers from Proofs SPEAKER: Alison Jones ABSTRACT. This talk outlines a prooftheoretic approach to developing correct and terminating monadic parsers. Using a modified realisability interpretation, we extract provably correct and terminating programs from formal proofs. If the proof system is proven to be correct, then any extracted program is guaranteed to be so. By extracting parsers, we can ensure that they are correct, complete and terminating for any input. The work is ongoing, and is being carried out in the interactive proof system Minlog. 
11:30  Intuitionistic Ancestral Logic SPEAKER: Liron Cohen ABSTRACT. We define pure intuitionistic Ancestral Logic (iAL), extending pure intuitionistic FirstOrder Logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for transitive closure, TC. We derive this operator from the natural type theoretic definition of TC using intersection.
We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable. 
10:45  Resolution Based Uniform Interpolation for Expressive Description Logics SPEAKER: unknown ABSTRACT. Ontologies represented using description logics model domains of interest in terms of concepts and binary relations, and are used in a range of areas including medical science, bioinformatics, semantic web or artificial intelligence. Often, ontologies are large and complex and cover 10,000s of concepts. Uniform interpolants are restricted views of ontologies, that only use a specified set of symbols, while preserving all entailments that can be expressed using these symbols. Uniform interpolation can be used for analysing hidden relations in an ontology, removing confidential concepts from an ontology, computing logical differences between ontologies or extracting specialised ontologies for ontology reuse and has many more applications. We follow a resolutionbased approach to make the computation of uniform interpolants of larger ontologies feasable. Uniform interpolants cannot always be represented finitely in the language of the input ontology, for which situation we offer three solutions: extending the signature with additional concepts, approximating the uniform interpolant, or using fixpoint operators. 
11:15  Practical CNF Interpolants Via BDDs SPEAKER: unknown ABSTRACT. Craig interpolation has been recently shown to be useful in a wide variety of problem domains. One use is in strategy extraction for two player games, as described in our accompanying submission. However, interpolation is not without its drawbacks. It is wellknown that an interpolant may be very large and highly redundant. Subsequent use of the interpolant requires that it is transformed to CNF or DNF, which will further increase its size. We present a new approach to handling both the size of interpolants and transformation to clausal representation. Our approach relies on the observation that in many realworld applications, interpolants are defined over a relatively small set of variables. Additionally, in most cases there likely exists a compact representation of the interpolant in CNF. For instance, in our application to games an interpolant represents a set of winning states that is likely to have a simple structure. 
11:45  Interpolation and Domain Independence applied to Databases SPEAKER: Enrico Franconi ABSTRACT. We study a general framework for query rewriting in the presence of a domain independent firstorder logic theory (a knowledge base) over a signature including database and nondatabase predicates, based on Craig's interpolant and Beth's definability theorem. In our framework queries are (possibly open) domain independent firstorder formulas over the extended signature. The database predicates are meant to be closed, i.e., their extensions are the same in every model since they represent a classical finite relational database, whereas the nondatabase predicates in the ontology are interpreted classically, i.e., their extensions may vary across different models. It is important to notice that all the conceptual modelling languages devised for the designing of information and database systems (such as EntityRelationship schemas, UML Class diagrams, ObjectRole Modelling ORM diagrams, etc) are domain independent: they can be formalised as domain independent first order theories. Given a domain independent knowledge base and a query implicitly definable from the database signature, the framework provides precise semantic conditions to decide the existence of a domain independent firstorder logically equivalent reformulation of the query (called exact rewriting) in terms of the database signature, and if so, it provides an effective approach to construct the reformulation based on interpolation using standard theorem proving techniques (e.g., tableau). We are interested in domain independent reformulations of queries because their rangerestricted syntax is needed to reduce the original query answering problem to a relational algebra evaluation over the original database, that is, it is effectively executable as an SQL query directly over the database. Due to the results on the applicability of Beth's theorem and Craig's interpolant, we prove the completeness of our framework in the case of domain independent ontologies and queries expressed in any fragment of firstorder logic enjoying finitely controllable determinacy, a stronger property than the finite model property of the logic. If the employed logic does not enjoy finitely controllable determinacy our approach would become sound but incomplete, but still effectively implementable using standard theorem proving techniques. In order to constructively compute the exact domain independent query reformulation we use the tableau based method to find the Craig’s interpolant to compute the from a validity proof of the implication (KB and Q) > (KB > Q). Since description logics knowledge bases are not necessarily domain independent, we have syntactically characterised the domain independent fragment of several very expressive fragments of description logics by enforcing a sort of guarded negation, a very reasonable restriction from the point of view of conceptual modelling. These fragments do also enjoy finitely controllable determinacy. We have applied this framework not only to query answering under constraints, but also to data exchange and to view update. 
12:15  Treebased Modular SMT Solving SPEAKER: unknown ABSTRACT. Modern Satisfiability Modulo Theories (SMT) solvers are highly efficient and can generate a resolution proof in case of unsatisfiability. Some applications, such as synthesis of Boolean controllers, compute multiple coordinated interpolants from a single refutation proof. In order to do so, the proof is required to have two properties: It must be colorable and localfirst. The latter means that resolution over a literal that occurs just in one partition, has to have both premises derived from this partition. Offtheshelf SMT solvers do not necessarily produce proofs that have these properties. In particular, proofs are usually not localfirst. Hofferek et al. 1 suggest to perform proof transformations to obtain a colorable and localfirst proof, but these transformations can be computationally expensive. Our goal is to introduce a new method to directly compute a localfirst, colorable resolution proof for an unsatisfiable SMT formula. This proof can then be directly used for ninterpolation. Our approach uses a treebased structure of SMT solvers, where every node in the tree is associated with a formula (possibly empty initially), and a (possibly empty) set of literals. The semantics of the modular SMT problem is the conjunction of the formulas of all nodes. The set of literals associated with a node is computed recursively as follows. Every literal, which appears in more than one descendant of a parent node, is assigned to the parent node. During solving, every node makes decisions about its associated literals only. We start at the root node and communicate the partial assignments to the child nodes until we reach a leaf. Every node has its own solver instance and tries to compute a satisfying assignment w.r.t. the given partial assignments. A blocking clause is added to the parent node if no satisfying assignment can be found. If all child nodes find a satisfying assignment and the conjunction of them is theoryconsistent, we either decide more literals, or return to the parent node if we already have a full assignment for all the literals of the current node. In case the conjunction is inconsistent within the theory, we respectively add a blocking clause for the current assignment to the children. In order to obtain this clauses while keeping the modular structure intact, we perform interpolation over the assignments of the children and use the interpolants, which are guaranteed to contain only "global" literals (which can safely be added to the children without breaking the modularity), to learn a blocking clause for every child node. The algorithm terminates if either solely full assignments are communicated to the root node and there is no literal left to decide, or when enough clauses have been learned at the root node to show inconsistency. In the latter case we are able to extract a resolution proof with the same modular structure as the original problem. We are currently working on implementing this approach in the hope that we can use it to generate colorable, localfirst proofs for synthesis problems much faster than with postprocessing proof transformations. 
10:45  Constructive Cryptography and Security Proofs SPEAKER: Ueli Maurer ABSTRACT. Constructive cryptography, an alternative paradigm for designing cryptographic protocols and proving their security, is reviewed in this talk and contrasted with other approaches. In constructive cryptography, a cryptographic scheme (e.g. encryption) is seen as constructing a certain resource (e.g. a secure channel) from another resource (e.g. an authenticated channel and a secret key), for a welldefined notion of construction. The construction notion is composable, which allows to design complex protocols in a modular, layered manner. The security proofs of the modules (e.g. encryption, authentication, key agreement, or signatures) directly compose to a security proof for the entire protocol. A treatment in constructive cryptography comes with several advantages, among them:  Simplicity and reusability due to the modular design.  The semantics of security definitions are clear in the sense that one knows how a scheme satisfying a given definition can be used. This allows to compare security definitions.  The treatment is at an abstract level, freed from artefacts like Turing machines, asymptotics, polynomialtime, communication tapes, etc.  Informationtheoretic and computational security are different instantiations of the same security statement.  It appears better amenable to a treatment by formal methods.

10:45  Connection matrices of finite rank instead of definability in Monadic Second Order Logic SPEAKER: Johann Makowsky ABSTRACT. Connection matrices for graphs and hypergraphs are a generalization of Hankel matrices for words. They were used by L. Lovasz and A. Schrijver and their collaborators to characterize which graph parameters arise from partition functions. Lovasz also noted that they can be used to make Courcelle's Theorem, which shows that graph properties definable in Monadic Second Order Logic (MSOL) are in FPT on graph classes of bounded treewidth, logicfree by replacing MSOLdefinability by a finiteness condition on the rank of connection matrices and allowing graph parameters with values in a field. In this paper we extend this to graph parameters with values in a tropical semirings rather than a field, and graph classes of bounded cliquewidth. 
11:15  Backdoors into Two Occurrences SPEAKER: Jan Johannsen ABSTRACT. The class CNF(2) of CNFformulas in which every variable has at most two occurrences is a lesser known tractable case of SAT. Backdoor sets for this class are studied in terms of parameterized complexity. The question whether there exist a CNF(2)backdoor set of size k is hard for the class W[2], for both weak and strong backdoors, and in both cases it becomes fixedparameter tractable when restricted to inputs in dCNF for a fixed d. 
10:45  Neighbourhood SAC for Preprocessing and Search SPEAKER: Richard Wallace ABSTRACT. This paper reports extensions and further analysis of a new form of singleton arc consistency, called neighbourhood SAC (NSAC), where a subproblem adjacent to the variable with a reduced domain (the "focal variable") is made arc consistent. The first part of the paper presents two important extensions: (1) NSAC is generalized to kNSAC, where k is the longest path between the focal variable and any variable in the subgraph. In this framework, the original NSAC becomes 1NSAC; but in addition, we can have 2NSAC, 3NSAC, etc. up to a point where there is no difference from full SAC. In this work we will only consider the justnamed forms. Obviously, there is an associated dominance hierarchy with respect to level of consistency, with kNSAC < (k+1)NSAC until full SAC is reached. (2) NSAC can be extended in a relatively straightforward way to handle nary constraints, although there are some subtleties, which are discussed. The second part presents some studies of hybrid search techniques based on NSAC and SAC, using a variety of problems. Comparisons are made using the domain/degree and the domain/weighted degree variable ordering heuristics. In some cases, higher levels of consistency maintenance outperform MAC by several orders of magnitude, although with weighted degree the best tradeoff is obtained when SACbased consistency is restricted to preprocessing. 
10:45  A SuperpositionBased Approach to Abductive Reasoning in Equational Clausal Logic SPEAKER: Nicolas Peltier ABSTRACT. (joint work with M. Echenim and S. Tourret) Abstract: Abduction can be defined as the process of inferring plausible explanations (or hypotheses) from observed facts (conclusions). This form of reasoning has the potential of playing a central role in system verification, particularly for identifying bugs and providing hints to correct them. We describe an approach to perform abductive reasoning that is based on the superposition calculus. The formulas we consider are sets of firstorder clauses with equality, and the abducibles (in other words the hypotheses that are allowed to be inferred) are boolean combinations of equations constructed over a given finite set of ground terms. By duality, abduction can be reduced to a consequencefinding problem. We thus show how the inference rules of the superposition calculus can be adapted to obtain a calculus that is deductive complete for ground clauses built on the considered sets of ground terms, thus guaranteeing that all abducible formulas can be generated. This calculus enjoys the same termination properties as the superposition calculus: in particular, it is terminating on ground extensions of decidable theories of interest in software verification. The number of implicates of a given equational formula is usually huge. We describe techniques for storing sets of abduced clauses efficiently, and show how usual triebased approaches for representing sets of propositional clauses in a compact way can be adapted and extended in order to denote equational clauses up to equivalence (modulo the axioms of equality). We provide algorithms for performing redundancy pruning in an efficient way on such representations. We identify hints for improvements and provide lines of ongoing and future research. 
10:45  Automated Test Case Generation and Model Checking with CHR SPEAKER: Ralf Gerlich ABSTRACT. We present an example for application of CHR to automated test data generation and model checking in verification of mission critical software for satellite control. 
11:15  From XML Schema to JSON Schema: Translation with CHR SPEAKER: Falco Nogatz ABSTRACT. Despite its rising popularity as data format especially for web services, the software ecosystem around the JavaScript Object Notation (JSON) is not as widely distributed as that of XML. For both data formats there exist schema languages to specify the structure of instance documents, but there is currently no opportunity to translate already existing XML Schema documents into equivalent JSON Schemas. 
11:45  Constraint Handling Rules with Multiset Comprehension Patterns SPEAKER: Iliano Cervesato ABSTRACT. CHR is a declarative, concurrent and committed choice rulebased constraint programming language. We extend CHR with multiset comprehension patterns, providing the programmer with the ability to write multiset rewriting rules that can match a variable number of constraints in the store. This enables writing more readable, concise and declarative code for algorithms that coordinate large amounts of data or require aggregate operations. We call this extension CHR^cp . We give a highlevel abstract semantics of CHR^cp , followed by a lowerlevel operational semantics. We then show the soundness of this operational semantics with respect to the abstract semantics. 
12:15  Discussion SPEAKER: Everyone ABSTRACT. We have additional discussion time for all talks before lunch 
10:45  On Unfolding for Programs Using Strings as a Data Type SPEAKER: Andrei Nemytykh ABSTRACT. {Regular paper} As a rule, program transformation methods based on semantics unfold a semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically. Unfolding is one of the basic operations, which is a metaextension of one step of the abstract machine executing the program. This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base. Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream. We define a class of term rewriting systems manipulating with strings and describe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete. Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set. 
11:30  Branching Processes of Conservative Nested Petri Nets SPEAKER: Daniil Frumin ABSTRACT. Nested Petri nets (NPnets) is an extension of the Petri nets formalism with accordance to the “netswithinnets” approach, when tokens in a marking are themselves Petri nets which have autonomous behavior and synchronize with the system net. The formalism of NPnets allows for modeling multilevel multiagent systems with dynamic structure in a natural way. In this paper we define branching processes and unfoldings for conservative NPnets, i.e. for NPnets with a persistent set of agents. We show that NPnets unfoldings satisfy the fundamental property of unfoldings, and thus can be used for verification of conservative NPnets in line with classical unfolding methods. 
12:15  Local Driving in HigherOrder Positive Supercompilation via the Omegatheorem SPEAKER: unknown ABSTRACT. A program transformation technique should terminate, return efficient output programs and be efficient itself. For positive supercompilation ensuring termination requires memoisation of expressions, and these are subsequently used to determine when to perform generalization and folding. For a firstorder language, every infinite sequence of transformation steps must include function unfolding, so it is sufficient to memoise only those expressions immediately prior to a function unfolding step. However, for a higherorder language, it is possible for an expression to have an infinite sequence of transformation steps which do not include function unfolding, so memoisation prior to a function unfolding step is not sufficient by itself to ensure termination. But memoising additional expressions is expensive during transformation and may lead to less efficient output programs due to auxiliary functions. This additional memoisation may happen explicitly during transformation or implicitly via a preprocessing transformation as outlined in previous work by the first author. We introduce a new technique for local driving in higherorder positive supercompilation which obliviates the need for memoising other expressions than function unfolding steps, thereby improving efficiency of both the transformation and the generated programs. We exploit the fact, due to the second author in the setting of typefree lambdacalculus that every expression with an infinite sequence of transformation steps not involving function unfolding must have somthing like the term Omega = (lambda x. x x) (lambda x . x x) embedded within it in a certain sense. The technique has proven useful on a host of examples. 
10:45  25 years of the Mizar Mathematical Library SPEAKER: Adam Grabowski ABSTRACT. Throughout the years, the development of the Mizar Mathematical Library was stimulated by large formalization projects, of which the proof of the Jordan Curve Theorem and the encoding of "Compendium of Continuous Lattices" were most influential. In Andrzej Trybulec's (the head of the Mizar project) opinion, expressed during QED II workshop in 1995, "one of the fundamental tasks of the QED effort should focus on reconstruction of the language and technology of mathematics." We will show how Andrzej's dreams of QED are implemented. 
11:20  The seL4 microkernel verification SPEAKER: Gerwin Klein ABSTRACT. This talk will first give a brief highlevel overview of the formal verification of the seL4 microkernel before showing some of its proof techniques in more detail. The aim will be to show examples of libraries and tactics for refinement, invariant, and security proofs for operating systems. 
11:55  Towards Formally Verified Theorem Provers  Part I SPEAKER: Magnus Myreen 
12:15  Towards Formally Verified Theorem Provers  Part II SPEAKER: Ramana Kumar 
12:30  TBA SPEAKER: Claudio Sacerdoti Coen 
10:45  Program Analysis for JavaScript Web Applications SPEAKER: Anders Møller ABSTRACT. JavaScript supports a powerful mix of objectoriented and functional programming, which provides flexibility for the programmers but also makes it difficult to reason about the behavior of the programs without actually running them. One of the main challenging for program analysis tools is to handle the complex programming patterns that are found in widely used libraries, such as jQuery, without losing critical precision. Another challenge is the use of dynamic language features, such as 'eval'. This talk presents an overview of the challenges and the techniques used in the TAJS research project that aims to develop sound and effective program analysis techniques for JavaScript web applications. 
11:45  Analyzing JavaScript: The Bad Parts SPEAKER: Nicholas Labich ABSTRACT. JavaScript is a popular, powerful, and highly dynamic programming language. It is the arguably the most widely used and ubiquitous programming language, has a low barrier to entry, and has vast amounts of code in the wild. JavaScript has grown from a language used primarily to add small amounts of dynamism to web pages into one used for largescale applications both in and out of the browserincluding operating systems and compilers. As such, automated program analysis tools for the language are increasingly valuable. Almost all of the research to date targets ECMAScript 3, a standard that was succeeded by the most recent version, 5.1, over four years ago. Much of the research targets wellbehaved subsets of JavaScript, eliding the darker corners of the language (the bad parts). In this work, we demonstrate how to statically analyze full, modern JavaScript, focusing on uses of the language's socalled bad parts. In particular, we highlight the analysis of scoping, strict mode, property and object descriptors, getters and setters, and eval. Speed, precision, and soundness are the basic requirements of any static analysis. To obtain soundness, we began with LambdaS5, a small, functional language developed by Guha et al. that, through desugaring, encompasses the entirety of the ECMAScript 5.1 standard. Its small size and deliberate desugaring make it a tractable intermediate representation for the analysis of JavaScript. Leveraging the semantics of LambdaS5, we build an abstract machine interpreter. Following the abstracting abstract machines recipe developed by Van Horn and Might, a smallstep abstract machine is easily and soundly transformed into an abstract interpreter. Once we have a sound abstract interpreter, speed and precision can be configured from a number of angles. Optimization techniques developed by Johnson et al. make any AAMstyle analyzer faster. By parameterizing the analyzer's allocation function we gain another axis of control. A modular design of the analyzer's values makes it possible to plugandplay different lattices, which is necessary for testing different abstractions of JavaScript's values and nontrivial objects. The objects of the 5.1 specification are no longer simple keyvalue mappings, but map their string keys to either data or accessor properties, each of which hold their own metadata. Further, data properties can be converted to and from accessor properties. The objects themselves hold metadata that changes the semantics of modifying both their mappings and metadata, causing the same line of code to either update a value, silently have no effect, or raise an exception. In the setting of analysis, a map with abstract spaces for both keys and values presents its own challenges to retain soundness while remaining performant. As an example of a potential lattice, we discuss an abstraction of JavaScript's objects that significantly improves performance at the cost of a loss in precision. 
12:15  Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract) SPEAKER: Matthew Hague ABSTRACT. Multistack pushdown systems are a wellstudied model of concurrent computation using threads with firstorder procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higherorder procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multistack collapsible pushdown systems have been little studied. In a recent FSTTCS article we studied ordered, phasebounded and scopebounded multistack collapsible pushdown systems using saturation techniques and showed decidability of control state reachability, as well as giving a regular representation of all configurations that can reach a given control state. 
11:00  On local induction schemes SPEAKER: Andres CordónFranco ABSTRACT. Firstorder Peano arithmetic $PA$ is axiomatized over a finite algebraic base theory by the full induction scheme $$\varphi(0,v) \land \forall x \, (\varphi(x,v) \rightarrow \varphi(x+1,v)) \rightarrow \forall x \, \varphi(x,v),$$ where $\varphi(x,v)$ ranges over all formulas in the language of arithmetic $\{0,1,+,\cdot,<\}$. Fragments of arithmetic are obtained by restricting, in one way or another, the induction scheme axiomatizing $PA$. Classical examples include the theories of $\Sigma_n$ and $\Pi_n$ induction and their parameter free counterparts. In this talk we present a new kind of restriction on the induction scheme, giving rise to new subsystems of arithmetic that we collectively call \emph{local induction} theories. Roughly speaking, local indiction axioms have the form $$\varphi(0,v) \land \forall x \, (\varphi(x,v) \rightarrow \varphi(x+1,v)) \rightarrow \forall x \in \mathcal{D} \, \varphi(x,v).$$ That is to say, we restrict the $x$'s for which the axiom claims $\varphi(x,v)$ to hold to the elements of a prescribed subclass $\mathcal{D}$ of the universe. Natural choices for $\mathcal{D}$ are the sets of the $\Sigma_n$definable elements of the universe as well as other related substructures of definable elements. We will study the basic properties of the local induction theories obtained in this way and derive a number of applications to the study of 'classical' fragments of $PA$. Remarkably, we show that the hierarchy of local reflection principles can be reexpressed in terms of our local induction theories, thus filling a gap in our understanding of the equivalence between reflection and induction in arithmetic. 
12:00  Tutorial on Classical Realizability and Forcing 2 SPEAKER: Alexandre Miquel 
11:20  Concept Learning by a MonteCarlo Tree Search of Argumentations SPEAKER: unknown ABSTRACT. MonteCarlo Tree Search (MCTS) is a heuristic to search in large trees. We apply it to argumentation with regard to concept learning where MCTS pursues the best argumentation meant to account for a possibly inconsistent set of training examples. We provide experimental results of our approach with the search variant Upper Confidence Bounds on Tree (UCT) 
11:50  Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies SPEAKER: unknown ABSTRACT. In the last decade, thanks to the ability of analyzing probabilistic models given specifications in temporal logics, Probabilistic Model Checking (PMC) has become a widely used methodology in several application domains, e.g., communication protocols, planning and scheduling, and robotics. Moreover, the availability of effective PMC tools enables automated analysis in such complex realworld scenarios. In this paper we evaluate PMC tools to investigate safety of robots whose control policies are learned by reinforcement, i.e., considering feedback signals received upon acting in unknown environments. Introduced in previous contributions of ours, a new challenging application domain for PMC tools is represented by their usage as backengines of an automated methodology aimed to verify and repair control policies. We present an evaluation of the current stateoftheart PMC tools and assess their potential on various case studies, including both real and simulated robots accomplishing navigation, manipulation and reaching tasks. 
12:20  Self Regulating Mechanisms for Network Immunization SPEAKER: unknown ABSTRACT. Many real network, e.g. internet or communication systems, can be modeled as scalefree network. An important property of these type of networks is that the diffusion of information to all nodes is very fast. Therefore, immunization strategies are necessary for this type of networks to prevent that a virus can infect, starting from some nodes, the entire network. In recent years, various immunization strategies has been developed and they can be divided into two main class: centralized and distributed strategies. Both of these approaches have a limitation of having the need to know the number of nodes of the network that must be immunized. In this paper, we propose an AOC based immunization strategy modification in which the entities self regulate their population inside the network. In this strategy the entities are deployed in a network with a threshold of coverage of the graph to be achieved. The entities, while collectively search the nodes with the highest degree, estimate the coverage of the graph through the information in their local environment and reproduce accordingly. The self regulating mechanism is evaluated on a set of public benchmark networks, even with communitybased structures, and experimental results about convergence, coverage efficiency, computational cost and scalability are presented. 
12:40  An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal CuttingStock Problem SPEAKER: Slimane AbouMsabah ABSTRACT. The orthogonal cuttingstock problem tries to place a given set of items in a minimum number of identicallysized bins. As part of solving this problem with guillotine constraint, we propose to combine the new BLF2G, Bottom Left Fill 2 direction Guillotine, placement heuristic with an advanced genetic algorithm. According to the items order, the BLF2G routine makes a direct placement of items on bins to give a cutting format. The genetic algorithm exploits the search space to find the supposed optimal items order. Other methods tires to guide the evolutionary process by introducing a greedy heuristics to the initial population to enhance the results. We propose to enrich the population by qualified individuals, without disturbing the genetic phase, by introducing a new enhancement to guide the evolutionary process. We control the evolution and when we observe that there are no improvements, after some iterations, we inject a qualified individual to the population to avoid premature convergence to a local optimum. We generate a set of orderbased individuals, to enrich the evolutionary process. Our method is compared with other heuristics and metaheuristics found in literature on existing data sets. 
11:45  Transfer Semantics for the Clear Parser SPEAKER: Richard Crouch ABSTRACT. Transfer semantics uses a rewriting (or transfer) system to map syntactic parses onto semantic representations [4, 5]. This form of semantic mapping was used to build broad coverage semantic text indexes at Powerset, and has been used in various other settings such as question answering for intelligence analysts and medical QA. It has been used for English, German [14] and Japanese [13]. However, in all these cases the transfer semantics has been applied to the output of just one kind of parser: LFG functional structures created by the XLE parser [6]. This paper describes the adaptation of transfer semantics to apply to the output of the Clear dependency parser [2]. 
12:15  Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts SPEAKER: unknown ABSTRACT. In this contribution, we start form a concrete problem: the identification of argument compounds and show how their structure can be modelled on a linguistic and logical basis. This investigation is, in a first stage, restricted to arguments found in technical texts. Then, we propose a typebased syntactic analysis and the premises of a conceptual model that accounts for the logical properties of such compounds. An implementation in Dislog is presented with an indicative evaluation of the results. Dislog runs on TextCoop which is a logicbased platform we developed for discourse analysis. 
12:00  Uniform Proofs of Normalisation and Approximation for Intersection Types SPEAKER: Kentaro Kikuchi ABSTRACT. We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method. Our systems are more natural than Valentini's ones and equivalent to the usual natural deduction style systems. We prove the characterisation theorems of strong and weak normalisation through the proposed systems, and, moreover, the approximation theorem without using the reducibility method. This provides in a uniform way proofs of the normalisation and approximation theorems via type systems in sequent calculus style. 
12:30  Indexed linear logic and higherorder model checking SPEAKER: unknown ABSTRACT. In recent work, Kobayashi observed that the acceptance by an alternating tree automaton A of an infinite tree T generated by a higherorder recursion scheme G may be formulated as the typability of the recursion scheme G in an appropriate intersection type system associated to the automaton A. The purpose of this article is to establish a clean connection between this line of work and Bucciarelli and Ehrhard's indexed linear logic. This is achieved in two steps. First, we recast Kobayashi's result in an equivalent infinitary intersection type system where intersection is not idempotent anymore. Then, we show that the resulting type system is a fragment of an infinitary version of Bucciarelli and Ehrhard's indexed linear logic. While this work is very preliminary and does not integrate key ingredients of higherorder modelchecking like priorities, it reveals an interesting and promising connection between higherorder model checking and linear logic. 
12:00  Interactive Theorem Provers from the perspective of Isabelle/Isar SPEAKER: Makarius Wenzel ABSTRACT. Interactive Theorem Provers have a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 2030 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of addon tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and openendedness in the combination of logical tools: typical interactive provers use automated provers and disprovers routinely in their portfolio. The subsequent exposition of interactive theorem proving (ITP) takes Isabelle/Isar as the focal point to explain concepts of the greater "LCF family'', which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to endusers without requiring selfassembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its overall architecture and extralogical infrastructure. The "Isar'' aspect of Isabelle refers first to the structured language for humanreadable and machinecheckable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus "Isabelle/Isar'' today refers to an advanced proof assistant with extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE). 
12:30  Calculus of Inductive Constructions SPEAKER: Christine PaulinMohring 
12:00  Temporal OBDA with LTL and DLLite SPEAKER: unknown ABSTRACT. We investigate various types of query rewriting over ontologies given in the standard temporal logic LTL as well as combinations of LTL with DLLite logics. In particular, we consider FO(<)rewritings that can use the temporal precedence relation, FO(<,+)rewritings that can also employ the arithmetic predicate PLUS, and rewritings to finite automata with data given on the automaton tape. 
12:25  Complexity of Temporal Query Abduction in DLLite SPEAKER: unknown ABSTRACT. Temporal query abduction is the problem of hypothesizing a minimal set of temporal data which, given some fixed background knowledge, warrants the entailment of the query. This problem formally underlies a variety of forms of explanatory and diagnostic reasoning in the context of time series data, data streams, or otherwise temporally annotated structured information. In this paper, we consider (temporally ordered) data represented in Description Logics from the popular DLLite family and Temporal Query Language, based on the combination of LTL with conjunctive queries. In this defined setting, we study the complexity of temporal query abduction, assuming different restrictions on the problem and minimality criteria for abductive solutions. As a result, we draw several revealing demarcation lines between NP, DP and PSpacecomplete variants of the problem. 
12:50  Temporalising EL Concepts with Time Intervals SPEAKER: unknown ABSTRACT. We design and investigate a new interval based temporal description logic, ELLambda, which is based on an Annotated Logic introduced by Kifer, AL, and motivated by lifescience applications. We show how a subset of the logic can be captured as the EL fragment of AL, ELAL, and then go on to show how we can extend this representation to capture further temporal entailments. We show that both ELAL and ELLambda maintain the same tractable complexity bounds for reasoning as EL and finally provide an example of how the logic can be utilised for the Drosophila developmental ontology. 
12:53  Transition Constraints for Temporal Attributes SPEAKER: E. A. Nasubo Ongoma ABSTRACT. Representing temporal data in conceptual data models and ontologies is required by various application domains, and for it to be useful for modelling precision and useful with automated reasoners, a language that is expressive enough to capture the required operational semantics of the timevarying information is essential. Temporal modelling languages have little support for temporal attributes, if at all, yet attributes are a standard element in the widely used conceptual modelling languages such as EER and UML. This hiatus prevents one to utilise a complete temporal conceptual data model and keep track of evolving values of data and its interaction with temporal classes. A rich axiomatization of fully temporized attributes is possible with a minor extension to the already very expressive description logic language DLRUS . We formalize the notion of transition of attributes, and their interaction with transition of classes. The transition specified for attributes are extension, evolution, and arbitrary quantitative extension. 
12:56  A StreamTemporal Query Language for Ontology Based Data Access SPEAKER: unknown ABSTRACT. The paper contributes to the recent enterprise of temporalizing and streamifiying ontology based data access (OBDA) by discussing rewritability and unfoldability aspects for DLLite instantiations of the new querylanguage framework STARQL. In particular, it demonstrates how STARQL queries can be rewritten and unfolded into queries expressed in one of the early relational stream query languages, the continuous query language CQL. 
12:00  A tool for automating the computationally complete symbolic attacker SPEAKER: unknown ABSTRACT. In this paper we describe a tool automating the computationally complete symbolic attacker model provided by Bana and Comon at POST'12. This model offers soundness guarantees without the usual computational soundness restrictions such as tagging, key cycles... This models allows to find attacks relying on implementation mistakes. Using our tool, we discovered a such new attack on Andrew's secure RPC, we hope to find more attacks in the next few months. 
12:20  Towards a Coinductive Characterization of Computational Indistinguishability SPEAKER: unknown ABSTRACT. Computational indistinguishability (CI in the following) is one of the most central concepts in modern cryptography, and many other definitions (e.g. pseudorandomness, security of cryptoschemes) can be rephrased in terms of CI. We present the results of a study directed towards giving a direct and precise characterization of computational indistinguishability in an higherorder functional language for polynomial time computability, in which tools from implicit computational complexity and coinduction both play a central role. 
12:40  Actual Causes of Security Violations SPEAKER: Divya Sharma ABSTRACT. Accurate blame assignment for security violations is essential in a wide range of settings. For example, protocols for authentication and key exchange, electronic voting, auctions, and secure multiparty computation (in the semihonest model) ensure desirable security properties if protocol parties follow their prescribed programs. However, if they deviate from their prescribed programs and a security property is violated, determining which agents should be blamed and appropriately punished is important to deter agents from committing future violations. This work proposes actual causation (i.e., identifying which agents' deviations caused a specific violation) as a useful building block for blameassignment. The central contribution of this work is formalizing and reasoning about actual causation in decentralized multiagent systems, in particular, to formalize programs (rather than events) as actual causes of security violations and to deal with nondeterministic systems. 
12:00  Discovering Archipelagos of Tractability: SplitBackdoors to Constraint Satisfaction SPEAKER: Robert Ganian ABSTRACT. The Constraint Satisfaction Problem (CSP) is a central and generic computational problem which provides a common framework for many theoretical and practical applications. A central line of research is concerned with the identification of classes of instances for which the CSP can be solved in polynomial time, such classes are often called "islands of tractability". A prominent way of defining islands of tractability for the CSP is to restrict the relations that may occur in the constraints to a fixed set, called a constraint language. A constraint language is conservative if it contains all unary relations. Schaefer's famous Dichotomy Theorem (STOC 1978) identifies all islands of tractability in terms of tractable constraint languages over a Boolean domain of values. Since then many extensions and generalizations of this result have been obtained. Recently, Bulatov (TOCL 2011, JACM 2013) gave a full characterization of all islands of tractability for CSP and the counting version CSP that are defined in terms of a conservative constraint language. Our results build upon these results and show how the identified islands of tractability can be combined to "archipelagos of tractability" (in general, the union of tractable constraint languages is not tractable). In order to put this to work, we need some control over the way how the constraints over the various considered tractable languages interact with each other. We capture this by the notion of a splitbackdoor which is a set of variables that, when instantiated, separate the CSP instance into pairwise independent parts, each of which falls into a different island of tractability. Strong backdoors, as introduced by Williams et al. (IJCAI 2003), form the special case where all instantiations of the backdoor variables move the instance into one fixed island. The main difficulty lies in finding a splitbackdoor of given size k; once the splitbackdoor is found, we can try all possible instantiations of the backdoor variables and apply the polynomial time algorithms associated with the islands of tractability on the list. Our main result is an algorithm that finds a splitbackdoor (with respect to a list of finite conservative constraint languages) in FPT time; this also gives an FPT time algorithm for solving the decision or counting version of CSP for the given instance, assuming the decision or counting version of CSP, respectively, is polynomialtime tractable for the considered constraint languages. As part of our algorithm for finding the splitbackdoors, we first develop an algorithm to compute "splitmodulators" in a graph theoretical setting. This has the advantage that we can build upon existing advanced algorithmic techniques. In particular, we show that for any finite collection of finite sets of (possibly disconnected) graphs F, there is an algorithm that, given a graph G and a positive integer k, in FPT time (parameterized by k) either finds a subset X of V(G) of size at most k such that for each connected component C of GX there is some F_i in F such that C has no graph from F_i as an induced subgraph, or correctly reports that no such set X exists. This result has numerous applications outside CSP, as it can be used to combine known polynomial time algorithms for NPhard problems restricted to classes of instances characterized by forbidden induced subgraphs. 
12:00  Satisfiability Modulo NonDisjoint Combinations of Theories Connected via Bridging Functions SPEAKER: unknown ABSTRACT. The NelsonOppen combination method is ubiquitous in all Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular nondisjoint unions of theories connected via bridging functions. This problem is of greatest interest for solving verification problems expressed in a combination of data structures and arithmetic. Our work can be viewed as a synthesis of previous contributions by different authors, based on different techniques and frameworks, like the one developed by SofronieStokkermans based on locality principles. We investigate here an approach by reduction from nondisjoint to disjoint combination which is particularly wellsuited to combine a wide range of data structures with bridging functions over a target theory. We focus on data structures for which the standard superposition calculus provides an offtheshelf underlying satisfiability procedure. We also consider the problem of adapting the combination procedure to get a satisfiability procedure for a standard interpretation of the data structure. 
12:30  Finding Minimum Type Error Sources SPEAKER: Zvonimir Pavlinovic ABSTRACT. Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler typically reports a single program location in its error message. This location is the point where the type inference failed, but not necessarily the actual source of the error. Other potential error sources are not even considered. Hence, the compiler often misses the true error source, which increases debugging time for the programmer. In this paper, we present a general framework for automatic localization of type errors. Our algorithm finds all minimum error sources, where the exact definition of minimum is given in terms of a compilerspecific ranking criterion. Compilers can use minimum error sources to produce more meaningful error reports, and for automatic error correction. Our approach works by reducing type inference to constraint satisfaction. We then formulate the problem of computing minimum error sources in terms of weighted maximum satisfiability modulo theories (MaxSMT). Ranking criteria are incorporated by assigning weights to typing constraints. The reduction to MaxSMT allows us to build on decision procedures to support rich type systems. 
12:00  Some thoughts about benchmarks for NMR SPEAKER: Daniel Le Berre ABSTRACT. The NMR community would like to build a repository of benchmarks to push forward the design of systems implementing NMR as it has been the case for many other area in AI. There are a number of lessons which can be learned from the experience of other communi ties. Here are a few thoughts about the requirements and choices to make before building such a repository. 
12:30  Towards a Benchmark of Natural Language Arguments SPEAKER: unknown ABSTRACT. The connections among natural language processing and argumentation theory are becoming stronger in the latest years, with a growing amount of works going in this direction, in different scenarios and applying heterogeneous techniques. In this paper, we present two datasets we built to cope with the combination of the Textual Entailment framework and bipolar abstract argumentation. In our approach, such datasets are used to automatically identify through a Textual Entailment system the relations among the arguments (i.e., attack, support), and then the resulting bipolar argumentation graphs are analyzed to compute the accepted arguments. 
14:30  Formalization of Errorcorrecting Codes using SSReflect SPEAKER: unknown ABSTRACT. By adding redundant information to transmitted data, errorcorrecting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and coding/decoding time has driven much research, culminating with LowDensity ParityCheck (LDPC) codes. Harddisk storage, wifi communications, mobile phones, etc.: most modern devices now rely on ECCs and in particular LDPC codes. Yet, correctness guarantees are only provided by research papers of evergrowing complexity. One solution to improve this situation is to provide a formalization of ECCs. We think that a first difficulty to achieve this goal has been lifted by the SSReflect library, that provides a substantial formalization of linear algebra. Using this library, we have been tackling the formalization of linear ECCs. Our formalization of linear ECCs is already rich enough to formalize most properties of Hamming codes and we are now in a position to formalize the more difficult LDPC codes. 
15:00  Autosubst: Automation for de Bruijn Substitutions SPEAKER: unknown ABSTRACT. Formalizing syntactic theories with variable binders is not easy. We present Autosubst, a library for the Coq proof assistant to automate this process. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions. Our core contribution is an automation tactic that solves equations involving terms and substitutions. This makes the usage of substitution lemmas unnecessary. The tactic is based on our current work on a decision procedure for the equational theory of an extension of the sigmacalculus by Abadi et. al. The library is completely written in Coq and uses Ltac to synthesize the substitution operation. 
15:30  Automating Abstract Logics SPEAKER: Gregory Malecha ABSTRACT. We present the results of our efforts building compositional proof automation for program verification. We focus our efforts on abstract axiomatizations of different logics in order to make our procedures more generally applicable. Our automation leverages computational reflection to solve both intuitionistic and separation logic entailments. These specialized procedures are parameterized by auxiliary procedures that can reason about domainspecific theories such as arithmetic. 
14:30  Regular Combinators for String Transformations SPEAKER: Rajeev Alur ABSTRACT. Abstract We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using twoway finitestate transducers, (oneway) cost register automata, and MSOdefinable graph transformations. In this paper, we give an algebraic and machineindependent characterization of this class analogous to the definition of regular languages by regular expressions. When the monoid is commutative, we prove that every regular function can be constructed from constant functions using the combinators of choice, split sum, and iterated sum, that are analogs of union, concatenation, and Kleene*, respectively, but enforce unique (or unambiguous) parsing. Our main result is for the general case of noncommutative monoids, which is of particular interest for capturing regular stringtostring transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions: (1) the leftadditive versions of split sum and iterated sum, which allow transformations such as string reversal; (2) sum of functions, which allows transformations such as copying of strings; and (3) function composition, or alternatively, a new concept of chained sum, which allows output values from adjacent blocks to mix. The uploaded PDF is the concetation of the short and full versions of the paper. 
15:00  On Periodically Iterated Morphisms SPEAKER: unknown ABSTRACT. We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control, PerD0L systems for short. These systems give rise to a class of onesided infinite sequences, called PerD0L words. We construct a PerD0L word with exponential subword complexity, thereby answering a question raised by (Lepisto 1993) on the existence of such words. We solve another open problem concerning the decidability of the firstorder theories of PerD0L words (Muchnik, Pritykin, Semenov 2009); we show it is already undecidable whether a certain letter occurs in a PerD0L word. This stands in sharp contrast to the situation for D0L words (purely morphic words), which are known to have at most quadratic subword complexity, and for which the monadic theory is decidable. 
15:30  FiniteMemory Strategy Synthesis for Robust Multidimensional MeanPayoff Objectives SPEAKER: Yaron Velner ABSTRACT. Twoplayer games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis problem is to compute the minimal (or infimum) value that player 1 can assure, and the boolean analysis problem asks whether player 1 can assure that the value of the objective is at most r (for a given threshold r). Meanpayoff expression games are played on a multidimensional weighted graph. An atomic meanpayoff expression objective is the meanpayoff value (the longrun average weight) of a certain dimension, and the class of meanpayoff expressions is the closure of atomic meanpayoff expressions under the algebraic operations of max, min, numerical complement and sum. In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with meanpayoff expression objectives. While in general, optimal strategies for these games require infinitememory, in synthesis we are typically interested in the construction of a finitestate system. Hence, we consider games in which player 1 is restricted to finitememory strategies, and our main contribution is as follows. We prove that for meanpayoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is interreducible with Hilbert's tenth problem over rationals  a fundamental longstanding open problem in computer science and mathematics. 
14:30  A type theory for productive coprogramming via guarded recursion SPEAKER: Rasmus Ejlers Møgelberg ABSTRACT. To ensure consistency and decidability of type checking, proof assistants impose a requirement of productivity on corecursive definitions. In this paper we investigate a typebased alternative to the existing syntactic productivity checks of Coq and Agda, using a combination of guarded recursion and quantification over clocks. This approach was developed by Atkey and McBride in the simply typed setting, here we extend it to a calculus with dependent types. Building on previous work on the toposoftrees model we construct a model of the calculus using a family of presheaf toposes, each of which can be seen as a multidimensional version of the toposoftrees. As part of the model construction we must solve the coherence problem for modelling dependent types in locally cartesian closed categories simulatiously in a whole family of locally cartesian closed categories. We do this by embedding all the categories in a large one and applying a recent approach to the coherence problem due to Streicher and Voevodsky. 
15:00  FormulaeasTypes for an Involutive Negation SPEAKER: Guillaume MunchMaccagnoni ABSTRACT. Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulaeastypes correspondence between the involutive negation in proof theory, and a notion of highlevel access to the stacks studied by Felleisen and Clements. 
15:30  EilenbergMacLane Spaces in Homotopy Type Theory SPEAKER: unknown ABSTRACT. Homotopy type theory is an extension of MartinL\"of type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopytheoretic theorems, in a way that is very amenable to computerchecked proofs in proof assistants such as Coq and Agda. In this paper, we give a computerchecked construction of \emph{EilenbergMacLane spaces}. For an abelian group $G$, an EilenbergMacLane space $K(G,n)$ is a space (type) whose $n^{th}$ homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in $G$. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far. 
14:30  Hardware Model Checking (Part A) SPEAKER: Fabio Somenzi 
14:30  Answer Set Programming I SPEAKER: Martin Gebser 
14:30  Lucretia — intersection type polymorphism for scripting languages SPEAKER: Aleksy Schubert ABSTRACT. Scripting code may present maintenance problems in the long run. There is, then, the call for methodologies that make it possible to control the properties of programs written in dynamic languages in an automatic fashion. We introduce Lucretia, a core language with an introspection primitive. Lucretia is equipped with a (retrofitted) static type system based on local updates of types that describe the structure of objects being used. In this way, we deal with one of the most dynamic features of scripting languages, that is, the runtime modification of object interfaces. Judgements in our systems have a Hoarelike shape, as they have a precondition and a postcondition part. Preconditions describe static approximations of the interfaces of visible objects before a certain expression has been executed and postconditions describe them after its execution. The field update operation complicates the issue of aliasing in the system. We cope with it by introducing intersection types in method signatures. 
15:00  Liquid Intersection Types SPEAKER: Mário Pereira ABSTRACT. We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been able to prove several interesting properties for our system (including subject reduction) and developed an inference algorithm, which we proved to be sound. 
14:30  Frege on mathematical progress SPEAKER: Patricia Blanchette ABSTRACT. Progress in mathematics has often involved a good deal of conceptual clarification, including increasingly precise characterizations of concepts (e.g. those of infinity, of continuity, perhaps of ‘set,’ etc.) that were less clearly understood by earlier theorists. But the sometimesvast difference between the earlier and later concepts that go by the same name raises the possibility that such conceptual refinement really brings with it a whole new subjectmatter for the branch of mathematics in question, rather than a clarified understanding of the concepts used by earlier generations. This talk investigates Gottlob Frege’s approach to understanding this kind of conceptual progress, and assesses the plausibility of his view that a given subjectmatter can survive essentially unscathed despite fairly radical changes in the surrounding theory. 
15:15  On Bernays' Generalization of Cantor's Theorem SPEAKER: Gabriel Uzquiano ABSTRACT. Cantor's theorem that no oneone function maps a set a onto the power set of a follows from the statement that no function maps a set a onto the power set of a. Paul Bernays showed how to encode assignments of subclasses of a given A to members of A by means of a class of ordered pairs, and he deployed a familiar diagonal argument to show that no assignment of subclasses of A to members of A is onto. It much less clear how to make sense of an assignment of members of A to subclasses of A, but when we do, we are in a position to show that no such assignment is oneone. Unfortunately, familiar arguments for this claim fail to provide an explicit characterization of two different subclasses of A which are assigned one and the same member of A by a given assignment. George Boolos later showed how to specify explicit counterexamples to the claim that a function from the power set of a set a into the set a is oneone. Similar constructions turn out to be available in the case of classes, but they are sensitive to the presence of impredicative class comprehension. We explore some ramifications of this observation for traditional philosophical puzzles raised by the likes of Russell's paradox of propositions in Appendix B of "The Principles of Mathematics" and Kaplan's paradox. 
14:30  Large cardinals, forcing axioms, and the theory of subsets of \omega_1 SPEAKER: Daisuke Ikegami ABSTRACT. The goal of this research is to rule out "natural" independence phenomena in Set Theory by maximizing your theory in terms of large cardinals and forcing axioms. Using large cardinals in ZFC, by the results of Woodin, we have a clear understanding of the theory of the secondorder structure (\omega, P(\omega), \in)) and what it should be. In this talk, we try to extend this understanding to the theory of the structure (\omega_1, P(\omega_1), \in) by using large cardinals, forcing axioms, and some hypothesis from inner model theory in ZFC. This is joint work with Matteo Viale. 
15:15  Locally definable wellorders SPEAKER: Philipp Lücke ABSTRACT. A classical theorem of Mansfield shows that there exists a wellordering of the set \omega^\omega of all functions from \omega to \omega$that is definable over the collection H(\omega_1) of all hereditarily countable sets by a \Pi_1formula without parameters if and only if every such function is contained in Gödel's constructible universe L. In particular, the existence of such a wellordering implies that the continuum hypothesis holds. We consider the question whether this implication generalizes to higher cardinalities: does the existence of a wellordering of the set \omega_1^{\omega_1} of all functions from \omega_1 to \omega_1 that is definable over H(\omega_2) by a \Pi_1formula without parameters imply that the GCH holds at \omega_1? This is joint work with Peter Holy (Bristol). 
14:30  On the derivational complexity of Kachinuki orderings SPEAKER: Dieter Hofbauer ABSTRACT. For string rewriting systems compatible with the standard Kachinuki ordering it is known that their derivational complexity is primitive recursively bounded. However, in case the definition of Kachinuki orderings comprises a possibly different lexicographic status for different letters, the standard upper bound proof method by monotone interpretations fails, and primitive recursive complexity bounds are an open problem, to the best of our knowledge. In this talk, such an upper bound result is shown by examining worst case rewriting strategies. 
15:00  Kurth's Criterion H Revisited SPEAKER: Alfons Geser ABSTRACT. Criterion H is one of the criteria for termination of string rewriting that Winfried Kurth implemented in his thesis. Criterion H can be slightly improved. The improved version can be translated into a termination proof by Semantic Labelling. 
15:30  Another Proof for the Recursive Path Ordering SPEAKER: Nachum Dershowitz ABSTRACT. Yet another proof of wellfoundedness of the recursive path ordering is provided. 
14:30  Algorithmic Paradigms for Solving QBF SPEAKER: Fahiem Bacchus ABSTRACT. The past 15 years has seen tremendous improvement in the effectiveness of solvers for Quantified Boolean Formulas (QBF). This talk will discuss some of the main algorithmic approaches that have been employed in constructing such solvers. We will aim to identify certain features of these approaches that are effective and not so effective. Some of the theoretical questions that arise from our empirical experience with these solvers will be identified in an attempt to spur more synergy between theory and practice for solving QBF. 
15:30  Projective Quantifier Elimination for Equational Constraint Solving SPEAKER: Paqui Lucio ABSTRACT. We deal with (general) equational constraints, that is, firstorder formulas, with equality as its only predicate symbol, over a (finite or infinite) language $\Language$ of function symbols. As semantic domain, we consider the algebra of finite terms over L. Solving one of such constraints means to find all the solutions for (i.e. assignments to) its free variables. We present the Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraicstyle transformation of expressions instead of handling firstorder formulas. PQE is formulated on the basis of three algebraic operations on expressions: complement, intersection and projection. We aim to contribute not only a new style of quantifier elimination for constraint solving, but also a more efficient method for equational constraint solving. PQE avoids unnecessary applications of the costly Explosion Rule (ER) that are performed by traditional solving methods. 
14:30  Playing with Automata and Trees SPEAKER: Olivier Serre ABSTRACT. Roughly speaking a finite automaton on infinite trees is a finite memory machine that takes as input an infinite nodelabelled binary tree and processes it in a topdown fashion as follows. It starts at the root of the tree in its initial state, and picks (possibly nondeterministically) two successor states, one per son, according to the current control state, the letter at the current node and the transition relation. Then the computation proceeds in parallel from both sons, and so on. Hence, a run of the automaton on an input tree is a labelling of this tree by control states of the automaton, that should satisfy the local constrains imposed by the transition relation. A branch in a run is accepting if the omegaword obtained by reading the states along the branch satisfies some acceptance condition (typically an omegaregular condition such as a Büchi or a parity condition). A run is accepting if *all* branches are accepting. Finally, a tree is accepted by the automaton if *there exists* an accepting run over this tree. Hence, there are three natural levers on which one can act to define alternative families of tree automata / tree languages.  The first lever is local with respect to the run: it is the conditionrequired for a branch to be accepting.  The second lever is global with respect to the run: it is the condition required for a run to be accepting.  The third lever has to do with the set of runs: it is the condition required for a tree to be accepted (wrt the set of runs over it). For the usual definition of tree automata the three lever are: parity condition on branches / all branches accepting for run / there exists an accepting run. In this talk I will mainly focus on the second and third levers and propose variants of them. More precisely (time depending):  second lever: count the number of accepting/rejecting branches (cardinality constraint), topologically measure the largeness of the set of accepting/rejecting branches, measure (à la Lebesgue) the set of accepting/rejecting branches.  third lever (possibly combined with the second lever): alternating and probabilistic models. I will explain how decidability results can be obtained by extending the wellknown equivalence between games and tree automata (that I will recall first!). This will lead us, in several situations, to leave the usual than perfectinformation turn based twoplayer framework: in particular we will have to deal with stochastic aspects and/or imperfect information. 
15:30  Quantitative Automatic Structures SPEAKER: Martin Lang ABSTRACT. see pdf 
14:30  Symbolic Evaluation Graphs and Term Rewriting  A General Methodology for Analyzing Logic Programs SPEAKER: Jürgen Giesl ABSTRACT. There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. 
15:30  Discussion SPEAKER: Everyone ABSTRACT. Discussion on invited talk about "Symbolic Evaluation Graphs and Term Rewriting  A General Methodology for Analyzing Logic Programs". 
14:30  Foundational Proof Certificates SPEAKER: Dale Miller 
15:00  Deduction Modulo SPEAKER: Gilles Dowek 
15:30  Mathematical Proof Analysis SPEAKER: Alexander Leitsch 
14:30  Automated verification of security protocols and services SPEAKER: Michael Rusinowitch ABSTRACT. Cryptographic protocols such as IKE, SET, TLS, Kerberos have been developed to secure electronic transactions. However the design of such protocols often appears to be problematic even assuming that the cryptographic primitives are perfect, i.e. even assuming we cannot decrypt a message without the proper key. An intruder may intercept messages, analyse them, modify them without much ressources and then carry out malevolent actions. This may lead to a variety of attacks such as wellknown ManInTheMiddle attacks. In this setting, the socalled DolevYao model, protocol analysis can be automated by designing suitable symbolic constraint solving techniques. Messages are represented by terms and intruder actions are simulated by deduction rules. It is also possible to somewhat relax the perfect encryption hypothesis by taking into account some algebraic properties of operators. Secrecy and authentification properties, as expected of correct protocol specifications, are verified by showing that no sequence of intruder actions leads to a failure state. We present some applications of the same security protocol analysis techniques to service oriented computing such as the synthesis of a secure composed service and its validation. In this original framework intruder actions are replaced by mediator actions and the failure states are replaced by accepting states for both client and services. 
15:30  Building explicit induction schemas for cyclic induction reasoning SPEAKER: Sorin Stratulat ABSTRACT. In the setting of classical firstorder logic with inductive predicates, two kinds of sequentbased induction reasoning are distinguished: cyclic and structural. Proving their equivalence is of great theoretical and practical interest for the automated reasoning community. It has been shown previously how to transform structural proofs developed with the LKID system into cyclic proofs using the CLKID$^\omega$ system. However, the inverse transformation was only conjectured. We provide a simple procedure that performs the inverse transformation for an extension of LKID with explicit induction rules issued from the structural analysis of CLKID$^{\omega}$ proofs, then establish the equivalence of the two systems. This result is further refined for an extension of LKID with Noetherian induction rules. Based on it, we propose a solution for validating cyclic reasoning by (higherorder) sequentbased systems integrating the Noetherian induction principle, like Coq. 
14:30  Model Checking Parameterized Timed Systems SPEAKER: Francesco Spegni ABSTRACT. In this work we extend the Emerson and Kahlon’s cutoff theorems for process skeletons with conjunctive guards to Parameterized Networks of Timed Automata, i.e. systems obtained by an unbounded number of Timed Automata instantiated from a finite set (U_1 , ..., U_n) of Timed Automata templates. In this way we aim at giving a first tool for universally verifying software systems where an unknown number of software components (i.e. processes) interact with temporal constraints. It is often the case, indeed, that distributed algorithms show an heterogeneous nature, combining dynamic aspects with realtime aspects. In the paper we will also show how to model check a protocol that uses special variables storing identifiers of the participating processes (i.e. PIDs) in Timed Automata with conjunctive guards. This is nontrivial, since solutions to the parameterized verification problem often relies on the processes to be symmetric, i.e. indistinguishable. On the other side, many popular distribute algorithms make use of PIDs and thus cannot directly apply those solutions. 
14:55  Timed Refinements for Verification of RealTime Object Code Programs SPEAKER: Mohana Asha Latha Dubasi ABSTRACT. We introduce a refinementbased notion of correctness for verification of interrupt driven realtime object code programs, called timed refinements. The notion of timed refinements is targeted at verification of lowlevel object code against highlevel specification models. For timed refinements, both the object code (implementation) and the specification are encoded as timed transition systems. Hence, timed refinements can be construed as a notion of equivalence between two timed transition systems that allows for stuttering between the implementation and specification, and also allows for the use of refinement maps. Stuttering is the phenomenon where multiple but finite transitions of the implementation can match a single transition of the specification. Refinement maps allow lowlevel implementations to be verified against highlevel specification models. We also present a procedure for checking timed refinements. The proposed techniques are demonstrated with the verification of object code programs of six case studies from electric motor control applications. 
15:20  Formal Modeling and Verification of CloudProxy SPEAKER: Wei Yang Tan ABSTRACT. Services running in the cloud face threats from several parties, including malicious clients, administrators, and external attackers. CloudProxy is a recentlyproposed framework for secure deployment of cloud applications. In this work, we present the first formal model of CloudProxy, including a formal specification of desired security properties. We model CloudProxy as a transition system in the UCLID modeling language, using termlevel abstraction. Our formal specification includes both safety and noninterference properties. We use induction to prove these properties, employing a backend SMTbased verification engine. Furthermore, we structure our proof as an "assurance case", showing how we decompose the proof into various lemmas, and listing all assumptions and axioms employed. We also perform some limited model validation to gain assurance that the formal model correctly captures all behaviors of the implementation. 
14:30  Laziness is next to Godliness SPEAKER: Peter Stuckey ABSTRACT. Solving combinatorial optimization problems is hard. There are many 
15:30  Lazy Model Expansion: Interleaving Grounding with Search SPEAKER: Bart Bogaerts ABSTRACT. Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state oftheart approach for bounded model generation for rich knowledge representation languages, like Answer Set Programming (ASP), FO(·) and the CSP modeling language Zinc, is groundandsolve: reduce the theory to a ground or propositional one and apply a search algorithm to the resulting theory. An important bottleneck is the blowup of the size of the theory caused by the reduction phase. Lazily grounding the theory during search is a way to overcome this bottleneck. We present a theoret ical framework and an implementation in the context of the FO(·) knowledge representation language. Instead of grounding all parts of a theory, justifications are derived for some parts of it. Given a partial assignment for the grounded part of the theory and valid justifications for the formulas of the nongrounded part, the justifications provide a recipe to construct a complete assignment that satisfies the non grounded part. When a justification for a particular formula becomes invalid during search, a new one is derived; if that fails, the formula is split in a part to be grounded and a part that can be justified. The theoretical framework captures existing approaches for tackling the grounding bottleneck such as lazy clause generation and grounding onthefly, and presents a generalization of the 2watched literal scheme. We present an algorithm for lazy model expansion and integrate it in a model generator for FO(ID), a language extending firstorder logic with inductive definitions. The algorithm is implemented as part of the stateoftheart FO(ID) KnowledgeBase System IDP. Experimental results illustrate the power and generality of the approach.

14:30  A lowlevel treatment of quantifiers in categorical compositional distributional semantics SPEAKER: unknown ABSTRACT. We show how one can formalise quantifiers in the categorical compositional distributional model of meaning. Our model is based on the generalised quantifier theory of Barwise and Cooper. We develop an abstract compact closed semantics and instantiate it in vector spaces and in relations. The former is an example for the distributional corpusbased models of language and the latter for the truththeoretic ones. 
15:00  Divergence in Dialogues SPEAKER: Myriam Quatrini ABSTRACT. This work is part of a project which goal is to understand natural language by taking dialogue as a primitive notion. For this aim, the core of our theoretical framework is a logical theory of interaction, namely Ludics. Ludics is a logical theory developed by J.Y. Girard as an achievement of both proof theoretical and computational theoretical considerations. Above all it is a theory of interaction in the sense that interaction is ontologically the primitive element of Ludics. Ludics being a logical theory, our framework is relevant for grasping logical dimensions of language, especially for studying argumentation but also divergences in dialogue as we show in this paper. In particular complementary aspects of argumentation and divergence in dialogues are modelled in a uniform way: from logics and pragmatics to semantics and syntax. Furthermore we account for several features of dialogues directly at the formal level. Therefore, we may expect a finegrained representation of various dialogical phenomenas. More precisely we illustrate this last point by describing how different divergences in dialogue may be distinguished in our modelling. 
15:30  Modelling implicit dynamic introduction of function symbols in mathematical texts SPEAKER: Marcos Cramer ABSTRACT. The specialized language of mathematics has a number of linguistically and logically interesting features. One of them, which to our knowledge has not been systematically studied before, is the implicit dynamic introduction of function symbols, exemplified by constructs of the form "for every x there is an f(x) such that ...". We present an extension of Groenendijk and Stokhof's Dynamic Predicate Logic  Typed HigherOrder Dynamic Predicate Logic  which formally models this feature of the language of mathematics. Furthermore, we illustrate how the implicit dynamic introduction of function symbols is treated in the proof checking algorithm of the Naproche system. 
14:30  FirstOrder Logics and Truth Degrees SPEAKER: George Metcalfe 
15:30  Classification of germinal MValgebras SPEAKER: Leonardo Manuel Cabrer ABSTRACT. The aim of this paper is to give a complete classification of germinal MValgebras. As an application, we will settle the fifth one of the eleven problems present by Mundici in [D. Mundici, Advanced Łukasiewicz calculus and MValgebras, Trends in Logic, Studia Logica Library. Vol. 35, Springer, Berlin, 2011]. 
14:30  General Panel Discussion SPEAKER: All Workshop Presenters ABSTRACT. This panel discussion be a forum for considering the main issues and future challenges in the domain of parallel search and optimization 
15:30  Towards a complete constraint solver on GPU SPEAKER: unknown ABSTRACT. Constraint programming has gained prominence as an effective and declarative paradigm for modeling and solving complex combinatorial problems. In spite of the natural presence of concurrency, there has been relatively limited effort to use novel massively parallel architecturessuch as those found in modern Graphical Processing Units (GPUs)to speedup constraint programming algorithms. This paper presents an ongoing work for the development of a constraint solver which exploits GPU parallelism. The work is based on two previous results where constraint propagation and approximated search have been parallelized. We summarize these result and discuss the features we have planned to carry on. 
14:30  Application Oriented Low Cost Security Modules SPEAKER: Dan Cvrcek ABSTRACT. Building an HSM out of Smartcards 
15:10  Security APIs for Device Enrolment SPEAKER: Mike Bond ABSTRACT. This talk considers the challenges in designing a Security API for back end systems which enrol devices into a central network, such as a payments network. Since no prior relationship exists with the device, whatever the enrolment protocol, in effect it will reveal keys in clear to the endpoint upon completion. In order to save on database space, key derivation is a common approach in financial organisations, but revelation in clear can be a problem if device keys are derived rather than randomly generated  since the same process could be repeated to reveal the same key with an unwanted party. The talk discusses how to harmonise the desire for secure APIs that support enrolment while minimising storage requirements, and find that parametric API designs (where the API uses a configurable mixture of security mechanisms) can offer a convenient solution  for better or worse  when hammering out a design which will satisfy parties with differing interests within a design team. A parametric design for enrolment is presented and constrasted with previously presented parametric designs for data tokenisation. 
14:30  Gödel FL_0 with Greatest FixedPoint Semantics SPEAKER: Stefan Borgwardt ABSTRACT. We study the fuzzy extension of FL_0 with semantics based on the Gödel tnorm. We show that gfpsubsumption w.r.t. a finite set of primitive definitions can be characterized by a relation on weighted automata, and use this result to provide tight complexity bounds for reasoning in this logic. 
14:55  Fuzzy DLs over Finite Lattices with Nominals SPEAKER: Stefan Borgwardt ABSTRACT. The complexity of reasoning in fuzzy description logics over finite lattices usually does not exceed that of the underlying classical DLs. This has recently been shown for the logics between LIALC and LISCHI using a combination of automata and tableaubased techniques. In this paper, this approach is modified to deal with nominals and constants in LISCHOI. Reasoning w.r.t. general TBoxes is ExpTimecomplete, and PSpacecompleteness is shown under the restriction to acyclic terminologies in two sublogics. The latter implies two previously unknown complexity results for the classical DLs ALCHO and SO. 
15:20  A MILPbased decision procedure for the (Fuzzy) Description Logic ALCB SPEAKER: unknown ABSTRACT. To overcome the inability of Description Logics (DLs) to represent vague or imprecise information, several fuzzy extensions have been proposed in the literature. In this context, an important family of reasoning algorithms for fuzzy DLs is based on a combination of tableau algorithms and Operational Research (OR) problems, specifically using Mixed Integer Linear Programming (MILP). 
15:23  Complexity sources in FDL SPEAKER: Marco Cerami ABSTRACT. In recent years many FDLs based on infinite tnorms have been proved to be undecidable. On the other hand, several FDLs based on finite tnorms, not only have been proved to be decidable, but they have been proved to belong to the same complexity classes as the corresponding crisp DLs. On the light of such results, a question that naturally arises is whether the finitevalued fuzzy framework is really more complex than the old crispvalued formalism. The aim of this work is to analyze some of the complexity sources that are not present in the crisp framework. To this end, we will consider FDL languages with low expressivity that allow us to observe how the need for more complex deciding strategies, not required in the crisp framework, arises in manyvalued FDLs. 
15:26  Gödel Description Logics with General Models SPEAKER: Rafael Peñaloza ABSTRACT. In the last few years, the complexity of reasoning in fuzzy description logics has been studied in depth. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy description logics using the Gödel tnorm. It was recently shown that in the logic GIALC under witnessed model semantics, all standard reasoning problems can be solved in exponential time, matching the complexity of reasoning in classical ALC. We show that this also holds under general model semantics. 
15:29  Certain Answers in a Rough World SPEAKER: Veronika Thost ABSTRACT. Rough Description Logics have recently been studied as a means for representing and reasoning with imprecise knowledge. Realworld applications need to exploit reasoning over such knowledge in an efficient way. We describe how the combined approach to query answering can be extended to the rough setting. In particular, we extend both the canonical model and the rewriting procedure such that rough queries over rough EL ontologies can be answered by considering this information alone. 
15:32  Bayesian Description Logics SPEAKER: Ismail Ilkan Ceylan ABSTRACT. We present Bayesian Description Logics (BDLs): an extension of Description Logics with contextual probabilities encoded in a Bayesian network (BN). Classical DL reasoning tasks are extended to consider also the contextual and probabilistic information in BDLs. A complexity analysis of these problems shows that, for propositionally closed DLs, this extension comes without cost, while for tractable DLs the complexity is affected by the cost of reasoning in the BN. 
15:35  Reasoning about Belief Uncertainty in DLLite N bool SPEAKER: Ala Djeddai ABSTRACT. Dealing with uncertainty is a very important issue in description logics (DLs). In this paper, we present PrDLlite N bool a new probabilistic extension of DLLite N bool, known as a very expressive DLLite, by supporting the belief degree interval in a single axiom or a set of axioms connected with conjunction (by ∧) or disjunction (by ∨) operators. The PrDLlite N bool semantics is based on DLLite N bool features which are a new alternative semantics for DLlite N bool having a finite structure and its number is always finite unlike classical models. PrDLlite N bool also supports terminological and assertional probabilistic knowledge and the reasoning tasks (satisfiability, deciding the entailment, computing tight interval for entailment) are achieved by solving linear optimization problems. A prototype of the approach is implemented using OWLAPI for knowledge base creation, Pellet for reasoning and LpSolve for solving the linear programs. 
15:38  Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information SPEAKER: Federico Cerutti ABSTRACT. This paper investigates how to restrict the spread of sensitive information. This work is situated in a military context, and provides a tractable method to decide what semantic information to share, with whom, and how. The latter decision is supported by obfuscation, where a related concept or fact may be shared instead of the original. We consider uncertain information, and utilise Subjective Logic as an underlying formalism to further obfuscate concepts, and reason about obfuscated concepts. 
15:41  Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure? SPEAKER: Tahani Alsubait ABSTRACT. Several attempts have been made to develop similarity measures for ontologies. Motivated by finding problems in existing measures, we design a new family of measures to address these problems. We carry out two sets of empirical studies. Firstly, to explore how good the new measures are by comparing them to human judgments of similarity. Secondly, we investigate how likely it is to encounter specific taskoriented problems when using a bad similarity measure. 
15:44  Mary, What's Like All Cats? SPEAKER: unknown ABSTRACT. In Description Logics (DL) knowledge bases (KBs) information is typically captured by crisp concepts. For many applications querying the KB by crisp query concepts is too restrictive. A controlled way of gradually relaxing a query concept can be achieved by the use of concept similarity. We formalize the task of instance query answering for crisp DL KBs using concepts relaxed by concept similarity measures (CSM). For the DL EL we investigate computation algorithms for this task, their complexity and properties for the employed CSM in case unfoldable TBoxes or general TBoxes are used. 
14:30  Proofsearch in natural deduction calculi for IPL SPEAKER: Camillo Fiorentini ABSTRACT. We address the problem of proofsearch in the natural deduction calculus Ni for intuitionistic propositional logic (IPL). Our aim is to improve the usual n\"aive proofsearch procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Nbu, a sequentstyle variant of Ni and we show that its derivations can be reduced in $\theta$NF, a normal form (stronger than the usual one) where applications of $\lor E$ and $\to I$ satisfy additional conditions involving an evaluation relation $\theta$. This limits the application of such rules in proofsearch and restricts the search space. 
15:15  A joint logic of problems and propositions, a modified BHKinterpretation and proofrelevant topological models of intuitionistic logic SPEAKER: Sergey Melikhov ABSTRACT. In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper ("Zur Deutung der intuitionistischen Logik") "was written in hope that with time, the logic of solution of problems will become a permanent part of [a standard] course of logic. Creation of a unified logical apparatus dealing with objects of two types  propositions and problems  was intended." We describe such a formal system, QHC, which is a conservative extension of both the intuitionistic predicate calculus, QH, and the classical predicate calculus, QC. Moreover:  The only new connectives ? and ! of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC, regarded as posets.  Kolmogorov's double negation translation of propositions into problems extends to a retraction of QHC onto QH.  Goedel's provability translation of problems into modal propositions extends to a retraction of QHC onto its QC+(?!) fragment, which can be identified with the modal logic QS4. This leads to a new paradigm that views intuitionistic logic not as an alternative to classical logic that criminalizes some of its principles, but as an extension package that upgrades classical logic without removing it. The purpose of the upgrade is proofrelevance, or "categorification"; thus, if the classical conjunction and disjunction are to be modeled by intersection and union (of sets), the intuitionistic conjunction and disjunction will be modeled by product and disjoint union (of sheaves of sets). More formally, we describe a family of sheafvalued models of QH, inspired by dependent type theory (not to be confused with the wellknown open setvalued sheaf models of QH), which can be regarded as proofrelevant analogues of classical topological models of Tarski et al., and which extend to models of QHC. We also give an interpretation of some of these models in terms of stable solutions of algebraic equations; this can be seen as a proofrelevant counterpart of Novikov's classical interpretation of some Tarski models in terms of weighting of masses. The new paradigm also suggests a rethink of the BrouwerHeytingKolmogorov interpretation of QH. Traditional ways to understand intuitionistic logic (semantically) have been rooted either in philosophy  with emphasis on the development of knowledge (Brouwer, Heyting, Kripke) or in computer science  with emphasis on effective operations (Kleene, Markov, MartinLoef). Our "modified BHK interpretation" is rooted in the usual mathematical ideas of canonicity and stability; it emphasizes simply the order of quantifiers, developing Kolmogorov's original approach. This interpretation is compatible with two complete classes models of QH: (i) Tarski topological models and (ii) settheoretic models of MedvedevSkvortsov and Laeuchli; as well as with (iii) our sheafvalued models. 
14:30  Using Interpolation for the Verification of Security Protocols (Extended Abstract) SPEAKER: Luca Viganò ABSTRACT. Interpolation has been successfully applied in formal methods for model checking and testcase generation for sequential programs. Security protocols, however, exhibit such idiosyncrasies that make them unsuitable to the direct application of such methods. In this paper, we address this problem and present an interpolationbased method for security protocol verication. Our method starts from a formal protocol specication and combines Craig interpolation, symbolic execution and the standard DolevYao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. We illustrate an implementation of our method and its application to concrete examples. 
15:00  Interpolation Strategies SPEAKER: Kenneth McMillan ABSTRACT. We consider some of the issues and tradeoffs in computing useful interpolants in practice, including questions of proof search strategy, proof translation vs. local proof and interpolant optimization. These issues are explored empirically using the Duality fixed point engine as a platform and benchmark problems from software model checking. 
15:30  Towards Craig Interpolation for String Constraints SPEAKER: unknown ABSTRACT. The problem of reasoning automatically about string formulae, containing constraints such as string/word equations, regular language membership, or length restrictions, has increasingly received attention over the past years. Much of the existing work has concentrated on checking satisfiability of string formulae, by means of translation to bitvector formulae or analysis of finite automata representations, among others. We report about ongoing research on Craig interpolation for string formulae, done in the context of work presented in our CAV’14 paper. 
14:30  Adversary Gain vs. Defender Loss in Quantified Information Flow SPEAKER: Piotr Mardziel ABSTRACT. Metrics for quantifying information leakage assume that an adversary’s gain is the defender’s loss. We demonstrate that this assumption does not always hold via a class of scenarios. We describe how to extend quantification to account for a defender with goals distinct from adversary failure. We implement the extension and experimentally explore the impact on the measured information leakage of the motivating scenario. 
15:00  Generalizing PermissiveUpgrade in Dynamic Information Flow Analysis SPEAKER: unknown ABSTRACT. Preventing implicit information flows by dynamic program analysis requires coarse approximations that result in false positives, because a dynamic monitor sees only the executed trace of the program. One widely deployed method is the nosensitiveupgrade check, which terminates a program whenever a variable's taint is upgraded (made more sensitive) due to a control dependence. Although sound, this method is impermissive, e.g., it terminates the program even if the upgraded variable is never used subsequently. To counter this, Austin and Flanagan introduced the permissiveupgrade check, which allows a variable upgrade due to control dependence, but marks the variable "partiallyleaked". The program is stopped later if it tries to use (caseanalyze) the partiallyleaked variable. Permissiveupgrade handles the deadvariable assignment problem and remains sound. However, Austin and Flanagan develop permissiveupgrade only for a twopoint (lowhigh) security lattice and indicate a generalization to pointwise products of such lattices. In this paper, we develop a nontrivial and nonobvious generalization of permissiveupgrade to arbitrary lattices. The key difficulty lies in finding a suitable notion of partial leaks that is both sound and permissive and in developing a suitable definition of memory equivalence that allows an inductive proof of soundness. 
15:30  MicroPolicies: Formally Verified LowLevel Tagging Schemes for Safety and Security (Short Paper) SPEAKER: Catalin Hritcu ABSTRACT. Today's computer systems are distressingly insecure. A host of vulnerabilities arise from the violation of known, but inpractice unenforceable, safety and security policies, including highlevel programming models and critical invariants of lowlevel programs. This project is aimed at showing that a rich and valuable set of _micropolicies_ can be efficiently enforced by a new generic hardwaresoftware mechanism and result in more secure and robust computer systems. In particular we aim to come up with a clean formal framework in Coq for expressing, composing, and verifying arbitrary micropolicies, and to instantiate this framework on a diverse set of interesting examples. 
14:30  Structural Decomposition Methods: How They Matter SPEAKER: Georg Gottlob ABSTRACT. This talk is based on the published paper [Aschinger, Drescher, Gottlob, Jeavons, and Thorstensen, STACS 2011]. We review structural problem decomposition methods, such as tree and path decompositions. It is argued that these notions can be applied in two distinct ways: Either to show that a problem is efficiently solvable when a width parameter is fixed, or to prove that the unrestricted (or some widthparameter free) version of a problem is tractable by using a widthnotion as a mathematical tool for directly solving the problem at hand. Examples are given for both cases, and the refined taxonomy below is illustrated. When we speak about the treewidth of a problem instance, we mean the treewidth of some graph associated with the instance. Obviously, for each concrete problem, one has to indicate what this graph is, and, whenever necessary, how it can be obtained from the instance. Taxonomy: 
14:30  The Social Engineering Personality Framework SPEAKER: unknown ABSTRACT. We explore ICT security in a sociotechnical world and focus in particular on the susceptibility to social engineering attacks. We pursue the question if and how personality traits influence this susceptibility. We use Cialdini's principles of influence to categorise social engineering attacks. With a comprehensive literature review we first show how existent research approaches social engineering susceptibility. Based on this review we construct suggestions for plausible relations between personality traits of the FiveFactor Model (Big 5) and the principles of influence. We propose our – at this stage theorybased – "Social Engineering Personality Framework" (SEPF) which we will evaluate in future empiric research. The characteristics of victims' personality traits in the SEPF will support and guide security researchers and practitioners in developing detection, mitigation, and prevention strategies while dealing with human factors in social engineering attacks. 
15:15  Modeling Human Behaviour with Higher Order Logic: Insider Threats SPEAKER: Florian Kammueller ABSTRACT. In this paper, we approach the problem of modeling the human component in technical systems with a view on the difference between the use of model and theory in sociology and computer science. One aim of this essay is to show that building of theories and models for sociology can be compared and implemented in Higher Order Logic. We validate this working hypothesis by revisiting Weber's understanding explanation. We focus on constructive realism in the context of logical explanation. We review Higher Order Logic (HOL) as a foundation for computer science and summarize its use of theories relating it to the sociological process of logical explanation. As a case study on modeling human behaviour, we present the modeling and analysis of insider threats as a Higher Order Logic theory in Isabelle/HOL. We show how each of the three step process of sociological explanation can be seen in our modeling of insider's state, its context within an organisation and the effects on security as outcomes of a theorem proving analysis. 
14:30  Decidability of Iterationfree PDL with Parallel Composition SPEAKER: Joseph Boudou ABSTRACT. PRSPDL is a highly undecidable propositional dynamic logic with an operator for parallel composition of programs. This operator has a separation semantic such that a multiplicative conjunction similar to the one found in the logic of Boolean bunched implications is definable. The present work identifies an iterationfree decidable fragment of PRSPDL in which the multiplicative conjunction is still definable. A NEXPTIME complexity upper bound for the fragment is given. 
15:00  Axiomatic and TableauBased Reasoning for Kt(H,R) SPEAKER: Renate A. Schmidt ABSTRACT. We introduce a tense logic, called Kt(H,R), arising from logics for spatial reasoning. Kt(H,R) is a multimodal logic with two modalities and their converses defined with respect to a preorder and a relation stable over this preorder. We show Kt(H,R) is decidable, it has the effective finite model property and reasoning in Kt(H,R) is PSPACEcomplete. Two complete Hilbertstyle axiomatisations are given. The main focus of the paper is tableaubased reasoning. Our aim is to gain insight into the numerous possibilities of defining tableau calculi and their properties. We present several labelled tableau calculi for Kt(H,R) in which the theory rules range from accommodating correspondence properties closely, to accommodating Hilbert axioms closely. The calculi provide the basis for decision procedures that have been implemented and tested on modal and intuitionistic problems. Though the focus is on Kt(H,R), the techniques and ideas used in this research are of general nature and provide a useful methodology for developing practical decision procedures for modal logics, which we will discuss. 
15:30  On dual tableaubased decision procedures for relational fragments SPEAKER: unknown ABSTRACT. We give a brief survey of the main results on dual tableaubased decision procedures for fragments of the logic of binary relations and we outline our current work in the design of relational decision procedures for logics for orderofmagnitude reasoning. Then we shortly hint at some further research plans on other relational decision procedures. 
14:30  Epsilonsemantics and hybrid automata SPEAKER: Tommaso Dreossi ABSTRACT. Hybrid automata are mathematical model designed to describe systems characterized by mixed discretecontinuous behaviours. Standard semantics defined over hybrid automata implicitly assume perfect knowledge of the observed systems and infinite precision measurements. In the biological context these assumptions are unrealistic and often lead to unfaithful models. From these observations, we introduce a family of more flexible semantics, the εsemantics, able to handle noise, partial information, and finite precision.
In this presentation we study the relationship between εsemantics and standard semantics over first order formulae used to construct logicbased hybrid automata. Under this framework, we present a decidability result concerning the reachability problem. Finally, we consider some biological models and show the qualitative benefits brought by the εsemantics application. 
15:00  Verifying FloatingPoint Implementations of Nonlinear Functions SPEAKER: Sicun Gao ABSTRACT. We are developing a new approach for debugging and verifying floatingpoint implementations of nonlinear functions. Our method combines testing, numerical analysis, and deltacomplete SMT solving using dReal. We generate point inputs to obtain preliminary coverage, and then generalize them to an automatically chosen neighborhood based on static analysis. In this way we often obtain full coverage of bounded intervals of interest in reasonable amount of time. Applying the techniques on the current version of the Embedded GNU C library, we have found serious bugs in the implementations of elementary functions, as well as intervals where their correctness is verified. 
15:30  Correctness of Parallel Interval Computations SPEAKER: Philippe Theveny ABSTRACT. Interval computations are a means to guarantee a possible range of a numerical result computed with finite precision numbers. With a parallel implementation, the nondeterminism of the execution order, which hinders the reproducibility of numerical result from one run to the other, may also affect the correctness of an interval algorithm. In addition, implementations of interval algorithms depend on the respect of the rounding mode by the software stack: from the compiler to the thread manager. The talk illustrates these pitfalls with the parallel implementation of interval matrix multiplications. 
14:30  TBA SPEAKER: Thomas C. Hales 
15:00  Mixing proofs and computations SPEAKER: Michael Beeson ABSTRACT. In order to achieve the goals of QED, it will be necessary to effectively combine calculations and proofs in the same formal and computerized representation. We discuss the obstacles to this combination, and some of the attempts to overcome those obstacles. 
15:30  The Naproche system: Proofchecking mathematical texts in controlled natural language SPEAKER: Marcos Cramer ABSTRACT. We have developed a controlled natural language (CNL) – i.e. a subset of a natural language defined through a formal grammar – for writing mathematical texts. The Naproche system can check the correctness of mathematical proofs written in this CNL. In this talk we will highlight some interesting logical and linguistic problems that had to be solved in the development of the Naproche CNL and the Naproche system: The system uses a formalism from the linguistic theory of presuppositions in order to work with potentially undefined terms, and can handle dynamic quantification, including the phenomenon of implicit dynamic function introduction, which had previously not been discussed in the literature. 
14:30  Weak well orders and related inductions SPEAKER: Gerhard Jaeger ABSTRACT. It is an interesting program to investigate the relationship between the proof theory of second order arithmetic and more general second order systems (e.g. theories of sets and classes such as von NeumannBernaysGoedel set theory and MorseKelley set theory). Which prooftheoretic results can be lifted from second order arithmetic to theories of sets and classes, for which is this not the case, and what are the reasons? What is specific of second order number theory and what additional insights can we gain? One of the crucial questions is how to distinguish between "small" and "large" in the various contexts. In second order arithmetic, the small objects are the natural numbers whereas the large objects are the infinite sets of natural numbers. Hence it seems natural to identify the small objects in sets and classes with sets and the large objects with proper classes. As long as only comparatively weak systems are concerned, the moving up from second order arithmetic to sets and classes seems to be a matter of routine. However, as soon as well orderings enter the picture, the situation becomes interesting. In second order arithmetic, every $\Pi^1_1$ statement is equivalent to the question whether a specific arithmetic relation is well ordered; on the other hand, in set theory a simple elementary formulas expresses the well foundedness of a given relation. We propose studying the (new) notion of weak well order in sets and classes as the prooftheoretically adequate analogue of well order in second order arithmetic. To support this claim several results about inductions and recursions in connection with weak well orders will be presented. This is joint work with D. Flumini. 
15:15  Automating inductive proof SPEAKER: Alan Bundy ABSTRACT. We discuss the automation of inductive proof. 
14:30  Automatic Detection of Webpage Candidates for SiteLevel Web Template Extraction SPEAKER: Josep Silva 
14:30  Analysis of Dialogical Argumentation via Finite State Machines SPEAKER: Anthony Hunter ABSTRACT. Dialogical argumentation is an important cognitive activity by which agents exchange arguments and counterarguments as part of some process such as discussion, debate, persuasion and negotiation. Whilst numerous formal systems have been proposed, there is a lack of frameworks for implementing and evaluating these proposals. Firstorder executable logic has been proposed as a general framework for specifying and analysing dialogical argumentation. In this paper, we investigate how we can implement systems for dialogical argumentation using propositional executable logic. Our approach is to present and evaluate an algorithm that generates a finite state machine that reflects a propositional executable logic specification for a dialogical argumentation together with an initial state. We also consider how the finite state machines can be analysed, with the minimax strategy being used as an illustration of the kinds of empirical analysis that can be undertaken. 
15:00  Abduction in Argumentation: Dialogical Proof Procedures and Instantiation SPEAKER: unknown ABSTRACT. We develop a model of abduction in abstract argumentation, where changes to an argumentation frame work act as hypotheses to explain the support of an observation. We present dialogical proof theories for the main decision problems (i.e., finding hypotheses that explain skeptical/credulous support) and we show that our model can be instantiated on the basis of abductive logic programs. 
15:30  NonMonotonic Reasoning and Story Comprehension SPEAKER: unknown ABSTRACT. This paper develops a Reasoning about Actions and Change framework integrated with Default Reasoning, suitable as a Knowledge Representation and Reasoning framework for Story Comprehension. The proposed framework, which is guided strongly by existing knowhow from the Psychology of Reading and Comprehension, is based on the theory of argumentation from AI. It uses argumentation to capture appropriate solutions to the frame, ramification and qualification problems and generalizations of these problems required for text comprehension. In this first part of the study the work concentrates on the central problem of integration (or elaboration) of the explicit information from the narrative in the text with the implicit (in the reader’s mind) common sense world knowledge pertaining to the topic(s) of the story given in the text. We also report on our empirical efforts to gather background common sense world knowledge used by humans when reading a story and to evaluate, through a prototype system, the ability of our approach to capture both the majority and the variability of understanding of a story by the human readers in the experiments. 
15:30  Backdoors into Heterogeneous Classes of SAT and CSP SPEAKER: Sebastian Ordyniak ABSTRACT. Backdoor sets represent clever reasoning shortcuts through the search space for SAT and CSP. By instantiating the backdoor variables one reduces the given instance to several easy instances that belong to a tractable class. The overall time needed to solve the instance is exponential in the size of the backdoor set, hence it is a challenging problem to find a small backdoor set if one exists; over the last years this problem has been subject of intensive research. In this paper we extend the classical notion of a strong backdoor set by allowing that different instantiations of the backdoor variables result in instances that belong to different base classes; the union of the base classes forms a heterogeneous base class. Backdoor sets to heterogeneous base classes can be much smaller than backdoor sets to homogeneous ones, hence they are much more desirable but possibly harder to find. We draw a detailed complexity landscape for the problem of detecting strong backdoor sets into heterogeneous base classes for SAT and CSP. We provide algorithms that establish fixedparameter tractability under natural parameterizations, and we contrast the tractability results with hardness results that pinpoint the theoretical limits. Our results apply to the current stateoftheart of tractable classes of CSP and SAT that are definable by restricting the constraint language. 
16:30  Asynchronous interaction for Coq SPEAKER: Carst Tankink ABSTRACT. In this talk I will discuss the new jEdit editor integration for Coq, that supports asynchronous interaction with the proof assistant. 
17:00  Coqoon: towards a modern IDE for Coq SPEAKER: Alexander Faithfull ABSTRACT. Users of modern IDEs expect sophisticated features like automatic dependency resolution, background recompilation, contentaware search features (such as "show me where this is defined"), automatic indentation, syntax highlighting and code completion. Coqoon, which is built on top of the Eclipse platform, provides such an IDE for Coq. 
17:30  Update on Coq 8.5 SPEAKER: Matthieu Sozeau 
16:30  Hardware Model Checking (Part B) SPEAKER: Fabio Somenzi 
16:30  Citations for the TestofTime Award from 1994 SPEAKER: Dexter Kozen 
16:30  Answer Set Programming II SPEAKER: Martin Gebser 
18:30  Summer School Closing SPEAKER: Gopal Gupta 
16:30  Semantic Types for Classes and Mixins SPEAKER: unknown ABSTRACT. We consider a formalization of mixins composition and class linearization yielding a class in mixinbased inheritance. We provide an interpretation of the mixin calculus into a lambdacalculus extended with records and a record merge operator. After extending the BCD intersection type assignment to such calculus showing that types are preserved by subject expansion and reduction, we naturally interpret mixin terms as the sets of the types that can be deduced of their translations. It turns out that the class obtained from a composition of mixins and the composition itself have the same logical meaning. 
17:00  Delegationbased Mixin Composition Synthesis SPEAKER: Andrej Dudenhefner ABSTRACT. In the object oriented world existing inheritance concepts have been extended by mixins to assist modular software design. Actually, most languages only have limited mixin support. We use staged computation proposed by Davies and Pfenning together with a specification following an interface based design pattern to introduce mixins to Java 8. We present a synthesis based approach for mixin composition guided by user annotated semantics translated to intersection types. Synthesis results in meaningful Java code utilizing delegation to augment existing classes with mixin features. 
16:30  Restrictiveness relative to notions of interpretation SPEAKER: Luca Incurvati ABSTRACT. In [4], Maddy gives a semiformal account of restrictiveness by defining a corresponding formal notion based on a class of interpretations. In [2] and [3], Maddy's notion of restrictiveness was discussed and the theory ZF + `Every uncountable cardinal is singular' was presented as a potential witness to the restrictiveness of ZFC. More recently, Hamkins has given more examples and pointed out some structural issues with Maddy's definition [1]. We look at Maddy's definitions from the point of view of an abstract interpretation relation. We consider various candidates for this interpretation relation, including one that is close to Maddy's original notion, but fixes the issues raised in [1]. Our work brings to light additional structural issues that we also discuss. 
17:15  Reflection, Trust, Entitlement SPEAKER: Leon Horsten ABSTRACT. It has been argued by Feferman and others that when we accept a mathematical theory, we implicitly commit ourselves to reflection principles for this theory. When we reflect on this implicit commitment, we come to explicitly believe certain reflection principles. In my talk I will discuss our epistemic warrant for this resulting explicit belief in reflection principles. 
16:30  Definable valuation rings SPEAKER: Jochen Königsmann 
17:15  The Fitting subgroup of a supersimple group SPEAKER: Daniel Palacín 
16:30  Discussion and Business Meeting SPEAKER: Everyone 
16:30  Efficiently Solving Quantified BitVectors SPEAKER: Christoph Wintersteiger ABSTRACT. There is great interest in the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifierfree fragment of bitvector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bitvector formulas to avoid an exponential blowup during construction and QBF solvers are often inefficient. I will present an approach based on a set of effective wordlevel simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on function templates. I will also go into why we got interested in this problem in the first place and where we would like to take it from here. 
17:00  Quantifier Projection SPEAKER: Nikolaj Bjorner ABSTRACT. We take as starting point routines for quantifier reasoning in the SMT solver Z3 and we analyze these through the lens of quantfier projection: quantifiers are specialized or instantiated partially using information about possible feasible interpretations that is collected during search. 
17:30  Finding Conflicting Instances of Quantified Formulas in SMT SPEAKER: Andrew Reynolds ABSTRACT. Modern SMT solvers primarily rely on heuristic methods such as Ematching for answering ``unsatisfiable" in the presence of quantified formulas. The success of these solvers is often hindered by an overabundance of instantiations produced by these heuristics, making it difficult for the solver to continue its operation. In this paper, we introduce new techniques that alleviate this shortcoming by first discovering instantiations that are in conflict with the current state of the solver. In these techniques, the solver only resorts to heuristic methods when such an instantiation cannot be found, thus decreasing its dependence upon Ematching. Our experimental results show our technique significantly reduces the number of instantiations required by the SMT solver for answering ``unsatisfiable" for several benchmark libraries, and consequently leads to improvements over stateoftheart implementations. 
16:30  Simulation for infinite state systems. SPEAKER: Piotr Hofman ABSTRACT. Abstract is in the pdf file. My submission is quiet unusual, as I propose 2 topics (closely related). I hope that one of them will suit to this year AISS programme. 
17:30  Simulation Over OneCounter Nets is PSPACEComplete SPEAKER: Patrick Totzke ABSTRACT. Onecounter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of onecounter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACEcomplete. 
16:30  Intelligent Visual Surveillance Logic Programming: Implementation Issues SPEAKER: Alexei A. Morozov ABSTRACT. The main idea of the logic programming approach to the intelligent video surveillance is in using a first order logic for describing complex events and abstract concepts like anomalous human activity, i.e. brawl, sudden attack, armed attack, leaving object, loitering, pick pocketing, personal theft, immobile person, etc. We consider main implementation issues of our approach to the intelligent video surveillance logic programming: objectoriented logic programming of concurrent stages of video processing, translating video surveillance logic programs to fast Java code, embedding lowlevel means for video storage and processing to the logic programming system. 
17:00  A Parallel Virtual Machine for Executing ForwardChaining Linear Logic Programs SPEAKER: Flavio Cruz ABSTRACT. Linear Meld is a concurrent forwardchaining linear logic programming language where logical facts can be asserted and retracted in a structured way. The database of facts is partitioned by the nodes of a graph structure which leads to parallelism if nodes are executed simultaneously. Communication arises whenever nodes send facts to other nodes by fact derivation. We present an overview of the virtual machine that we implemented to run Linear Meld on multicores, including code organization, thread management, rule execution and database organization for efficient fact insertion, lookup and deletion. Although our virtual machine is a workinprogress, our results already show that Linear Meld is not only capable of scaling graph and machine learning programs but it also exhibits some interesting performance results when compared against other programming languages. 
17:30  Discussion SPEAKER: Everyone ABSTRACT. We have additional discussion time at the end of the workshop. 
16:30  Program Verification (B Method) SPEAKER: JeanRaymond Abrial 
17:00  Security SPEAKER: Gilles Barthe 
17:30  Deep Inference SPEAKER: Alessio Guglielmi 
16:30  The DFLAT System for Dynamic Programming on Tree Decompositions SPEAKER: Stefan Woltran ABSTRACT. Complex reasoning problems over large amounts of data pose a great challenge for computer science. To overcome the obstacle of high computational complexity, exploiting structure by means of tree decompositions has proved to be effective in many cases. However, the implementation of suitable efficient algorithms is often tedious. DFLAT is a software system that combines the logic programming language Answer Set Programming with problem solving on tree decompositions and can serve as a rapid prototyping tool for such algorithms. Since we initially proposed DFLAT, we have made major changes to the system, improving its range of applicability and its usability. In this paper, we present the system resulting from these efforts. 
17:10  CrossTranslating Answer Set Programs SPEAKER: Tomi Janhunen ABSTRACT. Answer set programming (ASP) is a declarative programming paradigm where computation takes place in two phases. The rules of a logic program are first instantiated after which the answer sets of the resulting ground program are computed. There are two mainstream approaches to the search for answer sets: either by using native answer set solvers or by translating ground rules into other kinds of constraints and using other offtheshelf solver technology to perform the search. Over the years, we have developed a number of translations from ASP to Boolean satisfiability (SAT), difference logic, bitvector logic, and mixed integer programming. If a target formalism does not support extended rule types, they have to be normalized before translation. Our latest translation of ASP into SAT modulo acyclicity enables a crosscompilation architecture where the backend formalism is determined by the last translation step generating Clark’s completion extended by acyclicity constraints. In this invited talk, I describe the resulting crosstranslation framework for ASP and discuss lessons learned from the tenyear development of the framework.

16:30  Program Extraction Applied to Monadic Parsing SPEAKER: Alison Jones ABSTRACT. This paper outlines a prooftheoretic approach to developing correct and terminating monadic parsers. Using a modified realisability interpretation, we extract provably correct and terminating programs from formal proofs. If the proof system is proven to be correct, then any extracted program is guaranteed to be so. By extracting parsers, we can ensure that they are correct, complete and terminating for any input. The work is ongoing, and is being carried out in the interactive proof system M\textsc{inlog}. 
17:00  On Translating ContextFree Grammars into Lambek Categorial Grammars SPEAKER: Stepan Kuznetsov ABSTRACT. We modify Buszkowski's translation of contextfree grammars to Lambek categorial grammars in order to deal with Montaguestyle semantics properly. 
16:30  Cutfree calculus for secondorder {G\"odel} logic SPEAKER: unknown ABSTRACT. We prove that the extension of the known hypersequent calculus for standard firstorder {G\"odel} logic with usual rules for secondorder quantifiers is sound and (cutfree) complete for Henkinstyle semantics for secondorder {G\"odel} logic. The proof is semantic, and it is similar in nature to {Sch\"utte} and Tait's proof of Takeuti's conjecture. 
17:00  Poof Search and CoNP completeness for ManyValued Logics SPEAKER: unknown ABSTRACT. We provide a methodology to introduce relational hypersequent calculi for a large class of manyvalued logics, and a sufficient condition for their CoNP completeness. Our results include the most important CoNP fuzzy logics. 
17:30  Cut and completion? SPEAKER: Sam van Gool ABSTRACT. During the last decade a connection emerged between proof theory and algebra via which cutelimination, one of the cornerstones of structural proof theory, can be proved by using completions, in particular, the MacNeille completion. This technique, which has been developed for a wide range of logics, including substructural ones, is far from trivial. Our modest aim in this paper is to establish what the technique of completions boils down to for "strong" logics such as full intuitionistic propositional logic, and what the connection is with other semantical proofs of cutelimination. 
16:30  Definability of truth predicates in abstract algebraic logic SPEAKER: Tommaso Moraschini ABSTRACT. One of the main topics of Abstract Algebraic Logic is the study of the Leibniz hierarchy, in which logics are classified by means of properties of the Leibniz operator which determine how nicely the Leibniz congruences and the truth predicates can be described in models of the logic. In this talk we will introduce and characterize logics, whose truth predicates are defined by means of equations with parameters. Then we will go through the consideration of weaker conditions on the truth predicates of a logic. This will give rise to a small hierarchy, in which logics are classified according to the way their truth predicates are defined; this new hierarchy can be thought of as an extension of the Leibniz hierarchy, since almost all the conditions we take into account turn out to be characterised by a property of the Leibniz operator. 
17:00  Generalizing the Leibniz and Suszko operators SPEAKER: Hugo Albuquerque ABSTRACT. In this paper we study the notion of an Scoherent family of Scompatibility operators, for a sentential logic S. This notion is tailored to be a common generalization of the wellknown Leibniz and Suszko operators, which have been fundamental tools in recent developments of Abstract Algebraic Logic. The first main result we prove is a General Correspondence Theorem, which generalizes several results of this kind obtained for either the Leibniz operator (Blok and Pigozzi, 1986; Font and Jansana, 2001) or the Suszko operator (Czelakowski, 2003). We apply the general results to obtain several new characterizations of the main classes of logics in the Leibniz hierarchy in terms of the Leibniz operator or in terms of the Suszko operator. 
17:30  Churchstyle type theories over finitary weakly implicative logics SPEAKER: Libor Behounek ABSTRACT. In this paper, ChurchHenkin simple type theories are constructed for finitary weakly implicative logics. The resulting type theory TT(L) over a given finitary weakly implicative logic L is the minimal (extensional, substitutioninvariant) type theory closed under the rules of lambdaconversion and the intersubstitutivity of equals whose propositional fragment coincides with L and whose sound and complete Henkin semantics consists of Henkinstyle general models over a generating class of Lalgebras. The soundness and completeness theorem for TT(L) is obtained by a schematic adaptation of the proof for the ground theory TT0 which is a common fragment of all TT(L). 
16:30  Protocol Indistinguishability and the Computationally Complete Symbolic Attacker SPEAKER: unknown ABSTRACT. We considered the problem the computational indistinguishability of two bounded protocols. We designed a symbolic model that is amenable to automated deduction, and such that an inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. The idea is to define a computationally complete symbolic attacker in order to achieve unconditional computational soundness of the symbolic analysis. Following our previous work on reachability properties, we achieve this by axiomatizing what an attacker cannot violate. By adding computationally sound, modular axioms, a library of axioms can be built. Despite additional difficulties stemming from equivalences, the models and proofs are much simpler than in the case of reachability properties. 
16:50  On WellFounded Security Protocols SPEAKER: Sibylle Froeschle ABSTRACT. We introduce the class of wellfounded protocols, and explain why leakiness is decidable for it. We hope that this will help to unify our understanding of a group of results that obtain decidability by imposing conditions that make encrypted messages contextexplicit. 
17:10  Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model SPEAKER: unknown ABSTRACT. We explain the connection between Fitting's embedding of classical logic in S4 and the nonTarskian computational semantics that Bana and Comon defined to interpret firstorder formulas for their computationally complete symbolic attacker. 
17:30  Towards Timed Models for CyberPhysical Security Protocols SPEAKER: unknown ABSTRACT. Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as cyberphysical. The key elements of such protocols are the use of cryptographic keys, nonces and time. This paper investigates timed models for the verification of such protocols. Firstly, we introduce a multiset rewriting framework with continuous time and fresh values. We demonstrate that in this framework one can specify distance bounding protocols and intruder models for cyberphysical security protocols that take into account the physical properties of the environment. Then we prove that models with discrete time are not able to expose as many security flaws as models with continuous time. This is done by proposing a protocol and demonstrating that there is no attack to this protocol when using the model with discrete time, but there is an attack when using the model with continuous time. For the important class of Bounded Memory CyberPhysical Security Protocols with a Memory Bounded Intruder the reachability problem is PSPACEcomplete if the size of terms is bounded. 
16:30  What You Enter Is What You Sign: input integrity in an online banking environment SPEAKER: Sven Kiljan ABSTRACT. One problem with most currently used transaction authentication methods is that they depend on the customer's computer for integrity of the information flow between customer and bank. This allows maninthemiddle attacks to be conducted using malware for financial fraud. Some banks are implementing new authentication methods that allow customers to verify transactions received by a bank without depending on the customer's computer to provide information integrity. These new methods are more complex compared to traditional authentication methods and need the customer's attention to be effective, since it is up to the customer to verify the information that was received by his or her bank. By examining the intrinsic problems of traditional and new transaction authentication methods as used by banks, we designed an alternative authentication method named 'Entered Single Transaction Authentication'. Our method ensures that the bank receives information as the customer entered it without requiring further verification by the customer. We introduce the concept 'What You Enter Is What You Sign', which ensures the digital integrity of information as soon as it is entered. Our proposal is theoretical and highlevel, but opens the way for secure transaction authentication methods that rely less on the authenticating party to provide correct information, thereby reducing errors and improving user friendliness. 
17:15  Using Statistical Information to Communicate Android Permission Risks to Users SPEAKER: Lydia Kraus ABSTRACT. The Android OS has a permissionbased security system that controls the third party applications’ access to sensitive information on the smartphone. The risk evaluation is left to the user who has to evaluate whether or not the requested permissions are appropriate. However, former work has shown that users lack attention to and understanding of the permissions which makes it difficult for them to make appropriate decisions. To support users with better understandable information we provide statistical information about permissions, grouped by functionality. We use methods from health risk communication to communicate this information to the users. In a lab experiment with 48 participants we find that users tend to choose more often the app with a lower number of permissions when statistical information is provided together with graphics. We also find that the privacyintrusiveness and trustworthiness of apps is perceived differently when statistical information is given. 
16:30  Numerical Challenges in Simulationguided Dynamical System Analysis SPEAKER: Jim Kapinski ABSTRACT. Verification and validation (V&V) for industrial control designs can be a difficult and expensive process. Simulationguided approaches offer a practical means of performing V&V for industrial applications. One such technology uses simulation traces to discover Lyapunov functions or barrier certificates. This technique has proved promising; however, there are challenges related to the numerical computations involved. For example, the technique translates data obtained from simulation traces into a large collection of linear constraints, but not all of these constraints are necessarily useful for solving the problem. Strategies for selecting an appropriate subset of these constraints are required. In this talk, we present an overview of the simulationguided analysis approach and discuss these numerical challenges. 
16:30  QED and the TPTP World SPEAKER: Geoff Sutcliffe 
17:00  MathHub.info: Active Mathematics SPEAKER: Michael Kohlhase ABSTRACT. We present the MathHub.info system, a development environment for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with mathematical documents and knowledge. The core MathHub.info system is an archive for flexiformal mathematical documents and libraries in the OMDoc/MMT format. Content can be authored or archived in the source format of the respective system, is versioned in GIT repositories, and transformed into OMDoc/MMT for machinesupport and further into HTML5 for reading and interaction. 
17:30  Hammering towards QED SPEAKER: Cezary Kaliszyk 
16:30  Static Enforcement of RoleBased Access Control SPEAKER: Asad Ali ABSTRACT. We propose a new static approach to RBAC policy enforcement. The static approach we advocate includes a new design methodology, for applications involving RBAC, which integrates the security requirements into the system's architecture, helping to ensure that policies are correctly defined and enforced. We apply this new approach to policies restricting calls to methods in Java applications. However, our approach is more general and can be applied to other ObjectOriented languages. We present a language to express RBAC policies on calls to methods in Java, a set of design patterns which Java programs must adhere to for the policy to be enforced statically, and a highlevel algorithm for static enforcement. 
17:00  A Local Logic for Realizability in Web Service Choreographies SPEAKER: R. Ramanujam ABSTRACT. Web service choreographies specify conditions on observable interactions among the services. An important question in this regard is realizability: given a choreography C, does there exist a set of service implementations I that conform to C ? Further, if C is realizable, is there an algorithm to construct implementations in I ? We propose a local temporal logic in which choreographies can be specified, and for specifications in the logic, we solve the realizability problem by constructing service implementations (when they exist) as communicating automata. These are nondeterministic finite state automata with a coupling relation. We also report on an implementation of the realizability algorithm and discuss experimental results. 
17:00  The Ackermann Award 2014 SPEAKER: Anuj Dawar 
17:30  Formal Replay of Translation Validation for Highly Optimised C SPEAKER: Thomas Sewell ABSTRACT. In previous work~\cite{sewell2013translation} we have implemented a translation validation mechanism for checking that a C compiler is adhering to the expected semantics of a verified program. We used this apparatus to check the compilation of the seL4 verified operating system kernel~\cite{Klein_EHACDEEKNSTW_09} by GCC 4.5.1. To get this result, we carefully chose a problem representation that worked well with certain highly optimised SMT solvers. This raises a question of correctness. While we are confident the result is correct, we still aim to replay this result with the most dependable tools available. In this work we present a formalisation of the proof rules needed to replay the translation check within the theorem prover Isabelle/HOL. This is part of an ongoing effort to bring the entire translation validation result within a single trusted proof engine and derive a single correctness theorem, thus reaching the gold standard level of trustworthiness for program verification. We had hoped to present the formal rule set in action through a worked example. Unfortunately while we have all the theory we need, the mechanisms for selecting and applying the rules and discharging certain side conditions remain a work in progress, and our example proof is incomplete. 
18:15  A completeness theorem for general relativity SPEAKER: Judit X. Madarász ABSTRACT. We introduce several firstorder axiom systems for general relativity and show that they are complete with respect to the standard models of general relativity, i.e., to Lorentzian manifolds having the corresponding smoothness properties. This is only a sample of our approach (see the references in [2]) to the logical analysis of special and general relativity theory in the axiomatic framework of modern mathematical logic. The aim of our research is to build a flexible hierarchy of axiom systems (instead of one axiom system only), analyzing the logical connections between the different axioms and axiomatizations. We try to formulate simple, logically transparent and intuitively convincing axioms. The questions we study include: What is believed and why?  Which axioms are responsible for certain predictions?  What happens if we discard some axioms?  Can we change the axioms, and at what price? [1] H. Andréka, J.X. Madarász, I. Németi, and G. Székely, An axiom system for general relativity complete with respect to Lorentzian manifolds, arXiv:1310.1475, 2013. [2] H. Andréka, J.X. Madarász, I. Németi, and G. Székely, A logic road from special relativity to general relativity, Synthese, vol. 186 (2012), no. 3, pp. 633–649, arXiv:1005.0960. 
18:35  More On Completion with Horn Filters SPEAKER: Cyrus F Nourani 
18:15  Predicative Mathematics via Safety Relations SPEAKER: Liron Cohen ABSTRACT. In [1] a new framework for predicative mathematics was developed. The main new features of this framework are that it is typefree, based on a subsystem of ZF, and the language it employs includes nothing that is not used in ordinary mathematical texts. In particular: it reflects real mathematical practice in making an extensive use of statically defined abstract set terms of the form {xφ}. In this work we show how large portions of classical analysis can be developed within that framework in a natural, predicatively acceptable way. Among other things, this includes the introduction of the natural numbers, the real line and continuous real functions, as well as formulating and proving the main classical results concerning these notions. [1] Arnon Avron, A New Approach to Predicative Set Theory, Ways of Proof Theory (R. Schindler, editor), Onto Series in Mathematical Logic, onto verlag, 2010, pp. 31  63. 
18:35  Natural Deduction in Renaissance Geometry SPEAKER: Ryszard Mirek ABSTRACT. Moritz Cantor was so impressed by the achievements of Piero della Francesca in mathematics and geometry that devoted him in his Vorlesungen uber Geschichte der Mathematik far more attention than to any other contem porary algebraicist. In Francesca's treatise De prospectiva pingendi we find the advanced geometrical exercises presented in the form of propositions. For instance, in Book 1, Proposition 8, he shows that the perspective images of orthogonals converge to a point. Proposition 12 shows how to draw in per spective a surface of undefined shape, which is located in profile as a straight line. The task is to find the image of a line perpendicular to the picture plane. But the most interesting is Proposition 13 that shows how to degrade a square and, more precisely the sides of the square. It is obvious that most of these propositions are used in the paintings of Francesca. The purpose of the study is to describe these results in the form of logi cal system EF. Generally, the logical language is six sorted, with sorts for points, lines, circles, segments, angles, and areas. As proofs it is possible to employ the method of natural deduction. The aim is to demonstrate that such a method is the most useful for the presentation of the geometric proofs of Francesca, taking into account also the importance of diagrams within them. 
18:55  Aristotle’s conception of demonstration and modern proof theory SPEAKER: Olga Antonova ABSTRACT. The history of modern mathematical proof theory begins with Beweistheorie or Hilbert’s proof theory. The mathematical theories such as logicism (Frege, Russell), intuitionism (Brouwer, Heyting), set theory (Cantor, Dedekind) influenced directly the conception of proof and generally modern proof theory. The modern proof theory is based not only on mathematical theories, but also on the philosophical and logical proof theories, such as Aristotle’s conception of demonstration. According to Aristotle a demonstration is a “scientific syllogism”, in which the premises are true, first, immediate, more known than the conclusion, prior to the conclusion and causes of the conclusion. Aristotle’s theory of demonstration impacted on the development of logic and, in particular, on the philosophical and logical conception of proof. Can we say that Aristotle’s conception of demonstration is modern? Is the actual conception of proof really based on Aristotle’s conception? The purpose of my talk is to analyze Aristotle’s definition of demonstration and compare it with the modern approach to demonstration. [1]Barnes, J. Aristotle. Posterior Analytics. Oxford University Press, 1976. [2]Hendricks, V. et al., eds, Proof Theory: History and Philosophical Significance, Kluwer. 2000. 
18:15  Modelling Inference in Fiction SPEAKER: unknown ABSTRACT. As it is widelyknown, fiction became a serious problem for several classical conceptions closed related to philosophy of logic (J. Woods, 2006). This was mainly due to some of the leading features of reasoning in fiction. Firstly, inference in fiction involves reasoning with incomplete information. Stories describe their characters, places, and events only in an incomplete way. Due to the fact that stories are composed by a finite set of sentences, a large amount of information about them remains unknown. Secondly, inference in fiction also involves reasoning with inconsistent information. Inconsistencies can emerge from two sources. On the one hand, information belonging to a fiction contradicts reality in many aspects. On the other hand, some stories are based on a contradiction or contain inconsistent information. This is the case of stories in which contradictions are an essential part of their plots. In order to cope with the abovementioned features of reasoning in fiction, we propose a semantic approach of fiction based on an intuitionistic modal system. The semantic model is an adaptation of the multipleexpert semantics developed by Melvin Fitting in 1992. Firstly, we consider a propositional language to represent fictional information formally. That propositional language is interpreted in an intuitionistic modal semantics that involves two different perspectives and a partial valuation. On the one hand, these two perspectives make it possible to distinguish two sources of information involved in reasoning in fiction, i.e., fiction and reality. On the other hand, the partial valuation makes it possible to deal with incomplete information. A relation of logical consequence is defined in order to distinguish between valid and invalid inferences within the fictional context. Finally, we explore different prooftheoretical alternatives in order to characterize a deductive system for this semantic approach. 
18:35  Metalogical ExtensionsPart II: Firstorder Consequences and Gödel SPEAKER: Joachim MuellerTheys ABSTRACT. Metalogical extensions incorporate metalogics by means of new logical symbols. Among many other things, they thereby yield a soundness criterion for immanent attempts, which try to reflect provability or truth by means of unary formulae in stock. However, this benchmark cannot be met within sufficiently strong consistent theories—a further consequence of the Diagonal Lemma. Thus it is particularly questionable whether Prov(x) really expresses provability and Con (derived therefrom) really states consistency: the 2nd Incompleteness Theorem may be doubted. 