5 papers
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…
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 Monoidal View on Fixpoint Checks
Paolo Baldan, Richard Eggert, Barbara König +2
Fixpoints are ubiquitous in computer science as they play a central role in providing a meaning to recursive and cyclic definitions. Bisimilarity, behavioural metrics, termination…
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…
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…