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
None.

ComputerPapers:
Precondition Inference via Partitioning of Initial States. https://t.co/i9zbDuESGm

Preconditions inferrer for Horn clauses

Stargazers: 0

Subscribers: 2

Subscribers: 2

Forks: 0

Open Issues: 0

Open Issues: 0

None.

Sample Sizes : None.

Authors: 5

Total Words: 9466

Unqiue Words: 2161

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
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

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

None.

None.

Sample Sizes : None.

Authors: 5

Total Words: 19034

Unqiue Words: 4658

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
None.

arxivml:
"Granularity and Generalized Inclusion Functions - Their Variants and Contamination",
Mani A
https://t.co/Rw3gVHimwq

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 4758

Unqiue Words: 1564

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
MathPaper:
Progressive Algorithms for Domination and Independence. https://t.co/o5hWXr5TBQ

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 18056

Unqiue Words: 2598

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
None.

ComputerPapers:
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments. https://t.co/ojJABUDgqP

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 15815

Unqiue Words: 3205

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
None.

ComputerPapers:
Computing the Expected Execution Time of Probabilistic Workflow Nets. https://t.co/p89RQBZn7Z

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 15074

Unqiue Words: 2550

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
None.

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

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 7371

Unqiue Words: 1370

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
None.

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

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 13202

Unqiue Words: 2346

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
None.

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

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 12138

Unqiue Words: 2850

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
None.

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

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 10089

Unqiue Words: 2294

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.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible