34233329
Search Trees with Relaxed Balance and Near-Optimal Height
We introduce the relaxed k-tree, a search tree with relaxed balance and a height bound, when in balance, of (1 + Ɛ) log2 n + 1, for any Ɛ > 0. The rebalancing work is amortized O(1/Ɛ) per update. This is the first binary search tree with relaxed balance having a height bound better than c ċ log2 n for a fixed constant c. In all previous proposals, the constant is at least 1/ log2 Φ > 1.44, where Φ is the golden ratio. 
 
As a consequence, we can also define a standard (non-relaxed) k-tree with amortized constant rebalancing per update, which is an improvement over the original definition. 
 
Search engines based on main-memory databases with strongly fluctuating workloads are possible applications for this line of work.
6986183
Efficient Simplification of Bisimulation Formulas
The problem of checking or optimally simplifying bisimulation formulas is likely to be computationally very hard. We take a different view at the problem: we set out to define a very fast algorithm, and then see what we can obtain. Sometimes our algorithm can simplify a formula perfectly, sometimes it cannot. However, the algorithm is extremely fast and can, therefore, be added to formula-based bisimulation model checkers at practically no cost. When the formula can be simplified by our algorithm, this can have a dramatic positive effect on the better, but also more time consuming, theorem provers which will finish the job.
80794
Efficient Rebalancing of Chromatic Search Trees
Chromatic trees were defined by Nurmi and Soisalon-Soininen, as a new type of binary search tree for databases. The aim is to improve runtime performance by allowing a greater degree of concurrency, which, in turn, is obtained by uncoupling updating from rebalancing. This also allows rebalancing to be postponed completely or partially until after peak working hours. The advantages of the proposal of Nurmi and Soisalon-Soininen are quite significant, but there are definite problems with it. First, they give no explicit upper bound on the complexity of their algorithm. Second, some of their rebalancing operations can be applied many more times than necessary. Third, some of their operations, when removing one problem, create another. We define a new set of rebalancing operations which we prove give rise to at most @?log"2(N+1)@?-1 rebalancing operations per insertion and at most @?log"2(N+1)@?-2 rebalancing operations per deletion, where N is the maximum size the tree could ever have, given its initial size and the number of insertions performed. Most of these rebalancing operations, in fact, do no restructuring; they simply move weights around. The number of operations which actually change the structure of the tree is at most one per update.
27033090
Exponentially Decreasing Number of Operations in Balanced Trees
While many tree-like structures have been proven to support amortized constant number of operations after updates, considerably fewer structures have been proven to support the more general exponentially decreasing number of operations with respect to distance from the update. In addition, all existing proofs of exponentially decreasing operations are tailor-made for specific structures. We provide the first formalization of conditions under which amortized constant number of operations imply exponentially decreasing number of operations. Since our proof is constructive, we obtain the constants involved immediately. Moreover, we develop a number of techniques to improve these constants.
12699441
Fully abstract models for a process language with refinement
We study the use of sets of labelled partial orders (pomsets) as denotational models for process algebras. More specifically, we study their capability to capture degrees of nonsequentiality of processes. We present four full abstractness results. The operational equivalences are based on maximal action-sequences and step-sequences — defined for a very simple process language and its extensions with a refinement combinator (change of atomicity). The denotational models are all expressed as abstractions of a standard association of sets of labelled partial orders with processes.
30882911
Complexity of Layered Binary Search Trees with Relaxed Balance
When search trees are made relaxed, balance constraints are weakened such that updates can be made without immediate rebalancing. This can lead to a speed-up in some circumstances. However, the weakened balance constraints also make it more challenging to prove complexity results for relaxed structures.In our opinion, one of the simplest and most intuitive presentations of balanced search trees has been given via layered trees. We show that relaxed layered trees are among the best of the relaxed structures. More precisely, rebalancing is worst-case logarithmic and amortized constant per update, and restructuring is worst-case constant per update.
39576178
Resource-Efficient Scheduling for Real Time Systems
For embedded systems efficient utilization of resources is an acute problem arising from the increasing computational demands in all sorts of applications. The consumers constantly demand better functionality and flexibility of embedded products which imply an increase in the resources needed for their realization. In several areas – e.g. portable devices such as PDAs, mobile phones and laptops as well as mission critical systems such as space applications – the ability to design resource efficient solutions is crucial.
2304363
Time-Optimal Real-Time Test Case Generation Using Uppaal
Testing is the primary software validation technique used by industry today, but remains ad hoc, error prone, and very expensive. A promising improvement is to automatically generate test cases from formal models of the system under test.
6559743
A refinement logic for the fork calculus
The Fork Calculus FC presents a theory of communicating systems in family with CCS, but it differs in the way that processes are put in parallel. In CCS there is a binary parallel operator |, whereas FC contains a unary fork operator. We provide FC with an operational semantics, together with a congruence relation between processes. Further, a refinement logic for program specification and design is presented. In this logic it is possible to freely mix programming constructs with specification constructs, thereby allowing us to define a compositional proof system. The proof rules of this system are applied to a non-trivial example.
5725449
Verification of an Audio Protocol with Bus Collision Using UPPAAL
In this paper we apply the tool Uppaal1 to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly larger than the real-time/hybrid systems previously analysed by automatic tools. During the case study the tool Uppaal was extended with a new feature, committed locations, allowing efficient modelling of broadcast communication.
12983032
Practical verification of embedded software
Using a new verification algorithm called the compositional backward technique, the authors demonstrate that they can exhaustively verify even the largest industrial applications-comprising more than 1,000 components-in a few minutes on a standard PC.