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
44 papers · 1 filter
An Approach to the Abstract Interpretation of Goal-Directed Answer Set Programming
Daniel Jurjo-Rivas, Joaquín Arias, Gopal Gupta +3
Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling t…
Basic Model Theory for Path Predicate Modal Logic
Raul Fervari, Santiago Figueira, Gabriel Goren-Roig +1
Path Predicate Modal Logic (PPML) is a generalization of Basic Modal Logic, where atoms are relational predicates instead of propositional symbols. The study of PPML is motivated a…
Supermartingale Certificates for Quantitative Omega-regular Verification and Control
Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi +1
We present the first supermartingale certificate for quantitative -regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the produ…
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can…
Integer Linear-Exponential Programming in NP by Quantifier Elimination
Dmitry Chistikov, Alessio Mansutti, Mikhail R. Starchak
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer line…
On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
Christoph Haase, Alessio Mansutti, Amaury Pouly
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that…