Top 10 Arxiv Papers Today in Logic In Computer Science


2.076 Mikeys
#1. Precondition Inference via Partitioning of Initial States
Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J. Stuckey
Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of \emph{safe} and \emph{unsafe} \emph{initial} states. Then we repeatedly use the current abstractions to partition the program's \emph{initial} states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods.
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Precondition Inference via Partitioning of Initial States. https://t.co/i9zbDuESGm
Github

Preconditions inferrer for Horn clauses

Repository: PI-Horn
User: bishoksan
Language: Prolog
Stargazers: 0
Subscribers: 2
Forks: 0
Open Issues: 0
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 5
Total Words: 9466
Unqiue Words: 2161

2.027 Mikeys
#2. Spatial Logics and Model Checking for Medical Imaging (Extended Version)
Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink
Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces -- Closure Spaces being a generalisation of topological spaces, covering also discrete space structures -- and topochecker, a model-checker for SLCS (and extensions thereof). We introduce the logical language ImgQL ("Image Query Language"). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distancebased operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our...
more | pdf | html
Figures
Tweets
arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
arxivml: "Spatial Logics and Model Checking for Medical Imaging (Extended Version)", Fabrizio Banci Buonamici, Gina Belmonte… https://t.co/blLKoDwmDY
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
arxiv_cscv: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/stc0xvKGU4
ComputerPapers: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/DL0Gtf0GQc
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
Rosenchild: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
Rosenchild: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
bd_gfngfn: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPh9U9N
elazzouzim: RT @HubBucket: Spatial Logics and Model Checking for #MedicalImaging - Extended Version ⚕️https://t.co/cUk8ippRrX @HubBucket @HubMedX @Hu…
na4zagin3: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
nakano_muramoto: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
komorin9502: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
Bchoudhury_1: RT @arxiv_org: Spatial Logics and Model Checking for Medical Imaging (Extended Version). https://t.co/RWG7kMkfvY https://t.co/YLamwtP2q5
SandMouth: RT @arxiv_cslo: Spatial Logics and Model Checking for Medical Imaging (Extended Version) https://t.co/6zLAPhrv1l
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 5
Total Words: 19034
Unqiue Words: 4658

2.015 Mikeys
#3. Granularity and Generalized Inclusion Functions - Their Variants and Contamination
Mani A
Rough inclusion functions (RIFs) are known by many other names in formal approaches to vagueness, belief, and uncertainty. Their use is often poorly grounded in factual knowledge or involve wild statistical assumptions. The concept of contamination introduced and studied by the present author across a number of her papers, concerns mixing up of information across semantic domains (or domains of discourse). RIFs play a key role in contaminating algorithms and some solutions that seek to replace or avoid them have been proposed and investigated by the present author in some of her earlier papers. The proposals break many algorithms of rough sets in a serious way. In this research, algorithm-friendly granular generalizations of such functions that reduce contamination are proposed and investigated from a mathematically sound perspective. Interesting representation results are proved and a core algebraic strategy for generalizing Skowron-Polkowski style of rough mereology is formulated.
more | pdf | html
Figures
None.
Tweets
arxivml: "Granularity and Generalized Inclusion Functions - Their Variants and Contamination", Mani A https://t.co/Rw3gVHimwq
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 4758
Unqiue Words: 1564

2.01 Mikeys
#4. Progressive Algorithms for Domination and Independence
Grzegorz Fabiański, Michał Pilipczuk, Sebastian Siebertz, Szymon Toruńczyk
We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the distance-r dominating set problem (parameterized by the solution size) in a wide variety of restricted graph classes, such as powers of nowhere dense classes, map graphs, and (for $r=1$) biclique-free graphs. Similarly, for the distance-r independent set problem the technique can be used to give a linear-time fixed-parameter algorithm on any nowhere dense class. Despite the simplicity of the method, in several cases our results extend known boundaries of tractability for the considered problems and improve the best known running times.
more | pdf | html
Figures
Tweets
MathPaper: Progressive Algorithms for Domination and Independence. https://t.co/o5hWXr5TBQ
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 18056
Unqiue Words: 2598

2.003 Mikeys
#5. Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 steps with probability at most 1%." To this goal, we devise a theory of supermartingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those supermartingales. Our experiments suggest the method's practical use.
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments. https://t.co/ojJABUDgqP
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 15815
Unqiue Words: 3205

2.003 Mikeys
#6. Computing the Expected Execution Time of Probabilistic Workflow Nets
Philipp J. Meyer, Javier Esparza, Philip Offtermatt
Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of "earliest-first" schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P-hard, and so polynomial algorithms are very unlikely to exist. Further, #P-hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite...
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Computing the Expected Execution Time of Probabilistic Workflow Nets. https://t.co/p89RQBZn7Z
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 15074
Unqiue Words: 2550

2.002 Mikeys
#7. Revisiting the generalized Łoś-Tarski theorem
Abhisekh Sankaran
We present a new proof of the generalized {\L}o\'s-Tarski theorem ($\mathsf{GLT}(k)$) introduced in [1], over arbitrary structures. Instead of using $\lambda$-saturation as in [1], we construct just the "required saturation" directly using ascending chains of structures. We also strengthen the failure of $\mathsf{GLT}(k)$ in the finite shown in [2], by strengthening the failure of the {\L}o\'s-Tarski theorem in this context. In particular, we prove that not just universal sentences, but for each fixed $k$, even $\Sigma^0_2$ sentences containing $k$ existential quantifiers fail to capture hereditariness in the finite. We conclude with two problems as future directions, concerning the {\L}o\'s-Tarski theorem and $\mathsf{GLT}(k)$, both in the context of all finite structures. [1] 10.1016/j.apal.2015.11.001 ; [2] 10.1007/978-3-642-32621-9\_22
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Revisiting the generalized {\L}o\'s-Tarski theorem. https://t.co/GGGCzQbMCH
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVdRHkx
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVdRHkx
arxiv_cslo: Revisiting the generalized {\L}o\'s-Tarski theorem https://t.co/HQehVe9iJ7
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 7371
Unqiue Words: 1370

2.002 Mikeys
#8. Jets and differential linear logic
James Wallbridge
We prove that the category of vector bundles over a fixed smooth manifold and its corresponding functional analytic category of convenient modules are models for intuitionistic differential linear logic in two ways. The first uses the jet comonad to model the exponential modality. In this case the Kleisli category is the category of convenient modules with linear differential operators as morphisms. The second uses the more familiar distributional comonad whose Kleisli category is the category of convenient modules and smooth morphisms. Combining the two gives a new interpretation of the semantics of differential linear logic where the Kleisli morphisms are smooth local functionals, or equivalently, non-linear partial differential operators, and the codereliction map induces the functional derivative. This points towards a logic and hence computational theory of non-linear partial differential equations and their solutions based on variational calculus.
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Jets and differential linear logic. https://t.co/4eD68U6jke
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHwaeo
danielmurfet: RT @arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
JosephJohnCox: RT @arxiv_cslo: Jets and differential linear logic https://t.co/tRF8SHNL5W
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 13202
Unqiue Words: 2346

2.001 Mikeys
#9. Verified Runtime Validation for Partially Observable Hybrid Systems
Stefan Mitsch, Andre Platzer
Formal verification provides strong safety guarantees about models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation. The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor...
more | pdf | html
Figures
None.
Tweets
ComputerPapers: Verified Runtime Validation for Partially Observable Hybrid Systems. https://t.co/Y6CcAgJTY9
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV742ck
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV742ck
arxiv_cslo: Verified Runtime Validation for Partially Observable Hybrid Systems https://t.co/KyAbV6MrkM
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 12138
Unqiue Words: 2850

2.001 Mikeys
#10. On the specification and verification of atomic swap smart contracts
Ron van der Meyden
Blockchain systems and smart contracts provide ways to securely implement multi-party transactions without the use of trusted intermediaries, which currently underpin many commercial transactions. However, they do so by transferring trust to computer systems, raising the question of whether code can be trusted. Experience with high value losses resulting from incorrect code has already shown that formal verification of smart contracts is likely to be beneficial. This note investigates the specification and verification of a simple form of multi-party transaction, atomic swaps. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, for our specific examples, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through a number of examples of the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.
more | pdf | html
Figures
None.
Tweets
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFwKmON
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFwKmON
arxiv_cslo: On the specification and verification of atomic swap smart contracts https://t.co/POLZFx1Ydn
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 10089
Unqiue Words: 2294

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 58,338 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 58,338 papers.