AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
Abstract elided by the publisher.
613 papers · page 10 of 31
Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Abstract elided by the publisher.
Higher-Order Model Checking in Direct Style
Abstract elided by the publisher.
SPEC: An Equivalence Checker for Security Protocols
Abstract elided by the publisher.
A Sound and Complete Bisimulation for Contextual Equivalence in \lambda -Calculus with Call/cc
Abstract elided by the publisher.
Unified Syntax with Iso-types
Abstract elided by the publisher.
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation
Abstract elided by the publisher.
A Strong Distillery
Abstract machines for the strong evaluation of \(\lambda \)-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest…
Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics
Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $\epsilon \in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $\epsilon_i \epsilon_j$. In static analysis, the zonotope domai…
Transactions on Mergeable Objects
Abstract elided by the publisher.
Programming Techniques for Reversible Comparison Sorts
Abstract elided by the publisher.
Randomized Resource-Aware Path-Sensitive Static Analysis
Abstract elided by the publisher.
Bottom-Up Context-Sensitive Pointer Analysis for Java
Abstract elided by the publisher.
Objects in Polynomial Time
Abstract elided by the publisher.
A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
Abstract elided by the publisher.
Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques
Abstract elided by the publisher.
Decision Algorithms for Checking Definability of Order-2 Finitary PCF
Abstract elided by the publisher.
A Secure Compiler for ML Modules
Abstract elided by the publisher.
Abstraction of Optional Numerical Values
Abstract elided by the publisher.
Tree-Like Grammars and Separation Logic
Abstract elided by the publisher.