FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover ...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily d...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
This paper is concerned with Freeze LTL, a temporal logic on data words with registers. In a (multi-attributed) data word each position carries a letter from a finite alphabet and...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
Abstract. We first develop a (semantical) characterization of call-byneed normalization by means of typability, i.e. we show that a term is normalizing in call-by-need if and only...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs a...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
We introduce a class of transformations of finite data words generalizing the well-known class of regular finite string transformations described by MSO-definable transductions ...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
Focusing is a general technique for transforming a sequent proof system into one with a syntactic separation of non-deterministic choices without sacrificing completeness. This no...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
The task of program slicing is to remove the parts of a program that are irrelevant in a given context. In probabilistic programs, where variables may be assigned random values fr...
FOSSACS
2016
Springer
8 years 3 months ago
2016
Springer
We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These Unordered Data...
FASE
2016
Springer
8 years 3 months ago
2016
Springer
Despite its recent popularity, program verification has to face practical limitations hindering its everyday use. One of these issues is scalability, both in terms of time and mem...