Concurrency Can't Be Observed, Asynchronously
Abstract elided by the publisher.
613 papers · page 17 of 31
Typechecking Higher-Order Security Libraries
Abstract elided by the publisher.
Metric Spaces and Termination Analyses
Abstract elided by the publisher.
A Provably Correct Stackless Intermediate Representation for Java Bytecode
Abstract elided by the publisher.
Interprocedural Control Flow Reconstruction
Abstract elided by the publisher.
A Certified Implementation of ML with Structural Polymorphism
Abstract elided by the publisher.
Data Structure Fusion
We consider the problem of specifying data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies; a novel fuse operation on…
Model Independent Order Relations for Processes
Abstract elided by the publisher.
A Logical Mix of Approximation and Separation
Abstract elided by the publisher.
Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics
Abstract elided by the publisher.
A Quick Tour of the VeriFast Program Verifier
This paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in separation logic, inductive data type and fixpoint definitions, lemma functions and…
Context-Preserving XQuery Fusion
Abstract elided by the publisher.
Categorical Descriptional Composition
Abstract elided by the publisher.
Live Heap Space Bounds for Real-Time Systems
Abstract elided by the publisher.
From a Verified Kernel towards Verified Systems
Abstract elided by the publisher.
Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates
Abstract elided by the publisher.
Type Inference for Sublinear Space Functional Programming
Abstract elided by the publisher.
A Calculus for Hybrid CSP
Abstract elided by the publisher.
Liberal Typing for Functional Logic Programs
Abstract elided by the publisher.
Reasoning about Computations Using Two-Levels of Logic
Abstract elided by the publisher.