VLDB 2026 Research / reviewers in the wild / expert
Magne Haveraaen
dblp:55/4636
· DBLP profile ↗
10ranked-venue papers
4as first author
2since 2021 · last 2026
0000-0003-0836-8347ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 7 · 2 first-author · 2 since 2021Systems, architecture and hardware · 2 · 2 first-authorTheory of computation · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Algebraic reasoning for timeliness-guided system design
Seyed Hossein Haeri, Peter Van Roy, Heinrich Apfelmus, Peter Thompson 0002, Neil Davies 0001, Magne Haveraaen, Mikhail Barash, Kevin Hammond, James Chapman 0001, Artjoms Sinkarovs |
J. Log. Algebraic Methods Program. | 6 |
| 2021 | Semantics of multiway dataflow constraint systemsabstractMultiway dataflow constraint systems (MDCS) is a programming model where statements are not executed in a predetermined order. Rather, individual methods are selected from specific method sets and then executed to achieve a desired global state. The selection is done by a planner, which typically bases the choice of methods on the history of updates to the global state. MDCS is well suited for describing user interface logic where choosing what code to execute depends in complicated ways on the history of user interactions and on data availability. User interfaces are the domain of examples in this paper. Much of the research into MDCS has been on planning algorithms and their efficiency. Here we investigate a semantic setting for MDCS, introducing dataflow constraints as modules with explicit goals and related method sets. MDCS is defined in a similar manner, with an explicit goal and a set of supporting dataflow constraints. This enables verification and testing of methods and dataflow constraints against the goals. The exposition is based on abstract syntax for an idealised programming language with global variables. On top of this we define a modular reuse mechanism for dataflow constraints based on Goguen-Burstall institution theory. We show how this setup enables reuse in user interfaces; traditionally code that defines user interface logic is almost invariably non-reusable. Magne Haveraaen, Jaakko Järvi |
J. Log. Algebraic Methods Program. | 1 |
| 2020 | Specifying with syntactic theory functorsabstractWe propose a framework, syntactic theory functors (STFs), for creating syntactic structuring mechanisms for specification languages. Good support for common reuse patterns is important for systematically developing specifications for large systems. Though immaterial to foundational theory, lack of support otherwise causes lengthy writing of boilerplate code or repeated adaptation from one context to another. We present STFs in the context of the Goguen & Burstall institution theory. This theory captures the essential structure of ontologies, modelling and formal specifications (OMS). In particular it provides powerful structuring mechanisms that are independent of the specification formalism, i.e., they are institution-independent. The presented STF framework is institution-independent as well. As such it encompasses many approaches to software and information systems. STFs subsume the standard institution-independent structuring mechanisms, and open up new ways of reusing existing and structuring new specifications. In this, STFs subsume and enrich the tool-set of ‘good practices’, which includes separation of concerns, ease of reuse of specification-text, and improved theorem proving support. STFs are aimed at structuring and reuse beyond the classical mechanisms. However, most STFs are institution-specific and support specific reuse patterns in that institution. With such institution-specific STFs it is possible to incrementally grow more complex institutions from simpler ones. This is very much needed when developing ontologies or specification languages for a new domain. In this paper, we motivate STFs with examples in Casl, the common standard algebraic specification language. We further demonstrate how STFs can ease specification through capturing repeated constructions once and for all as patterns formulated as STFs. Magne Haveraaen, Markus Roggenbach |
J. Log. Algebraic Methods Program. | 1 |
| 2014 | Specializing planners for hierarchical multi-way dataflow constraint systemsabstractA constraint system consists of variables and a set of constraints on those variables. To solve a constraint system is to find a valuation that satisfies all constraints; or the "best" subset of constraints if not all can simultaneously be satisfied. In a multi-way dataflow constraint system, solving requires selecting a set of user-defined functions which, when executed, will enforce the constraints. The task of selecting these functions is called planning. The planner has two kinds of input: the specification of the constraints and an order of priority for those constraints. The former typically changes seldom, while the latter frequently, making constraint planning a potential application for program specialization. This paper shows how to generate specialized planners for hierarchical multi-way dataflow constraint systems when the constraints are known in advance. The specialized planners are DFAs; they can be an order of magnitude or more faster than a general purpose planner for the same system. Our applications for constraint systems are in user interface programming, where constraint systems determine how a GUI should react to user interaction---specialized planners can help to ensure that GUIs' responses to user interaction are instantaneous. Jaakko Järvi, Gabriel Foust, Magne Haveraaen |
GPCE | 3 |
| 2009 | The axioms strike back: testing with concepts and axioms in C++abstractModern development practises encourage extensive testing of code while it is still under development, using unit tests to check individual code units in isolation. Such tests are typically case-based, checking a likely error scenario or an error that has previously been identified and fixed. Coming up with good test cases is challenging, and focusing on individual tests can distract from creating tests that cover the full functionality.Axioms, known from program specification, allow for an alternative way of generating test cases, where the intended functionality is described as rules or equations that can be checked automatically. Axioms are proposed as part of the concept feature of the upcoming C++0x standard.In this paper, we describe how tests may be generated automatically from axioms in C++ concepts, and supplied with appropriate test data to form effective automated unit tests. Anya Helene Bagge, Valentin David, Magne Haveraaen |
GPCE | 3 |
| 2009 | Concepts as Syntactic SugarabstractThe coming standard for C++ will contain language extensions. It can be expected that there will be some years between the release of the new standard and the time when most compilers will be compliant, like it happened for the 1998 standard. Concepts are an extension proposed for the new standard. We show how we can translate ConceptC++ code into pure C++03 using the C++ template mechanism. Such a translation tool could be used for example to port software written using a ConceptC++ compiler to architectures having only older compilers. Or a library written using concepts could be used by a project written in pure C++. The goal of this transformation is not to provide all capabilities of ConceptC++, but with restrictions we can afford, to be as simple as possible. Valentin David, Magne Haveraaen |
SCAM | 2 |
| 2006 | Stayin' alert: : moulding failure and exceptions to your needsabstractDealing with failure and exceptional situations is an important but tricky part of programming, especially when reusing existing components. Traditionally, it has been up to the designer of a library to decide whether to use a language's exception mechanism, return values, or other ways to indicate exceptional circumstances. The library user has been bound by this choice, even though it may be inconvenient for a particular use. Furthermore, normal program code is often cluttered with code dealing with exceptional circumstances.This paper introduces an alert concept which gives a uniform interface to all failure mechanisms. It separates the handling of an exceptional situation from reporting it, and allows for retro-fitting this for existing libraries. For instance, we may easily declare the error codes of the POSIX C library for file handling, and then use the library functions as if C had been extended with an exception mechanism for these functions -- a moulding of failure handling to the user's needs, independently of the library designer's choices. Anya Helene Bagge, Valentin David, Magne Haveraaen, Karl Trygve Kalleberg |
GPCE | 3 |
| 2001 | Computation AlgebrasabstractWe introduce a framework that generalizes algebraic specifications by equipping algebras with descriptions of evaluation strategies. The resulting abstract mathematical description allows one to model the implementation of algebras on various platforms in a way that is independent of the function-oriented specifications. We study algebras with associated data dependencies. The latter provide separate means for modelling computational aspects apart from the functional specifications captured by an algebra. The formalization of evaluation strategies (1) introduces increased portability among different hardware platforms, and (2) allows a potential increase in execution efficiency, since a chosen evaluation strategy may be tailored to a particular platform. We present the development process where algebraic specifications are equipped with data dependencies, the latter are refined, and, finally, mapped to actual hardware architectures. Michal Walicki, Magne Haveraaen, Sigurd Meldal |
Math. Struct. Comput. Sci. | 2 |
| 2000 | Efficient Parallelisation of Recursive Problems Using Constructive Recursion (Research Note)
Magne Haveraaen |
Euro-Par | 1 |
| 1990 | Distributing Programs on Different Parallel Architectures
Magne Haveraaen |
ICPP (2) | 1 |