ABSTRACT. In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or KL_1), over single-agent systems having imperfect information of the system state. [Vardi and Van der Meyden, CCONCUR'98] have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization.

We propose a "Safraless" synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into the problem of checking emptiness for universal co-B\"{u}chi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.

ABSTRACT. A standard approach to optimizing long-run running costs of discrete systems is based on minimizing the mean-payoff, i.e., the long-run average amount of resources (``energy'') per transition. However, this approach inherently assumes that the energy source has an unbounded capacity, which is not always realistic. For example, an autonomous robotic device has a battery of finite capacity that has to be recharged periodically, and the total amount of energy consumed between two successive charging cycles is bounded by the capacity. Hence, a controller minimizing the mean-payoff must obey this restriction. In this paper we study the controller synthesis problem for consumption systems with a finite battery capacity, where the task of the controller is to minimize the mean-payoff while preserving the functionality of the system encoded by a given linear-time property. We show that an optimal controller always exists, and it may either need only finite memory or require infinite memory (it is decidable in polynomial time which of the two cases holds). Further, we show how to compute an effective description of an optimal controller in polynomial time. Finally, we consider the limit values achievable by larger and larger battery capacity, show that these values are computable in polynomial time, and we also analyze the corresponding rate of convergence. To the best of our knowledge, these are the first results about optimizing the long-run running costs in systems with bounded energy stores.

ABSTRACT. We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.

ABSTRACT. This paper presents a new synthesis-based approach for helping programmers write low-level memory-safe code. Specifically, given a partial program with missing guards, our algorithm synthesizes concrete predicates to plug in for the missing guards such that all buffer accesses in the program are guaranteed to be memory safe. Furthermore, our algorithm gives a guarantee of optimality in that the synthesized guards are provably the simplest (that is, with the fewest number of variables) and weakest among guards that guarantee memory safety. Our approach is fully automatic and does not require any hints, such as templates, from the user. We have implemented our proposed algorithm in a prototype synthesis tool for C programs. Our experimental evaluation on a set of real-world C programs shows that the proposed approach is able to successfully synthesize guards that closely match hand-written programmer code.

ABSTRACT. Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences' semantics may be subtle, the automation of their placement is highly desirable. But precise methods restoring consistency do not scale to deployed systems code. We choose to trade some precision for genuine scalability: we present a novel technique suitable for large code bases. We implement this method in our new musketeer tool, and detail experiments on more than 350 executables of packages found in a Debian Linux distribution, e.g. memcached (about 10000 LoC).

ABSTRACT. We introduce MCMAS-SLK, a BDD-based model checker for the verification of systems against specifications expressed in a novel, epistemic variant of strategy logic. We give syntax and semantics of the specification language and a introduce a labelling algorithm for epistemic and strategy logic modalities. We provide details of the checker which can also be used for synthesising the agents' strategies so that a specification is satisfied by the system. We evaluate the efficiency of the implementation by discussing the results obtained for the dining cryptographers protocol and the cake-cutting problem.

ABSTRACT. Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. We propose a new method for solving reachability games. Our method works by exploring a subset of the possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided backtracking search to identify a subset of runs that are sufficient to consider to solve the game. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems.

ABSTRACT. G4LTL-ST automatically generates IEC 61131-3-compatible control code for industrial field-level devices from behavioral, timed specifications of input-output signals. Behavioral specifications are expressed in a linear temporal logic (LTL) extended language with (1) arithmetic constraints for describing data-intensive control behavior and (2) timers which are based on the industry standard IEC 61131-3. The code generated by G4LTL-ST is in the format of Structured Text which can readily be compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements a pseudo-Boolean abstraction of data constraints and a compilation of timer specifications into LTL, together with a CEGAR-like abstraction-refinement loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST includes a number of heuristics for suggesting additional environment assumptions for making the control problem at hand realizable.

ABSTRACT. We present results of the first competition for reactive synthesis tools. The performance of synthesis tools is compared on safety specifications in an extension of the AIGER format, and tools are ranked with respect to the time needed for realizability checks and the size of circuits produced by synthesis.

ABSTRACT. Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often require stronger guarantees. For instance, a histogram class that is implemented using a concurrent map may require a method to atomically increment a histogram bar, but its implementation requires multiple calls to the map and hence is not atomic by default. Indeed, prior work has shown that atomicity errors in clients of concurrent data structures occur frequently in production code. We present an automatic and modular verification technique for clients of concurrent data structures. We define a novel sufficient condition for atomicity of clients called condensability. We present a tool called Snowflake that generates proof obligations for condensability of Java client methods and discharges them using an off-the-shelf SMT solver. We applied Snowflake to an existing suite of client methods from several open-source applications. It successfully verified 76.9% of the atomic methods without any change and verified the rest of them with small code refactoring. It rejected all non-atomic methods.

ABSTRACT. While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present a new repair algorithm that avoids such regressions. The solution space is given by the program transformations we consider in the repair process. These include reordering of instructions within a thread, inserting atomic sections, and inserting wait-notify mechanisms. The new algorithm, PACES, is an extension of the CEGIS loop. It learns constraints on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From counterexamples, the algorithm learns a constraint necessary to remove them. From positive examples, it learns constraints that are necessary in order to prevent the repair from turning the trace into a counterexample. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs. The tool is able to fix the bugs while avoiding regressions.

ABSTRACT. Bounded model checking (BMC) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to BMC of sequentially consistent C programs using POSIX threads. Our approach first translates a multi-threaded C program into a non-deterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as back-ends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of non-determininsm, so that it produces tight SAT/SMT formulae, and is thus very effective in practice: our implementation won the the concurrency category of SV-COMP14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.

ABSTRACT. Model checkers based on Petri net coverability have been used successfully in recent years to verify safety properties of concurrent shared-memory or asynchronous message-passing software. We revisit a constraint approach to coverability based on classical Petri net analysis techniques. We show how to utilize an SMT solver to implement the constraint approach, and additionally, to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a large set of existing Petri net benchmarks. Even though our technique is incomplete, it can quickly discharge most of the safe instances. Additionally, the inductive invariants computed are usually orders of magnitude smaller than those produced by existing solvers.

ABSTRACT. This paper presents Leap, a tool for the verification of concurrent datatypes and parametrized systems composed by an unbounded number of threads that manipulate infinite data.

Concurrent datatypes are accessed by numerous threads which manipulate shared data in the heap using liberal patterns of synchronization like lock-freedom and fine-grain locking. Formally verifying concurrent datatypes is a challenging task, because of the combination of complex dynamic memory manipulation, and the rather unstructured concurrent execution. The difficulty is increased because one must also deal with concurrent system composed by the execution of an unbounded number of threads.

Leap receives as input a concurrent program description and a specification. Leap generates automatically a finite collection of verification conditions and discharges these to specialized decision procedures built on top of state-of-the-art SMT solvers. The validity of all verification conditions implies that the program executed by any number of threads satisfies the specification. Leap does not only include decision procedures for integers and booleans, but also implements specific theories for heap memory layouts such as linked-lists and skiplist.

ABSTRACT. We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic (FPA). Model construction has various applications, for instance the automatic generation of test inputs. It is well-known that naive encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed for model construction. We define a framework for systematic application of approximations in order to speed up model construction. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations (or the combination of both) can be used, and shows promising results in practice.

ABSTRACT. Interval Temporal Logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for automated ITL reasoning is available, possibly also owed to ITL's undecidability.

We consider the bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that makes use of the power of modern incremental SAT solvers and present a tool which tests an ITL specification for finite satisfiability.

ABSTRACT. We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theorem provers, SAT and SMT solvers, constraint solvers, model checkers, and software verifiers. The service, running on a compute cluster with 380 processors and 23 terabytes of disk space, is designed to provide a single piece of storage and computing in- frastructure to logic solving communities and their members. It aims at reducing duplication of effort and resources as well as enabling individual researchers or groups with no access to comparable infrastructure. StarExec allows community organizers to store, manage and make available benchmark libraries; competition organizers to run logic solver competitions; and community members to do com- parative evaluations of logic solvers on public or private benchmark problems.

ABSTRACT. This paper introduces Skeptik: a system for checking, compressing and improving proofs obtained by sat- and smt-solvers.

ABSTRACT. Our understanding of the notion "dynamic system" is a rather broad one: such a system has states, which can change over time. Ontologies are used to describe the states of the system, possibly in an incomplete way. Monitoring is then concerned with deciding whether some run of the system or all of its runs satisfy a certain property, which can be expressed by a formula of an appropriate temporal logic. We consider different instances of this broad framework, which can roughly be classified into two cases. In one instance, the system is assumed to be a black box, whose inner working is not known, but whose states can be (partially) observed during a run of the system. In the second instance, one has (partial) knowledge about the inner working of the system, which provides information on which runs of the system are possible.

In this talk, we will review some of our recent research that investigates different instances of this general framework of ontology-based monitoring of dynamic systems. We will also sketch possible extensions towards probabilistic reasoning and the integration of mathematical modelling of dynamical systems.

ABSTRACT. The Vienna Circle of Logical Empiricism, which was part of the intellectual movement of Central European philosophy of science, is certainly one of the most important currents in the emergence of modern philosophy of science. Apart from this uncontested historical fact there remains the question of the direct and indirect influence, reception and topicality of this scientific community in contemporary philosophy of science in general as well as in the philosophy of the individual sciences, including the formal and social sciences. 

First, I will characterize the road from the Schlick-Circle to contemporary philosophy of science. Second, I will refer to "the present situation in the philosophy of science" by identifying relevant impacts, findings, and unfinished projects since the classical Vienna Circle. Third, I will address some specific European features of this globalized philosophical tradition up to the present, and outline future perspectives after the linguistic, historical and pragmatic turns – looking back to the "received view", or standard view of the Vienna Circle.

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• Fifth Answer Set Programming Competition (ASPCOMP 2014);
• The 7th IJCAR ATP System Competition (CASC-J7);
• Hardware Model Checking Competition (HWMCC 2014);
• OWL Reasoner Evaluation (ORE 2014);
• Satisfiability Modulo Theories solver competition (SMT-COMP 2014);
• Competition on Software Verification (SV-COMP 2014);
• Syntax-Guided Synthesis Competition (SyGuS-COMP 2014);
• Synthesis Competition (SYNTCOMP 2014); and
• Termination Competition (termCOMP 2014).

ABSTRACT. Werner "Jimmy" DePauli-Schimanovich is being honored for his contributions to Gödel research, for his efforts towards re-establishing Vienna as a center of logic in the second half of the past century, and for extending the outreach of formal logic and logical thinking to other disciplines. The books about Gödel he authored, co-authored, or edited contain precious contributions of historical, philosophical, and mathematical value. His film on Gödel, and related articles and TV testimonials, attracted the general public to Gödel and his work. Moreover, DePauli-Schimanovich has unceasingly and successfully fought to re-establish logic in Vienna. He has inspired and encouraged a large number of students and young researchers, has organised meetings and social gatherings, and has created an intellectual home for scholars of logic. His activities significantly contributed to filling the intellectual vacuum in logic research that had developed in Austria in the years 1938–1945 and well into the post-war period. He was a main initiator and co-founder of the International Kurt Gödel Society. Jimmy’s research in logic involved criticism of current axiomatisations of set theory and development of new systems of naïve set theory. In informatics, DePauli-Schimanovich was co-founder and co-organiser of EuroCAST, a conference series on computer-assisted systems theory meeting alternatively in Vienna and Las Palmas, Gran Canaria. Finally, Jimmy has furthered implementation of logical ideas in disparate fields such as mechanical engineering, automated game playing, urban planning, and by inventing a number of logical games.

ABSTRACT. Zhang Mingyi is a pioneer in Artificial Intelligence and Knowledge Representation in China. He has built up a school of non-monotonic logic in Guiyang and has fostered the exchange between Chinese and Western scientists. He has contributed a large number of results on various forms of non-monotonic reasoning, including default logic, answer set programming, and belief revision. In particular, as early as 1992, he has provided important characterizations of various forms of default logic that paved the way for clarifying their computational properties and for developing algorithms for default reasoning.  Jointly with collaborators, he proposed a characterization of answer sets based on sets of generating rules, and introduced the concept of first-order loop formulas to relate answer set programming to classical logic. Other important results relate to theory revision (for example, the proof of the existence and uniqueness of finest splitting of Horn formulae) and to normal forms for Gödel logics. Many of Zhang Mingyi's former students have become internationally respected researchers.

ABSTRACT. The Free University of Bozen-Bolzano, the Technische Universität Dresden, the Universidade Nova de Lisboa, the Universidad Politécnica de Madrid (until 2010), the Technische Universität Wien, and Australia's Information Communications Technology Research Centre of Excellence (since 2007) are jointly running the European Master's Program in Computational Logic (EMCL) since 2004. The program is supported by the European Union within Erasmus Mundus and Eramsus+. So far, more than 100 students from 39 different countries have successfully completed the distributed master's program with a double or joint degree.

For the first time, the partner institutions are announcing the EMCL Distinguished Alumni Award for outstanding contributions of EMCL graduates to the field of Computational Logic.

http://www.emcl-study.eu/