16 citations · 46 across the 17 of their papers we have counts for
21 papers
Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
Paolo Baldan, Sebastian Gurke, Barbara König +1
The problem of determining the (least) fixpoint of (higher-dimensional) functions over the non-negative reals frequently occurs when dealing with systems endowed with a quantitativ…
A Program Logic for Abstract (Hyper)Properties
Paolo Baldan, Roberto Bruni, Francesco Ranzato +1
We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic…
Model Checking as Program Verification by Abstract Interpretation (Extended Version)
Paolo Baldan, Roberto Bruni, Francesco Ranzato +1
Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions…
Approximating Fixpoints of Approximated Functions
Paolo Baldan, Sebastian Gurke, Barbara König +2
Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one often considers least fixpoints of (higher-dimensional) functions ove…
Validity of contextual formulas (extended version)
Javier Esparza, Rubén Rubio
Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion $c[p] \equiv (p \wedge c[\math…
Left-Linear Rewriting in Adhesive Categories
Paolo Baldan, Davide Castelnovo, Andrea Corradini +1
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since indepe…