Compact Difference Bound Matrices
Abstract elided by the publisher.
613 papers · page 8 of 31
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
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…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
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 …
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
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…
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…