613 papers · page 4 of 31
We present a complete optimization procedure for hybrid quantum-classical circuits with classical parity logic. While common optimization techniques for quantum algorithms focus on rewriting solely the pure quantum segments, there is interest in applying a global optimization pro…
Abstract elided by the publisher.
Abstract elided by the publisher.
Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. This interface should provide for originating and invoking contracts as well as observing the state of th…
Datalog has become a popular implementation language for solving large-scale, real-world problems, including bug finders, network analysis tools, and disassemblers. These applications express complex behaviour with hundreds of relations and rules that often require a non-determin…
Abstract elided by the publisher.
Abstract elided by the publisher.
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approxi…
Abstract elided by the publisher.
We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can …
The Go programming language is an increasingly popular language but some of its features lack a formal investigation. This article explains Go's resolution mechanism for overloaded methods and its support for structural subtyping by means of translation from Featherweight Go …
Abstract elided by the publisher.
As neural networks are trained to be deeper and larger, the scalability of neural network analyzers is urgently required. The main technical insight of our method is modularly analyzing neural networks by segmenting a network into blocks and conduct the analysis for each block. I…
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $\lambda$-calculus. It is derived using Danvy et al.'s functional correspondence from Cregut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation…
We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling…
Stream Runtime Verification is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing to compute richer verdicts than Booleans (including quantitative and arbitrary data). In this paper we …
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.