PPDP

Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in ...

We summarise the state of the art in automatic amortized resource analysis. We then focus on some recent applications to term rewriting with G. Moser and conclude with open problems and questions.

Ten years ago we introduced ReactiveML, an extension of a strict ML language with synchronous parallelism à la Esterel to program reactive applications. Our purpose was to demonstrate that synchronous language principles, originally invented and used ...

In a world where trusting software systems is problematic, formal methods and formal proofs should be able to help. Proof checking can play an important role in establishing trust since such checkers can be smaller and easier to verify than, for example,...

The Service Oriented Computing (SOC) paradigm is based on service composition, that is, loosely coupled autonomous heterogeneous services, which are collectively composed to implement a particular task. This paper presents a new calculus, called sbCSP, ...

Current research in planning focuses mainly on so called domain independent models using the Planning Domain Description Language (PDDL) as the domain modeling language. This declarative modeling approach embraces the idea of a physics-only model ...

We investigate the control of evaluation strategies in a variant of the Λ-calculus derived through the Curry-Howard correspondence from LJF, a sequent calculus for intuitionistic logic implementing the focusing technique. The proof theory of focused ...

This paper presents a proposal for debugging deductive database programs. Although inspired in the logic programming paradigm, these programs have the particularity of involving large sets of data. In this context, debugging tools employed usually in ...

Session-based concurrency is a type-based approach to the analysis of communication-intensive systems. Correct behavior in these systems may be specified in an operational or declarative style: the former defines how interactions are structured; the ...

Networks are complex systems that unfortunately are ridden with errors. Such errors can lead to disruption of services, which may have grave consequences. Verification of networks is key to eliminating errors and building robust networks. In this paper, ...

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it specializes, by using ...

A devil's advocate is one who argues against a claim, not as a committed opponent but in order to determine the validity of the claim. We are interested in a devil's advocate that argues against termination of a program. He does so by producing a ...

The popular cognitive architecture ACT-R is used in many cognitive models to explain cognitive features of human-beings. It has a well-defined psychological theory but lacks a formalization of its underlying computational system. This lack allows for ...

We propose a static analysis technique that computes upper bounds of virtual machine usages in a concurrent language with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third ...

Concolic testing is a software testing technique combining concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that give better path coverage than random test case generation). ...

We design a mutex library for Hop -- a dialect of Scheme which supports preemptive multithreading and shared memory -- that mixes deadlock prevention and deadlock avoidance to provide an easy to use, expressive, and safe locking function. This requires ...

We enrich spatial constraint systems with operators to specify information and processes moving from a space to another. We shall refer to these news structures as spatial constraint systems with extrusion. We shall investigate the properties of this ...

Constraint programming is traditionally presented as the combination of two components: a constraint model and a search procedure. In this paper we show that tree search procedures can be fully internalized in the constraint model with a fixed ...

We propose Lasp, a new programming model designed to simplify large-scale distributed programming. Lasp combines ideas from deterministic dataflow programming together with conflict-free replicated data types (CRDTs). This provides support for ...

It is well-known that monads are monoids in the category of endofunctors, and in fact so are applicative functors. Unfortunately, the benefits of this unified view are lost when the additional nondeterminism structure of MonadPlus or Alternative is ...

We propose the new logic programming language PrefLog, which is based on an infinite-valued logic in order to support operators for expressing preferences. We demonstrate that if the operators used are continuous over the infinite-valued underlying ...

An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is not increased in any context. This paper investigates improvements an untyped call-by-...

Manually detecting bugs in concurrent programs is hard due to the myriad of thread interleavings that needs to be accounted for. Higher-order programming features only exacerbate this difficulty. The need for tool support therefore increases as these ...

A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn ...