7,482 papers · page 221 of 375
This paper describes a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples pr…
We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type checkers to express. Converse…
We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of assertions by rewriting program…
Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent efforts to combine Separation Log…
Asynchronous or 'event-driven' programming is a popular technique to efficiently and flexibly manage concurrent interactions. In these programs, the programmer can post tasks that get stored in a task buffer and get executed atomically by a non-preemptive scheduler at a future po…
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics.
A concurrent data-structure implementation is considered nonblocking if it meets one of three following liveness criteria: waitfreedom, lock-freedom,orobstruction-freedom. Developers of nonblocking algorithms aim to meet these criteria. However, to date their proofs for non-trivi…
Transactional memory (TM) is a promising paradigm for concurrent programming. Whereas the number of TM implementations is growing, however, little research has been conducted to precisely define TM semantics, especially their progress guarantees. This paper is the first to formal…
We describe an abstract interpretation based framework for proving relationships between sizes of memory partitions. Instances of this framework can prove traditional properties such as memory safety and program termination but can also establish upper bounds on usage of dynamica…
This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple p…
Pointer analysis is a prerequisite for many program analyses, and the effectiveness of these analyses depends on the precision of the pointer information they receive. Two major axes of pointer analysis precision are flow-sensitivity and context-sensitivity, and while there has b…
Building concurrent shared-memory data structures is a notoriously difficult problem, and so the widespread move to multi-core and multi-processor hardware has led to increasing interest in language constructs that may make concurrent programming easier. One technique that has be…
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the…
Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to call-by-value programs. This hides looping bugs from the programmer, and changes the behavior of a program depending on whether it is optimized or not. We present a superco…
We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is transformed to an HORS that g…
In this paper, we show how pattern matching can be seen to arise from a proof term assignment for the focused sequent calculus. This use of the Curry-Howard correspondence allows us to give a novel coverage checking algorithm, and makes it possible to give a rigorous correctness …
We present HML, a type inference system that supports full first-class polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified types are used. This makes th…
Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data by using a change-propagation mechanism that updates computation by re-building only the parts affected by changes. Previous work has proposed language…
We study modular, automatic code generation from hierarchical block diagrams with synchronous semantics. Such diagrams are the fundamental model behind widespread tools in the embedded software domain, such as Simulink and SCADE. Code is modular in the sense that it is generated …
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests.