7,482 papers · page 250 of 375
Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstracti…
The goal of this work is to develop compile-time algorithms for automatically verifying properties of imperative programs that manipulate dynamically allocated storage. The paper presents an analysis method that uses a characterization of a procedure's behavior in which parts of …
Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has been used for many years. Perhaps surprisingly, there is little high-level understandi…
We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only s…
We describe a software error-detection tool that exploits recent advances in boolean satisfiability (SAT) solvers. Our analysis is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, which we achieve using two te…
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more expressive. We formalise that the …
Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. If we postulate soundness (in the sense that whenever a term is accused…
We extend Haskell with regular expression patterns. Regular expression patterns provide means for matching and extracting data which goes well beyond ordinary pattern matching as found in Haskell. It has proven useful for string manipulation and for processing structured data suc…
This paper presents an approach to searching for deadlocks in Concurrent Haskell programs. The search is based on a redefinition of the IO monad which allows the reversal of Concurrent Haskells concurrency primitives. Hence, it is possible to implement this search by a backtracki…
If a subexpression in a query will never contribute data to the query answer, this should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition f…
Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is non-trivial. This paper show…
This paper presents a methodology for implementing natural language morphology in the functional language Haskell. The main idea behind is simple: instead of working with untyped regular expressions, which is the state of the art of morphology in computational linguistics, we use…
We study a type system equipped with universal types and equire-cursive types, which we refer to as F͘. We show that type equality may be decided in time O(nlog n), an improvement over the previous known bound of O(n2 ). In fact, we show that two more general problems, namely ent…
Sometimes it's worth doing things badly in order to do them fast. When is this the right plan? Are some kinds of mistakes worse than others? Could the right infrastructure make trial and error programming more effective? How will it play out in the future?
A generic function is a function that can be instantiated on many data types to obtain data type specific functionality. Examples of generic functions are the functions that can be derived in Haskell, such as show, read, and '=='. The recent years have seen a number of proposals …
We present a process logic for the p -calculus with the linear/affine type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of behaviours ranging from pure…
Writing boilerplate code is a royal pain. Generic programming promises to alleviate this pain by allowing the programmer to write a generic "recipe" for boilerplate code, and use that recipe in many places. In earlier work we introduced the "Scrap your boilerplate" approach to ge…
As a company, Galois began its life with the mission simply of supplying functional programming services, building tools and products for clients, leveraging the productivity of functional languages and the abilities of our engineers. This went well, except that our business lack…