Compositional Entailment Checking for a Fragment of Separation Logic
Abstract elided by the publisher.
613 papers · page 12 of 31
Resource Analysis of Complex Programs with Cost Equations
Abstract elided by the publisher.
A Translation of Intersection and Union Types for the λμ-Calculus
Abstract elided by the publisher.
Inferring Grammatical Summaries of String Values
Abstract elided by the publisher.
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
Abstract elided by the publisher.
NetKAT - A Formal System for the Verification of Networks
Abstract elided by the publisher.
Optimized Compilation of Multiset Rewriting with Comprehensions
Abstract elided by the publisher.
Functional Pearl: Nearest Shelters in Manhattan
Abstract elided by the publisher.
Types for Flexible Objects
Abstract elided by the publisher.
Syntax-Directed Divide-and-Conquer Data-Flow Analysis
Abstract elided by the publisher.
Call-by-Value in a Basic Logic for Interaction
Abstract elided by the publisher.
Necessary and Sufficient Preconditions via Eager Abstraction
The precondition for safe execution of a procedure is useful for understanding, verifying and debugging programs. We have previously presented a cegar-based approach for inferring necessary and sufficient preconditions based on the iterative abstraction-refinement of the set of s…
Address Chain: Profiling Java Objects without Overhead in Java Heaps
Abstract elided by the publisher.
Model-Checking for Android Malware Detection
Abstract elided by the publisher.
Automatic Memory Management Based on Program Transformation Using Ownership
Abstract elided by the publisher.
A ZDD-Based Efficient Higher-Order Model Checking Algorithm
Abstract elided by the publisher.
The Essence of Ruby
Abstract elided by the publisher.
A Method for Scalable and Precise Bug Finding Using Program Analysis and Model Checking
Abstract elided by the publisher.
The Proof Assistant as an Integrated Development Environment
Abstract elided by the publisher.
Environmental Bisimulations for Delimited-Control Operators
We present a theory of environmental bisimilarity for the delimited-control operators shift and reset. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one…