Top 7 Arxiv Papers Today in Programming Languages


2.017 Mikeys
#1. Hypothetical answers to continuous queries over data streams
Luís Cruz-Filipe, Graça Gaspar, Isabel Nunes
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
Figures
None.
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 9325
Unqiue Words: 2128

2.003 Mikeys
#2. Set Constraints, Pattern Match Analysis, and SMT
Joseph Eremondi
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
Figures
None.
Tweets
EremondiJoey: I'll be presenting my draft paper "Set Constraints, Pattern Match Analysis, and SMT" at TFP 2019! https://t.co/o76ZSaZ6QL
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 0
Unqiue Words: 0

1.998 Mikeys
#3. Towards Neural Decompilation
Omer Katz, Yuval Olshaker, Yoav Goldberg, Eran Yahav
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
Figures
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 13606
Unqiue Words: 3185

1.998 Mikeys
#4. Efficient Synthesis with Probabilistic Constraints
Samuel Drews, Aws Albarghouthi, Loris D'Antoni
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 9491
Unqiue Words: 2645

1.997 Mikeys
#5. A Quick Introduction to Functional Verification of Array-Intensive Programs
Kunal Banerjee, Chandan Karfa
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 5674
Unqiue Words: 2042

1.997 Mikeys
#6. D2d -- XML for Authors
Markus Lepper, Baltasar Trancón y Widemann
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 4234
Unqiue Words: 1409

1.997 Mikeys
#7. Reductions for Automated Hypersafety Verification
Azadeh Farzan, Anthony Vandikas
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
Figures
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 13227
Unqiue Words: 2934

About

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.

Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 131,277 papers.