Strategy Logic (SL, for short) has been recently introduced by Mogavero,
Murano, and Vardi as a useful formalism for reasoning explicitly about
strategies, as first-order objects, in multi-agent concurrent games. This logic
turns to be very powerful, subsuming all major previously studied modal logics
for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due
to its expressiveness, SL has a non-elementarily decidable model-checking
problem and a highly undecidable satisfiability problem, specifically,
$\Sigma_{1}^{1}$-Hard.

The modal logic S4 can be used via a Curry-Howard style correspondence to
obtain a lambda-calculus. Modal (boxed) types are intuitively interpreted as
`closed syntax of the calculus'. This lambda-calculus is called modal type
theory --- this is the basic case of a more general contextual modal type
theory, or CMTT.

CMTT has never been given a denotational semantics in which modal types are
given denotation as closed syntax. We show how this can indeed be done, with a
twist. We also use the denotation to prove some properties of the system.

We consider the problem of existential quantifier elimination for Boolean
formulas in Conjunctive Normal Form (CNF). We present a new method for solving
this problem called Derivation of Dependency-Sequents (DDS). A
Dependency-sequent (D-sequent) is used to record that a set of quantified
variables is redundant under a partial assignment. We show that D-sequents can
be resolved to obtain new, non-trivial D-sequents. We also show that DDS is
compositional, i.e. if our input formula is a conjunction of independent
formulas, DDS automatically recognizes and exploits this information.

To make the development of efficient multi-core applications easier,
libraries, such as Grand Central Dispatch, have been proposed. When using such
a library, the programmer writes so-called blocks, which are chunks of codes,
and dispatches them, using synchronous or asynchronous calls, to several types
of waiting queues. A scheduler is then responsible for dispatching those blocks
on the available cores. Blocks can synchronize via a global memory.

One central issue in the formal design and analysis of reactive systems is
the notion of refinement that asks whether all behaviors of the implementation
is allowed by the specification. The local interpretation of behavior leads to
the notion of simulation. Alternating transition systems (ATSs) provide a
general model for composite reactive systems, and the simulation relation for
ATSs is known as alternating simulation. The simulation relation for fair
transition systems is called fair simulation.

Girard's LLL characterized Ptime in the proof-as-program paradigm with a
complexity bound on cut elimination. This logic relied on a stratification
principle which Baillot and Mazza generalized by defining two variants L^4 and
L^4_0 referred to as light linear logic by levels. However, for L^4, a
polynomial bound was given on cut elimination only for a specific reduction
strategy. L^4_0 only enjoyed a complexity soundness result without an explicit
bound on cut elimination. These limitations are a problem for defining a proper
type system out of theses logics.

Seely's paper "Locally cartesian closed categories and type theory" contains
a well-known result in categorical type theory: that the category of locally
cartesian closed categories is equivalent to the category of Martin-L\"of type
theories with Pi-types, Sigma-types and extensional identity types. However,
Seely's proof relies on the problematic assumption that substitution in types
can be interpreted by pullbacks.

Connections between the sequentiality/concurrency distinction and the
semantics of proofs are investigated, with particular reference to games and
Linear Logic.

We give multiple descriptions of a topological universe of finitary sets,
which can be seen as a natural limit completion of the hereditarily finite
sets. This universe is characterized as a metric completion of the hereditarily
finite sets; as a Stone space arising as the solution of a functorial
fixed-point equation involving the Vietoris construction; as the Stone dual of
the free modal algebra; and as the subspace of maximal elements of a domain
equation involving the Plotkin (or convex) powerdomain.

We present a set-theoretic, proof-irrelevant model for Calculus of
Constructions (CC) with predicative induction and judgmental equality in
Zermelo-Fraenkel set theory with an axiom for countably many inaccessible
cardinals. We use Aczel's trace encoding which is universally defined for any
function type, regardless of being impredicative. Direct and concrete
interpretations of simultaneous induction and mutually recursive functions are
also provided by extending Dybjer's interpretations on the basis of Aczel's
rule sets.

We introduce a new domain for finding precise numerical invariants of
programs by abstract interpretation. This domain, which consists of level sets
of non-linear functions, generalizes the domain of linear "templates"
introduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic
templates, we use Shor's semi-definite relaxation to derive computable yet
precise abstractions of semantic functionals, and we show that the abstract
fixpoint equation can be solved accurately by coupling policy iteration and
semi-definite programming.

Complementation and determinization are two fundamental notions in automata
theory. The close relationship between the two has been well observed in the
literature. In the case of nondeterministic finite automata on finite words
(NFA), complementation and determinization have the same state complexity,
namely $\Theta(2^{n})$ where $n$ is the state size. The same similarity between
determinization and complementation was found for B\"{u}chi automata, where
both operations were shown to have $2^{\Theta(n \lg n)}$ state complexity.

Interactive theorem proving requires a lot of human guidance. Proving a
property involves (1) figuring out why it holds, then (2) coaxing the theorem
prover into believing it. Both steps can take a long time. We explain how to
use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based
reasoning. This approach makes it unnecessary to deeply understand why a
property is true, and automates the process of admitting it as a theorem. We
use GL at Centaur Technology to verify execution units for x86 integer, MMX,
SSE, and floating-point arithmetic.

Virtualization promises significant benefits in security, efficiency,
dependability, and cost. Achieving these benefits depends upon the reliability
of the underlying virtual machine monitors (hypervisors). This paper describes
an ongoing project to develop and verify MinVisor, a simple but functional
Type-I x86 hypervisor, proving protection properties at the assembly level
using ACL2. Originally based on an existing research hypervisor, MinVisor
provides protection of its own memory from a malicious guest.

This volume consists of the proceedings of the 5th Workshop on Formal
Languages and Analysis of Contract-Oriented Software (FLACOS'11). The FLACOS
Workshops serve as annual meeting places to bring together researchers and
practitioners working on language-based solutions to contract-oriented software
development. High-level models of contracts are needed as a tool to negotiate
contracts and provide services conforming to them.

Dialectical logic is the logic of dialectical processes. The goal of
dialectical logic is to introduce dynamic notions into logical computational
systems. The fundamental notions of proposition and truth-value in standard
logic are subsumed by the notions of process and flow in dialectical logic.
Dialectical logic has a standard aspect, which can be defined in terms of the
"local cartesian closure" of subtypes.

Arbuscular mycorrhiza (AM) is the most wide-spread plant-fungus symbiosis on
earth. Investigating this kind of symbiosis is considered one of the most
promising ways to develop methods to nurture plants in more natural manners,
avoiding the complex chemical productions used nowadays to produce artificial
fertilizers. In previous work we used the Calculus of Wrapped Compartments
(CWC) to investigate different phases of the AM symbiosis. In this paper, we
continue this line of research by modelling the colonisation of the plant root
cells by the fungal hyphae spreading in the soil.

This volume contains the papers presented at the second international
workshop on Logics for Component Configuration (LoCoCo 2011) which was
associated with the International Conference on Principles and Practice of
Constraint Programming (CP 2011) and which took place on September 12, 2011 in
Perugia, Italy. Representing and solving configuration problems is a hot topic
of great importance for many application domains. For example, modern software
distributions are based on the notion of components, which denote units of
independent development and deployment.

Rewriting is a common approach to logic optimization based on local
transformations. Most commercially available logic synthesis tools include a
rewriting engine that may be used multiple times on the same netlist during
optimization. This paper presents an And-Inverter graph based rewriting
algorithm using 5-input cuts. The best circuits are pre-computed for a subset
of NPN classes of 5-variable functions. Cut enumeration and Boolean matching
are used to identify replacement candidates.

Many programming languages and tools, ranging from grep to the Java String
library, contain regular expression matchers. Rather than first translating a
regular expression into a deterministic finite automaton, such implementations
typically match the regular expression on the fly. Thus they can be seen as
virtual machines interpreting the regular expression much as if it were a
program with some non-deterministic constructs such as the Kleene star. We
formalize this implementation technique for regular expression matching using
operational semantics.

In this paper, we introduce an extension of the GSOS rule format with
predicates such as termination, convergence and divergence. For this format we
generalize the technique proposed by Aceto, Bloom and Vaandrager for the
automatic generation of ground-complete axiomatizations of bisimilarity over
GSOS systems. Our procedure is implemented in a tool that receives SOS
specifications as input and derives the corresponding axiomatizations
automatically. This paves the way to checking strong bisimilarity over process
terms by means of theorem-proving techniques.

The process algebra HYPE was recently proposed as a fine-grained modelling
approach for capturing the behaviour of hybrid systems. In the original
proposal, each flow or influence affecting a variable is modelled separately
and the overall behaviour of the system then emerges as the composition of
these flows. The discrete behaviour of the system is captured by instantaneous
actions which might be urgent, taking effect as soon as some activation
condition is satisfied, or non-urgent meaning that they can tolerate some
(unknown) delay before happening.

This paper deals with model transformation based on attributed graph
rewriting. Our contribution investigates a single pushout approach for applying
the rewrite rules. The computation of graph attributes is obtained through the
use of typed lambda-calculus with inductive types. In this paper we present
solutions to cope with single pushout construction for the graph structure and
the computations functions. As this rewrite system uses inductive types, the
expressiveness of attribute computations is facilitated and appears more
efficient than the one based on Sigma-algebras.

This article de?nes a complement of a function and conditions for existence
of such a complement function and presents few algorithms to construct a
complement.

Event-B provides a flexible framework for stepwise system development via
refinement. The framework supports steps for (a) refining events (one-by-one),
(b) splitting events (one-by-many), and (c) introducing new events. In each of
the steps events can moreover possibly be anticipated or convergent. All such
steps are accompanied with precise proof obligations. Still, it remains unclear
what the exact relationship - in terms of a behaviour-oriented semantics -
between an Event-B machine and its refinement is.

Simulink/Stateflow charts are widely used in industry for the specification
of control systems, which are often safety-critical. This suggests a need for a
formal treatment of such models. In previous work, we have proposed a technique
for automatic generation of formal models of Stateflow blocks to support
refinement-based reasoning. In this article, we present a refinement strategy
that supports the verification of automatically generated sequential C
implementations of Stateflow charts.

Refinement is a powerful mechanism for mastering the complexities that arise
when formally modelling systems. Refinement also brings with it additional
proof obligations -- requiring a developer to discover properties relating to
their design decisions. With the goal of reducing this burden, we have
investigated how a general purpose theory formation tool, HR, can be used to
automate the discovery of such properties within the context of Event-B.

Floating point operations are fast, but require continuous effort on the part
of the user in order to ensure that the results are correct. This burden can be
shifted away from the user by providing a library of exact analysis in which
the computer handles the error estimates. Previously, we provided
[arXiv:1105.2751v1] a fast implementation of the exact real numbers in the Coq
proof assistant.

Embedded systems are everywhere, from home appliances to critical systems
such as medical devices. They usually have associated timing constraints that
need to be verified for the implementation. Here, we use an untimed bounded
model checker to verify timing properties of embedded C programs. We propose an
approach to specify discrete time timing constraints using code annotations.
The annotated code is then automatically translated to code that manipulates
auxiliary timer variables and is thus suitable as input to conventional,
untimed software model checker such as ESBMC.

Computability logic is a formal theory of computability. The earlier article
"Introduction to cirquent calculus and abstract resource semantics" by
Japaridze proved soundness and completeness for the basic fragment CL5 of
computability logic. The present article extends that result to the more
expressive cirquent calculus system CL6, which is a conservative extension of
both CL5 and classical propositional logic.

Parsing is an important problem in computer science and yet surprisingly
little attention has been devoted to its formal verification. In this paper, we
present TRX: a parser interpreter formally developed in the proof assistant
Coq, capable of producing formally correct parsers. We are using parsing
expression grammars (PEGs), a formalism essentially representing recursive
descent parsing, which we consider an attractive alternative to context-free
grammars (CFGs).

In this paper we present FASE (Fast Asynchronous Systems Evaluation), a tool
for evaluating worst-case efficiency of asynchronous systems. This tool
implements some well-established results in the setting of a timed CCS-like
process algebra: PAFAS (a Process Algebra for Faster Asynchronous Systems).
Moreover, we discuss some new solutions that are useful to improve the
applicability of FASE to concrete meaningful examples.

Working in the Blum-Shub-Smale model of computation on the real numbers, we
answer several questions of Meer and Ziegler. First, we show that, for each
natural number d, an oracle for the set of algebraic real numbers of degree at
most d is insufficient to allow an oracle BSS-machine to decide membership in
the set of algebraic numbers of degree d + 1. We add a number of further
results on relative computability of these sets and their unions.

Heterogeneous nonmonotonic multi-context systems (MCS) permit different
logics to be used in different contexts, and link them via bridge rules. We
investigate the role of symmetry detection and symmetry breaking in such
systems to eliminate symmetric parts of the search space and, thereby, simplify
the evaluation process. We propose a distributed algorithm that takes a local
stance, i.e., computes independently the partial symmetries of a context and,
in order to construct potential symmetries of the whole, combines them with
those partial symmetries returned by neighbouring contexts.

We present an abstract framework for concurrent processes in which atomic
steps have generic side effects, handled according to the principle of monadic
encapsulation of effects. Processes in this framework are potentially infinite
resumptions, modelled using final coalgebras over the monadic base. As a
calculus for such processes, we introduce a concurrent extension of Moggi's
monadic metalanguage of effects. We establish soundness and completeness of a
natural equational axiomatisation of this calculus.

A well-known problem in Petri net theory is to formalise an appropriate
causality-based concept of process or run for place/transition systems. The
so-called individual token interpretation, where tokens are distinguished
according to their causal history, giving rise to the processes of Goltz and
Reisig, is often considered too detailed. The problem of defining a fully
satisfying more abstract concept of process for general place/transition
systems has so-far not been solved.

The probability theory is a well-studied branch of mathematics, in order to
carry out formal reasoning about probability. Thus, it is important to have a
logic, both for computation of probabilities and for reasoning about
probabilities, with a well-defined syntax and semantics. Both current
approaches, based on Nilsson's probability structures/logics, and on linear
inequalities in order to reason about probabilities, have some weak points. In
this paper we have presented the complete revision of both approaches.

The aim of illocutionary logic is to explain how context can affect the
meaning of certain special kinds of performative utterances. Recall that
performative utterances are understood as follows: a speaker performs the
illocutionary act (e.g. act of assertion, of conjecture, of promise) with the
illocutionary force (resp. assertion, conjecture, promise) named by an
appropriate performative verb in the way of representing himself as performing
that act. In the paper I proposed many-valued interpretation of illocutionary
forces understood as modal operators.

First-order applicative term rewriting systems provide a natural framework
for modeling higher-order aspects. In earlier work we introduced an uncurrying
transformation which is termination preserving and reflecting. In this paper we
investigate how this transformation behaves for innermost termination and
(innermost) derivational complexity. We prove that it reflects innermost
termination and innermost derivational complexity and that it preserves and
reflects polynomial derivational complexity.

The evaluation mechanism of pattern matching with dynamic patterns is
modelled in the Pure Pattern Calculus by one single meta-rule. This
contribution presents a refinement which narrows the gap between the abstract
calculus and its implementation. A calculus is designed to allow reasoning on
matching algorithms. The new calculus is proved to be confluent, and to
simulate the original Pure Pattern Calculus. A family of new, matching-driven,
reduction strategies is proposed.

Finite automata on infinite words ($\omega$-automata) proved to be a powerful
weapon for modeling and reasoning infinite behaviors of reactive systems.
Complementation of $\omega$-automata is crucial in many of these applications.
But the problem is non-trivial; even after extensive study during the past 50
years, a handful of interesting problems remain unanswered, one of which is the
complexity of Streett complementation (complementation of Streett automata).
The best construction for complementing a Streett automaton with $n$ states and
$k$ Streett pairs, is $2^{O(nk\lg nk)}$, which is s

We present an iterative algorithm for enforcing policies represented in a
first-order logic, which can, in particular, express all transmission-related
clauses in the HIPAA Privacy Rule. The logic has three features that raise
challenges for enforcement --- uninterpreted predicates (used to model
subjective concepts in privacy policies), real-time temporal properties, and
quantification over infinite domains (such as the set of messages containing
personal information). The algorithm operates over audit logs that are
inherently incomplete and evolve over time.

Let $M=(A,<,\overline{P})$ where $(A,<)$ is a linear ordering and
$\overline{P}$ denotes a finite sequence of monadic predicates on $A$. We show
that if $A$ contains an interval of order type $\omega$ or $-\omega$, and the
monadic second-order theory of $M$ is decidable, then there exists a
non-trivial expansion $M'$ of $M$ by a monadic predicate such that the monadic
second-order theory of $M'$ is still decidable.

Superdeduction is a method specially designed to ease the use of first-order
theories in predicate logic. The theory is used to enrich the deduction system
with new deduction rules in a systematic, correct and complete way.

Bi-intuitionistic logic is the conservative extension of intuitionistic logic
with a connective dual to implication. It is sometimes presented as a symmetric
constructive subsystem of classical logic.

We prove that interactive learning based classical realizability (introduced
by Aschieri and Berardi for first order arithmetic) is sound with respect to
Coquand game semantics. In particular, any realizer of an
implication-and-negation-free arithmetical formula embodies a winning recursive
strategy for the 1-Backtracking version of Tarski games. We also give examples
of realizer and winning strategy extraction for some classical proofs.

FIT stands for Foundations of Interface Technologies. Component-based design
is widely considered as a major approach to developing systems in a time and
cost effective way. Central in this approach is the notion of an interface.
Interfaces summarize the externally visible properties of a component and are
seen as a key to achieving component interoperability and to predict global
system behavior based on the component behavior. To capture the intricacy of
complex software products, rich interfaces have been proposed.

In semantics and in programming practice, algebraic concepts such as monads
or, essentially equivalently, (large) Lawvere theories are a well-established
tool for modelling generic side-effects. An important issue in this context are
combination mechanisms for such algebraic effects, which allow for the modular
design of programming languages and verification logics.

Recently data trees and data words have received considerable amount of
attention in connection with XML reasoning and system verification. These are
trees or words that, in addition to labels from a finite alphabet, carry data
values from an infinite alphabet (data). In general it is rather hard to obtain
logics for data words and trees that are sufficiently expressive, but still
have reasonable complexity for the satisfiability problem. In this paper we
extend and study the notion of B\"uchi automata for omega-words with data.

Process behaviour is often defined either in terms of the tests they satisfy,
or in terms of the logical properties they enjoy. Here we compare these two
approaches, using extensional testing in the style of DeNicola, Hennessy, and a
recursive version of the property logic HML. We first characterise subsets of
this property logic which can be captured by tests. Then we show that those
subsets of the property logic capture precisely the power of tests.

Sound behavioral equations on open terms may become unsound after
conservative extensions of the underlying operational semantics. Providing
criteria under which such equations are preserved is extremely useful; in
particular, it can avoid the need to repeat proofs when extending the specified
language.

We introduce the process calculus Multi-CCS, which extends conservatively CCS
with an operator of strong prefixing able to model atomic sequences of actions
as well as multiparty synchronization. Multi-CCS is equipped with a labeled
transition system semantics, which makes use of a minimal structural
congruence. Multi-CCS is also equipped with an unsafe P/T Petri net semantics
by means of a novel technique. This is the first rich process calculus,
including CCS as a subcalculus, which receives a semantics in terms of unsafe,
labeled P/T nets.

The languages accepted by finite automata are precisely the languages denoted
by regular expressions. In contrast, finite automata may exhibit behaviours
that cannot be described by regular expressions up to bisimilarity. In this
paper, we consider extensions of the theory of regular expressions with various
forms of parallel composition and study the effect on expressiveness. First we
prove that adding pure interleaving to the theory of regular expressions
strictly increases its expressiveness up to bisimilarity.

Open Answer Set Programming (OASP) is an attractive framework for integrating
ontologies and rules. In general OASP is undecidable. In previous work we
provided a tableau-based algorithm for satisfiability checking w.r.t. forest
logic programs, a decidable fragment of OASP, which has the forest model
property. In this paper we introduce an optimized version of that algorithm
achieved by means of a knowledge compilation technique.

Model theoretic results such as Characterization and Definability give
important information about different logics. It is well known that the proofs
of those results for several modal logics have, somehow, the same 'taste'. A
general proof for most modal logics below first order is still too ambitious.
In this thesis we plan to isolate sufficient conditions for the
characterization and definability theorems to hold in a wide range of logics.
Along with these conditions we will prove that, whichever logic that meets
them, satisfies both theorems.

TLAPS, the TLA+ proof system, is a platform for the development and
mechanical verification of TLA+ proofs written in a declarative style requiring
little background beyond elementary mathematics. The language supports
hierarchical and non-linear proof construction and verification, and it is
independent of any verification tool or strategy. A Proof Manager uses backend
verifiers such as theorem provers, proof assistants, SMT solvers, and decision
procedures to check TLA+ proofs. This paper documents the first public release
of TLAPS, distributed with a BSD-like license.

Asynchronous programming is a ubiquitous systems programming idiom to manage
concurrent interactions with the environment. In this style, instead of waiting
for time-consuming operations to complete, the programmer makes a non-blocking
call to the operation and posts a callback task to a task buffer that is
executed later when the time-consuming operation completes. A co-operative
scheduler mediates the interaction by picking and executing callback tasks from
the task buffer to completion (and these callbacks can post further callbacks
to be executed later).

In this paper we investigate to which extent a very simple and natural
"reachability as deducibility" approach, originated in the research in formal
methods in security, is applicable to the automated verification of large
classes of infinite state and parameterized systems. The approach is based on
modeling the reachability between (parameterized) states as deducibility
between suitable encodings of states by formulas of first-order predicate
logic. The verification of a safety property is reduced to a pure logical
problem of finding a countermodel for a first-order formula.

The 4th Workshop on Membrane Computing and Biologically Inspired Process
Calculi (MeCBIC 2010) is organized in Jena as a satellite event of the Eleventh
International Conference on Membrane Computing (CMC11). Biological membranes
play a fundamental role in the complex reactions which take place in cells of
living organisms. The importance of this role has been considered in two
different types of formalisms introduced recently.

The paper describes an abstraction for protocols that are based on multiple
rounds of Chaum's Dining Cryptographers protocol. It is proved that the
abstraction preserves a rich class of specifications in the logic of knowledge,
including specifications describing what an agent knows about other agents'
knowledge. This result can be used to optimize model checking of Dining
Cryptographers-based protocols, and applied within a methodology for
knowledge-based program implementation and verification.

In a constraint satisfaction problem (CSP) the goal is to find an assignment
of a given set of variables subject to specified constraints. A global
cardinality constraint is an additional requirement that prescribes how many
variables must be assigned a certain value. We study the complexity of the
problem CCSP(G), the constraint satisfaction problem with global cardinality
constraints that allows only relations from the set G.

The PALS architecture reduces distributed, real-time asynchronous system
design to the design of a synchronous system under reasonable requirements.
Assuming logical synchrony leads to fewer system behaviors and provides a
conceptually simpler paradigm for engineering purposes. One of the current
limitations of the framework is that from a set of independent "synchronous
machines", one must compose the entire synchronous system by hand, which is
tedious and error-prone.

Distributed embedded systems (DESs) are no longer the exception; they are the
rule in many application areas such as avionics, the automotive industry,
traffic systems, sensor networks, and medical devices. Formal DES specification
and verification is challenging due to state space explosion and the need to
support real-time features. This paper reports on an extensive industry-based
case study involving a DES product family for a pedestrian and car 4-way
traffic intersection in which autonomous devices communicate by asynchronous
message passing without a centralized controller.

This paper presents a rewriting-logic-based modeling and analysis technique
for physical systems, with focus on thermal systems.

Orc is a theory of orchestration of services that allows structured
programming of distributed and timed computations. Several formal semantics
have been proposed for Orc, including a rewriting logic semantics developed by
the authors. Orc also has a fully fledged implementation in Java with
functional programming features.

We study logics defined in terms of second-order monadic monoidal and
groupoidal quantifiers. These are generalized quantifiers defined by monoid and
groupoid word-problems, equivalently, by regular and context-free languages. We
give a computational classification of the expressive power of these logics
over strings with varying built-in predicates. In particular, we show that
ATIME(n) can be logically characterized in terms of second-order monadic
monoidal quantifiers.

LF has been designed and successfully used as a meta-logical framework to
represent and reason about object logics. Here we design a representation of
the Isabelle logical framework in LF using the recently introduced module
system for LF. The major novelty of our approach is that we can naturally
represent the advanced Isabelle features of type classes and locales.

We present an approach to type theory in which the typing judgments do not
have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our
systems just have judgments of shape "A : B". A key feature is that we
distinguish free and bound variables even in pseudo-terms.

In this paper, we present an explicit substitution calculus which
distinguishes between ordinary bound variables and meta-variables. Its typing
discipline is derived from contextual modal type theory. We first present a
dependently typed lambda calculus with explicit substitutions for ordinary
variables and explicit meta-substitutions for meta-variables. We then present a
weak head normalization procedure which performs both substitutions lazily and
in a single pass thereby combining substitution walks for the two different
classes of variables.

Uncertainty in Logic Programming has been investigated during the last
decades, dealing with various extensions of the classical LP paradigm and
different applications. Existing proposals rely on different approaches, such
as clause annotations based on uncertain truth values, qualification values as
a generalization of uncertain truth values, and unification based on proximity
relations. On the other hand, the CLP scheme has established itself as a
powerful extension of LP that supports efficient computation over specialized
domains while keeping a clean declarative semantics.

Following a review of metric, ultrametric and generalized ultrametric, we
review their application in data analysis. We show how they allow us to explore
both geometry and topology of information, starting with measured data. Some
themes are then developed based on the use of metric, ultrametric and
generalized ultrametric in logic. In particular we study approximation chains
in an ultrametric or generalized ultrametric context.

Computability logic (CoL) (see this http URL) is a
recently introduced semantical platform and ambitious program for redeveloping
logic as a formal theory of computability, as opposed to the formal theory of
truth which logic has more traditionally been. Its expressions represent
interactive computational tasks seen as games played by a machine against the
environment, and "truth" is understood as existence of an algorithmic winning
strategy.

Structural operational semantics (SOS) is a technique for defining
operational semantics for programming and specification languages. Because of
its intuitive appeal and flexibility, SOS has found considerable application in
the study of the semantics of concurrent processes. It is also a viable
alternative to denotational semantics in the static analysis of programs and in
proving compiler correctness. Recently it has been applied in emerging areas
such as probabilistic systems and systems biology.

In context of efforts of composing category-theoretic and logical methods in
the area of knowledge representation we propose the notion of conceptory. We
consider intersection/union and other constructions in conceptories as
expressive alternative to category-theoretic (co)limits and show they have
features similar to (pro-, in-)jections. Then we briefly discuss approaches to
development of formal systems built on the base of conceptories and describe
possible application of such system to the specific ontology.

We give a real-time semantics for the concurrent, object-oriented modeling
language Creol, by mapping Creol processes to a network of timed automata. We
can use our semantics to verify real time properties of Creol objects, in
particular to see whether processes can be scheduled correctly and meet their
end-to-end deadlines. Real-time Creol can be useful for analyzing, for
instance, abstract models of multi-core embedded systems. We show how analysis
can be done in Uppaal.

Termination is an important and well-studied property for logic programs.
However, almost all approaches for automated termination analysis focus on
definite logic programs, whereas real-world Prolog programs typically use the
cut operator. We introduce a novel pre-processing method which automatically
transforms Prolog programs into logic programs without cuts, where termination
of the cut-free program implies termination of the original program. Hence
after this pre-processing, any technique for proving termination of definite
logic programs can be applied.

Querying over disjunctive ASP with functions is a highly undecidable task in
general. In this paper we focus on disjunctive logic programs with stratified
negation and functions under the stable model semantics (ASP^{fs}). We show
that query answering in this setting is decidable, if the query is finitely
recursive (ASP^{fs}_{fr}). Our proof yields also an effective method for query
evaluation. It is done by extending the magic set technique to ASP^{fs}_{fr}.
We show that the magic-set rewritten program is query equivalent to the
original one (under both brave and cautious reasoning).

We observe that the various formulations of the operational semantics of
Constraint Handling Rules proposed over the years fall into a spectrum ranging
from the analytical to the pragmatic. While existing analytical formulations
facilitate program analysis and formal proofs of program properties, they
cannot be implemented as is. We propose a novel operational semantics, which
has a strong analytical foundation, while featuring a terminating execution
model.

We present a form of algebraic reasoning for computational objects which are
expressed as graphs. Edges describe the flow of data between primitive
operations which are represented by vertices. These graphs have an interface
made of half-edges (edges which are drawn with an unconnected end) and enjoy
rich compositional principles by connecting graphs along these half-edges. In
particular, this allows equations and rewrite rules to be specified between
graphs. Particular computational models can then be encoded as an axiomatic set
of such rules.

This article presents the formal proof of correctness for a plane Delaunay
triangulation algorithm. It consists in repeating a sequence of edge flippings
from an initial triangulation until the Delaunay property is achieved. To
describe triangulations, we rely on a combinatorial hypermap specification
framework we have been developing for years. We embed hypermaps in the plane by
attaching coordinates to elements in a consistent way. We then describe what
are legal and illegal Delaunay edges and a flipping operation which we show
preserves hypermap, triangulation, and embedding invariants.

In this report we focus on some aspects related to modeling and formal
verification of embedded systems. Many models have been proposed to represent
embedded systems . These models encompass a broad range of styles,
characteristics, and application domains and include the extensions of finite
state machines, data flow graphs, communication processes and Petri nets.

Managing the software complexity of package-based systems can be regarded as
one of the main challenges in software architectures. Upgrades are required on
a short time basis and systems are expected to be reliable and consistent after
that. For each package in the system, a set of dependencies and a set of
conflicts have to be taken into account. Although this problem is
computationally hard to solve, efficient tools are required. In the best
scenario, the solutions provided should also be optimal in order to better
fulfill users requirements and expectations.

This volume contains the papers presented at the first international workshop
on Logics for Component Configuration (LoCoCo 2010) which was associated with
the International Conference on Theory and Applications of Satisfiability
Testing (SAT 2010) as part of the Federated Logic Conference (FLoC 2010), and
which took place on July 10, 2010 in Edinburgh, UK.

By considering probability distributions over the set of assignments the
expected truth values assignment to propositional variables are extended
through linear operators, and the expected truth values of the clauses at any
given conjunctive form are also extended through linear maps. The probabilistic
satisfiability problems are discussed in terms of the introduced linear
extensions. The case of multiple truth values is also discussed.

In this paper we revisit the well-known technique of predicate abstraction to
characterise performance attributes of system models incorporating probability.
We recast the theory using expectation transformers, and identify transformer
properties which correspond to abstractions that yield nevertheless exact bound
on the performance of infinite state probabilistic systems. In addition, we
extend the developed technique to the special case of "data independent"
programs incorporating probability.

We define a testing equivalence in the spirit of De Nicola and Hennessy for
reactive probabilistic processes, i.e. for processes where the internal
nondeterminism is due to random behaviour. We characterize the testing
equivalence in terms of ready-traces. From the characterization it follows that
the equivalence is insensitive to the exact moment in time in which an internal
probabilistic choice occurs, which is inherent from the original testing
equivalence of De Nicola and Hennessy.

The weakest pre-expectation calculus has been proved to be a mature theory to
analyze quantitative properties of probabilistic and nondeterministic programs.
We present an automatic method for proving quantitative linear properties on
any denumerable state space using iterative backwards fixed point calculation
in the general framework of abstract interpretation. In order to accomplish
this task we present the technique of random variable abstraction (RVA) and we
also postulate a sufficient condition to achieve exact fixed point computation
in the abstract domain.

The characterisation of termination using well-founded monotone algebras has
been a milestone on the way to automated termination techniques, of which we
have seen an extensive development over the past years. Both the semantic
characterisation and most known termination methods are concerned with global
termination, uniformly of all the terms of a term rewriting system (TRS). In
this paper we consider local termination, of specific sets of terms within a
given TRS.

While distributed systems with transfer of processes have become pervasive,
methods for reasoning about their behaviour are underdeveloped. In this paper
we develop a bisimulation technique for proving behavioural equivalence of such
systems modelled in the higher-order pi-calculus with passivation (and
restriction). Previous research for this calculus is limited to context
bisimulations and normal bisimulations which are either impractical or unsound.
In contrast, we provide a sound and useful definition of environmental
bisimulations, with several non-trivial examples.

We consider an extension of bi-intuitionistic logic with the traditional
modalities from tense logic Kt. Proof theoretically, this extension is obtained
simply by extending an existing sequent calculus for bi-intuitionistic logic
with typical inference rules for the modalities used in display logics.

In this paper, we show that the category of Mackey-complete, separated,
topological convex bornological vector spaces and bornological linear maps is a
differential category. Such spaces were introduced by Fr\"olicher and Kriegl,
where they were called convenient vector spaces. While much of the structure
necessary to demonstrate this observation is already contained in Fr\"olicher
and Kriegl's book, we here give a new interpretation of the category of
convenient vector spaces as a model of the differential linear logic of Ehrhard
and Regnier.

One technique to reduce the state-space explosion problem in temporal logic
model checking is symmetry reduction. The combination of symmetry reduction and
symbolic model checking by using BDDs suffered a long time from the
prohibitively large BDD for the orbit relation. Dynamic symmetry reduction
calculates representatives of equivalence classes of states dynamically and
thus avoids the construction of the orbit relation. In this paper, we present a
new efficient model checking algorithm based on dynamic symmetry reduction.

Algebraic lambda-calculi have been studied in various ways, but their
semantics remain mostly untouched. In this paper we propose a semantic analysis
of a general simply-typed lambda-calculus endowed with a structure of vector
space. We sketch the relation with two established vectorial lambda-calculi.
Then we study the problems arising from the addition of a fixed point
combinator and how to modify the equational theory to solve them. We sketch an
algebraic vectorial PCF and its possible denotational interpretations.

We present a reduction of the termination problem for a Turing machine (in
the simplified form of the Post correspondence problem) to the problem of
determining whether a continuous-time Markov chain presented as a set of Kappa
graph-rewriting rules has an equilibrium. It follows that the problem of
whether a computable CTMC is dissipative (ie does not have an equilibrium) is
undecidable.

Given a measurable space (X, M) there is a (Galois) connection between
sub-sigma-algebras of M and equivalence relations on X. On the other hand
equivalence relations on X are closely related to congruences on stochastic
relations. In recent work, Doberkat has examined lattice properties of posets
of congruences on a stochastic relation and motivated a domain-theoretic
investigation of these ordered sets.

We examine the relation of BSS-reducibility on subsets of the real numbers.
The question was asked recently (and anonymously) whether it is possible for
the halting problem H in BSS-computation to be BSS-reducible to a countable
set. Intuitively, it seems that a countable set ought not to contain enough
information to decide membership in a reasonably complex (uncountable) set such
as H. We confirm this intuition, and prove a more general theorem linking the
cardinality of the oracle set to the cardinality, in a local sense, of the set
which it computes.

We study and compare in two degree-theoretic ways (iterated Halting oracles
analogous to Kleene's arithmetical hierarchy and the Borel hierarchy of
descriptive set theory) the capabilities and limitations of three models of
analytic computation: BSS machines (aka real-RAM) and strongly/weakly analytic
machines as introduced by Hotz et. al. (1995).

Autoepistemic logic extends propositional logic by the modal operator L. A
formula that is preceded by an L is said to be "believed". The logic was
introduced by Moore 1985 for modeling an ideally rational agent's behavior and
reasoning about his own beliefs. In this paper we analyze all Boolean fragments
of autoepistemic logic with respect to the computational complexity of the
three most common decision problems expansion existence, brave reasoning and
cautious reasoning.

We investigate the expressiveness of backward jumps in a framework of
formalized sequential programming called program algebra. We show that - if
expressiveness is measured in terms of the computability of partial Boolean
functions - then backward jumps are superfluous. If we, however, want to
prevent explosion of the length of programs, then backward jumps are essential.

The extension of the Wagner hierarchy to blind counter automata accepting
infinite words with a Muller acceptance condition is effective. We determine
precisely this hierarchy.

Recursive relational specifications are commonly used to describe the
computational structure of formal systems. Recent research in proof theory has
identified two features that facilitate direct, logic-based reasoning about
such descriptions: the interpretation of atomic judgments through recursive
definitions and an encoding of binding constructs via generic judgments.
However, logics encompassing these two features do not currently allow for the
definition of relations that embody dynamic aspects related to binding, a
capability needed in many reasoning tasks.

We propose a method for automatically generating abstract transformers for
static analysis by abstract interpretation. The method focuses on linear
constraints on programs operating on rational, real or floating-point variables
and containing linear assignments and tests. Given the specification of an
abstract domain, and a program block, our method automatically outputs an
implementation of the corresponding abstract transformer. It is thus a form of
program transformation.

Dependently typed lambda calculi such as the Logical Framework (LF) can
encode relationships between terms in types and can naturally capture
correspondences between formulas and their proofs. Such calculi can also be
given a logic programming interpretation: the Twelf system is based on such an
interpretation of LF. We consider here whether a conventional logic programming
language can provide the benefits of a Twelf-like system for encoding type and
proof-and-formula dependencies.

In this paper we analyse various temporal formalisms, including
propositional/first-order linear temporal logics, branching temporal logics,
partial-order temporal logics, interval temporal logics, real-time temporal
logics and probabilistic temporal logics. We extrapolate the notions of
decidability, axiomatizability, expressiveness, model checking, etc. for each
logic analysed. We also provide a comparison of features of the temporal logics
discussed.

We study shedding in the setting of data linkage dynamics, a simple model of
computation that bears on the use of dynamic data structures in programming.
Shedding is complementary to garbage collection. With shedding, each time a
link to a data object is updated by a program, it is determined whether or not
the link will possibly be used once again by the program, and if not the link
is automatically removed. Thus, everything is made garbage as soon as it can be
viewed as garbage. By that, the effectiveness of garbage collection becomes
maximal.

We study techniques for deciding the computational complexity of
infinite-domain constraint satisfaction problems. For certain fundamental
algebraic structures Delta, we prove definability dichotomy theorems of the
following form: for every first-order expansion Gamma of Delta, either Gamma
has a quantifier-free Horn definition in Delta, or there is an element d of
Gamma such that all non-empty relations in Gamma contain a tuple of the form
(d,...,d), or all relations with a first-order definition in Delta have a
primitive positive definition in Gamma.

We embed Safe Recursion on Notation (SRN) into Light Affine Logic by Levels
(LALL), derived from the logic L4. LALL is an intuitionistic deductive system,
with a polynomial time cut elimination strategy.

Simple type theory is suited as framework for combining classical and
non-classical logics. This claim is based on the observation that various
prominent logics, including (quantified) multimodal logics and intuitionistic
logics, can be elegantly embedded in simple type theory. Furthermore, simple
type theory is sufficiently expressive to model combinations of embedded logics
and it has a well understood semantics. Off-the-shelf reasoning systems for
simple type theory exist that can be uniformly employed for reasoning within
and about combinations of logics.

The main goal of our work is to formally prove the correctness of the key
commands of the SCHUR software, an interactive program for calculating with
characters of Lie groups and symmetric functions. The core of the computations
relies on enumeration and manipulation of combinatorial structures. As a first
"proof of concept", we present a formal proof of the conjugate function,
written in C. This function computes the conjugate of an integer partition. To
formally prove this program, we use the Frama-C software.

Fixed point logics have a wide range of applications in computer science, in
particular in artificial intelligence and concurrency. The most expressive
logics of this type are the mu-calculus and its relatives. However, popular
fixed point logics tend to trade expressivity for simplicity and readability,
and in fact often live within the single variable fragment of the mu-calculus.
The family of such flat fixed point logics includes, e.g., CTL, the
*-nesting-free fragment of PDL, and the logic of common knowledge.

An important problem that arises during the execution of service-based
applications concerns the ability to determine whether a running service can be
substituted with one with a different interface, for example if the former is
no longer available.

We investigate a subclass of well-structured transition systems (WSTS), the
bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete
deterministic ones, which we claim provide an adequate basis for the study of
forward analyses as developed by Finkel and Goubault-Larrecq (ICALP 2009).
Indeed, we prove that, unlike other conditions considered previously for the
termination of forward analysis, boundedness is decidable.

We study the automatic synthesis of fair non-repudiation protocols, a class
of fair exchange protocols, used for digital contract signing. First, we show
how to specify the objectives of the participating agents and the trusted third
party (TTP) as path formulas in LTL and prove that the satisfaction of these
objectives imply fairness and abuse-freeness; properties required of fair
exchange protocols. We then show that weak (co-operative) co-synthesis and
classical (strictly competitive) co-synthesis fail, whereas assume-guarantee
synthesis (AGS) succeeds.

Gist is a tool that (a) solves the qualitative analysis problem of turn-based
probabilistic games with {\omega}-regular objectives; and (b) synthesizes
reasonable environment assumptions for synthesis of unrealizable
specifications. Our tool provides the first and efficient implementations of
several reduction-based techniques to solve turn-based probabilistic games, and
uses the analysis of turn-based probabilistic games for synthesizing
environment assumptions for unrealizable specifications.

We see how nested sequents, a natural generalisation of hypersequents, allow
us to develop a systematic proof theory for modal logics. As opposed to other
prominent formalisms, such as the display calculus and labelled sequents,
nested sequents stay inside the modal language and allow for proof systems
which enjoy the subformula property in the literal sense. In the first part we
study a systematic set of nested sequent systems for all normal modal logics
formed by some combination of the axioms for seriality, reflexivity, symmetry,
transitivity and euclideanness.

In a model-based testing approach as well as for the verification of
properties, B models provide an interesting solution. However, for industrial
applications, the size of their state space often makes them hard to handle. To
reduce the amount of states, an abstraction function can be used, often
combining state variable elimination and domain abstractions of the remaining
variables. This paper complements previous results, based on domain abstraction
for test generation, by adding a preliminary syntactic abstraction phase, based
on variable elimination.

Often one has a preference order among the different systems that satisfy a
given specification. Under a probabilistic assumption about the possible
inputs, such a preference order is naturally expressed by a weighted automaton,
which assigns to each word a value, such that a system is preferred if it
generates a higher expected value.

Shape types are a general concept of process types which work for many
process calculi. We extend the previously published Poly* system of shape types
to support name restriction. We evaluate the expressiveness of the extended
system by showing that shape types are more expressive than an implicitly typed
pi-calculus and an explicitly typed Mobile Ambients. We demonstrate that the
extended system makes it easier to enjoy advantages of shape types which
include polymorphism, principal typings, and a type inference implementation.

Graph transformation has been used to model concurrent systems in software
engineering, as well as in biochemistry and life sciences. The application of a
transformation rule can be characterised algebraically as construction of a
double-pushout (DPO) diagram in the category of graphs. We show how
intuitionistic linear logic can be extended with resource-bound quantification,
allowing for an implicit handling of the DPO conditions, and how resource logic
can be used to reason about graph transformation systems.

We view channels as the main form of resources in a message-passing
programming paradigm. These channels need to be carefully managed in settings
where resources are scarce. To study this problem, we extend the pi-calculus
with primitives for channel allocation and deallocation and allow channels to
be reused to communicate values of different types. Inevitably, the added
expressiveness increases the possibilities for runtime errors. We define a
substructural type system which combines uniqueness typing and affine typing to
reject these ill-behaved programs.

We present two rewriting systems that define labelled explicit substitution
lambda-calculi. Our work is motivated by the close correspondence between
Levy's labelled lambda-calculus and paths in proof-nets, which played an
important role in the understanding of the Geometry of Interaction.