Compact Difference Bound Matrices
Abstract elided by the publisher.
613 papers · page 8 of 31
Black-Box Equivalence Checking Across Compiler Optimizations
Abstract elided by the publisher.
A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, \(\lambda _\rho \), follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as d…
Enforcing Programming Guidelines with Region Types and Effects
We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over a…
Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications
Abstract elided by the publisher.
Programming by Examples: PL Meets ML
Abstract elided by the publisher.
Capabilities for Java: Secure Access to Resources
Abstract elided by the publisher.
Counterexample-Guided Bit-Precision Selection
Abstract elided by the publisher.
Safety and Liveness of MCS Lock - Layer by Layer
Abstract elided by the publisher.
Decision Procedure for Entailment of Symbolic Heaps with Arrays
This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially …
Sound and Efficient Language-Integrated Query - Maintaining the ORDER
Abstract elided by the publisher.
Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects
Abstract elided by the publisher.
Implementing Algebraic Effects in C - "Monads for Free in C"
Abstract elided by the publisher.
Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
Abstract elided by the publisher.
Programming and Proving with Classical Types
Abstract elided by the publisher.
A Nonstandard Functional Programming Language
Abstract elided by the publisher.
Verified Root-Balanced Trees
Abstract elided by the publisher.
Sharper and Simpler Nonlinear Interpolants for Program Verification
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent result by Dai et al.\ that combines real algebraic geometry and SDP optimization in synthesis of polynomi…
Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous
We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Push…
Efficient Functional Reactive Programming Through Incremental Behaviors
Many types of software are inherently event-driven ranging from web applications to embedded devices and traditionally, such applications are implemented using imperative callbacks. An alternative approach to writing such programs is functional reactive programming (FRP). FRP off…