Bi-Abduction with Pure Properties for Specification Inference
Abstract elided by the publisher.
613 papers · page 14 of 31
Dynamic Alias Protection with Aliasing Contracts
Abstract elided by the publisher.
Temporal Specification Mining for Anomaly Analysis
Abstract elided by the publisher.
Automated Inference of Library Specifications for Source-Sink Property Verification
Abstract elided by the publisher.
Ownership Types for Object Synchronisation
Abstract elided by the publisher.
Dynamic Software Update for Message Passing Programs
Abstract elided by the publisher.
Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis
Abstract elided by the publisher.
A Functional View of Imperative Information Flow
Abstract elided by the publisher.
A New Order-Theoretic Characterisation of the Polytime Computable Functions
We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order (sPOP⁎ for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term re…
End-to-end Multilevel Hybrid Information Flow Control
Abstract elided by the publisher.
Inference of Necessary Field Conditions with Abstract Interpretation
Abstract elided by the publisher.
A Generic Cyclic Theorem Prover
Abstract elided by the publisher.
Indexed Realizability for Bounded-Time Programming with References and Type Fixpoints
The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We present a realizability semantics for a higher-order functional lan…
Linear Approximation of Continuous Systems with Trapezoid Step Functions
Abstract elided by the publisher.
A Case for Behavior-Preserving Actions in Separation Logic
Abstract elided by the publisher.
Modular Verification of Concurrent Thread Management
Abstract elided by the publisher.
Vinter: A Vampire-Based Tool for Interpolation
Abstract elided by the publisher.
Succour to the Confused Deputy - Types for Capabilities
Abstract elided by the publisher.
Lazy v. Yield: Incremental, Linear Pretty-Printing
Abstract elided by the publisher.
Decision Procedures over Sophisticated Fractional Permissions
Abstract elided by the publisher.