98 citations
- Universidad Politécnica de MadridES38 papers
- Madrid Institute for Advanced StudiesES15 papers
- Roskilde UniversityDK11 papers
- University of PennsylvaniaUS11 papers
- Max Planck Institute for Software SystemsDE10 papers
- University at Buffalo, State University of New YorkUS9 papers
- Institut national de recherche en sciences et technologies du numériqueFR8 papers
- Universidad Complutense de MadridES7 papers
- Consejo Superior de Investigaciones CientíficasES5 papers
- Saarland UniversityDE5 papers
- University College LondonGB5 papers
- Centre National de la Recherche ScientifiqueFR4 papers
6 papers · 2 filters
Solving non-linear Horn clauses using a linear Horn clause solver
Bishoksan Kafle, John P. Gallagher, Pierre Ganty
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn…
Coupling proofs are probabilistic product programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu +1
Couplings are a powerful mathematical tool for reasoning about pairs of probabilistic processes. Recent developments in formal verification identify a close connection between coup…
Synthesizing Probabilistic Invariants via Doob's Decomposition
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti +1
When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then…
Differentially Private Bayesian Programming
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi +4
We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich fun…
Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code
Guillermo Vigueras, Manuel Carro, Salvador Tamarit +1
The current trend in next-generation exascale systems goes towards integrating a wide range of specialized (co-)processors into traditional supercomputers. However, the integration…
Towards a Semantics-Aware Transformation Toolchain for Heterogeneous Systems
Salvador Tamarit, Julio Mariño, Guillermo Vigueras +1
Obtaining good performance when programming heterogeneous computing platforms poses significant challenges for the programmer. We present a program transformation environment, impl…