12 papers · 1 filter
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mecha…
To Zip Through the Cost Analysis of Probabilistic Programs
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While…
Deciding Boolean Separation Logic via Small Models (Technical Report)
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar +1
We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded…
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
Lucas Bueri, Radu Iosif, Florian Zuleger
A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound o…
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
Marius Bozga, Lucas Bueri, Radu Iosif +1
The treewidth boundedness problem for a logic asks for the existence of an upper bound on the treewidth of the models of a given formula in that logic. This problem is found to be…
Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems
Benjamin Aminof, Sasha Rubin, Francesco Spegni +1
We study the complexity of the model-checking problem for parameterized discrete-timed systems with arbitrarily many anonymous and identical processes, with and without a distingui…