Continuous queries over data streams may suffer from blocking operations
and/or unbound wait, which may delay answers until some relevant input arrives
through the data stream. These delays may turn answers, when they arrive,
obsolete to users who sometimes have to make decisions with no help whatsoever.
Therefore, it can be useful to provide hypothetical answers - "given the
current information, it is possible that X will become true at time t" -
instead of no information at all.
In this paper we present a semantics for queries and corresponding answers
that covers such hypothetical answers, together with an online algorithm for
updating the set of facts that are consistent with the currently available
information.

more |
pdf
| html
None.

arxivml:
"Hypothetical answers to continuous queries over data streams",
Luís Cruz-Filipe, Graça Gaspar, Isabel Nunes
https://t.co/JcCzZrwf4r

SciFi:
Hypothetical answers to continuous queries over data streams. https://t.co/TZQD55nUOY

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 9325

Unqiue Words: 2128

Set constraints provide a highly general way to formulate program analyses.
However, solving arbitrary boolean combinations of set constraints is
NEXPTIME-complete. Moreover, while theoretical algorithms to solve arbitrary
set constraints exist, they are either too complex to implement, or too slow to
ever run.
We present a translation that converts a set constraint formula into an SMT
problem. Our technique allows for arbitrary boolean combinations of positive or
negative set constraints, and leverages the performance of modern solvers such
as Z3. To show the usefulness of unrestricted set constraints, we use them to
devise a pattern match analysis for functional languages. This analysis ensures
that missing cases of pattern matches are always unreachable. We implement our
analysis in the Elm compiler and show that the our translation is fast enough
to be used in practical verification.

more |
pdf
| html
None.

EremondiJoey:
I'll be presenting my draft paper "Set Constraints, Pattern Match Analysis, and SMT" at TFP 2019!
https://t.co/o76ZSaZ6QL

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 0

Unqiue Words: 0

We address the problem of automatic decompilation, converting a program in
low-level representation back to a higher-level human-readable programming
language. The problem of decompilation is extremely important for security
researchers. Finding vulnerabilities and understanding how malware operates is
much easier when done over source code.
The importance of decompilation has motivated the construction of
hand-crafted rule-based decompilers. Such decompilers have been designed by
experts to detect specific control-flow structures and idioms in low-level code
and lift them to source level. The cost of supporting additional languages or
new language features in these models is very high.
We present a novel approach to decompilation based on neural machine
translation. The main idea is to automatically learn a decompiler from a given
compiler. Given a compiler from a source language S to a target language T ,
our approach automatically trains a decompiler that can translate (decompile) T
back to S . We used our framework to...

more |
pdf
| html
Miles_Brundage:
"Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

BrundageBot:
Towards Neural Decompilation. Omer Katz, Yuval Olshaker, Yoav Goldberg, and Eran Yahav https://t.co/6CrnJQCutq

NandoDF:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

rbhar90:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

judegomila:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

rquintino:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

mrdrozdov:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

suvsh:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

balicea1:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

AssistedEvolve:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

dmi_paras:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

urosn:
RT @Miles_Brundage: "Towards Neural Decompilation," Katz et al.: https://t.co/MLIHbuntRy

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 13606

Unqiue Words: 3185

We consider the problem of synthesizing a program given a probabilistic
specification of its desired behavior. Specifically, we study the recent
paradigm of distribution-guided inductive synthesis (DIGITS), which iteratively
calls a synthesizer on finite sample sets from a given distribution. We make
theoretical and algorithmic contributions: (i) We prove the surprising result
that DIGITS only requires a polynomial number of synthesizer calls in the size
of the sample set, despite its ostensibly exponential behavior. (ii) We present
a property-directed version of DIGITS that further reduces the number of
synthesizer calls, drastically improving synthesis performance on a range of
benchmarks.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 9491

Unqiue Words: 2645

Array-intensive programs are often amenable to parallelization across many
cores on a single machine as well as scaling across multiple machines and hence
are well explored, especially in the domain of high-performance computing.
These programs typically undergo loop transformations and arithmetic
transformations in addition to parallelizing transformations. Although a lot of
effort has been invested in improving parallelizing compilers, experienced
programmers still resort to hand-optimized transformations which is typically
followed by careful tuning of the transformed program to finally obtain the
optimized program. Therefore, it is critical to verify that the functional
correctness of an original sequential program is not sacrificed during the
process of optimization. In this paper, we cover important literature on
functional verification of array-intensive programs which we believe can be a
good starting point for one interested in this field.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 5674

Unqiue Words: 2042

D2d is an input format which allows experienced authors to create type
correct xml text objects with minimal disturbance of the creative flow of
writing. This paper contains the complete specification of the parsing process,
including the generation of error messages.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 4234

Unqiue Words: 1409

We propose an automated verification technique for hypersafety properties,
which express sets of valid interrelations between multiple finite runs of a
program. The key observation is that constructing a proof for a small
representative set of the runs of the product program (i.e. the product of the
several copies of the program by itself), called a reduction, is sufficient to
formally prove the hypersafety property about the program. We propose an
algorithm based on a counterexample-guided refinement loop that simultaneously
searches for a reduction and a proof of the correctness for the reduction. We
demonstrate that our tool Weaver is very effective in verifying a diverse array
of hypersafety properties for a diverse class of input programs.

more |
pdf
| html
None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 13227

Unqiue Words: 2934

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

*Tracking 131,277 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible