Imagen de Portada

Model Checking as Program Verification by Abstract Interpretation (Extended Version)

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Baldan, Paolo, Bruni, Roberto, Ranzato, Francesco, Rigo, Diletta
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

A Program Logic for Abstract (Hyper)Properties
por: Baldan, Paolo, et al.
Publicado: (2026)

A Monoidal View on Fixpoint Checks
por: Baldan, Paolo, et al.
Publicado: (2023)

Practical Deductive Verification of OCaml Programs (Extended Version)
por: Pereira, Mário
Publicado: (2024)

Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
por: Soares, Tiago Lopes, et al.
Publicado: (2024)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
por: Gerlach, Lina, et al.
Publicado: (2025)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
por: Cheng, Ruotong, et al.
Publicado: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
por: Tsukada, Takeshi, et al.
Publicado: (2025)

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
por: Acclavio, Matteo, et al.
Publicado: (2026)

An Abstract Domain for Heap Commutativity (Extended Version)
por: Pincus, Jared, et al.
Publicado: (2024)

VerifyThis 2019: A Program Verification Competition (Extended Report)
por: Dross, Claire, et al.
Publicado: (2020)

Coalgebraic Behavioral Metrics
por: Baldan, Paolo, et al.
Publicado: (2017)

Fixpoint Theory -- Upside Down
por: Baldan, Paolo, et al.
Publicado: (2021)

Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
por: Kettmann, Pascal, et al.
Publicado: (2026)

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
por: Gheorghiu, Alexander V., et al.
Publicado: (2023)

A set-theoretical approach for ABox reasoning services (Extended Version)
por: Cantone, Domenico, et al.
Publicado: (2017)

Automata-less Monitoring via Trace-Checking (Extended Version)
por: Brunello, Andrea, et al.
Publicado: (2025)

Left-Linear Rewriting in Adhesive Categories
por: Baldan, Paolo, et al.
Publicado: (2024)

Monadic Intersection Types, Relationally (Extended Version)
por: Gavazzo, Francesco, et al.
Publicado: (2024)

Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics (Extended Version)
por: Kettmann, Pascal, et al.
Publicado: (2025)

A Fully Abstract Model of PCF Based on Extended Addressing Machines
por: Intrigila, Benedetto, et al.
Publicado: (2023)

Partially Finite Model Reasoning in Description Logics Extended Version
por: Gogacz, Tomasz, et al.
Publicado: (2026)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
por: Haselwarter, Philipp G., et al.
Publicado: (2026)

Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
por: Baldan, Paolo, et al.
Publicado: (2026)

A C++ reasoner for the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
por: Cantone, Domenico, et al.
Publicado: (2017)

Systematic Design of Separation Logics
por: Bruni, Roberto, et al.
Publicado: (2026)

A set-based reasoner for the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
por: Cantone, Domenico, et al.
Publicado: (2018)

Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version
por: Bezhanishvili, Nick, et al.
Publicado: (2024)

On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
por: Abdulla, Parosh Aziz, et al.
Publicado: (2026)

Formal Verification of Quantum Programs: Theory, Tools and Challenges
por: Lewis, Marco, et al.
Publicado: (2021)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
por: Li, Kwing Hei, et al.
Publicado: (2025)

Splitting Answer Set Programs with respect to Intensionality Statements (Extended Version)
por: Fandinno, Jorge, et al.
Publicado: (2025)

Complexity of the Model Checking problem for inquisitive propositional and modal logic
por: Grilletti, Gianluca, et al.
Publicado: (2024)

A General Automata Model for First-Order Temporal Logics (Extended Version)
por: Geatti, Luca, et al.
Publicado: (2024)

An optimized KE-tableau-based system for reasoning in the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
por: Cantone, Domenico, et al.
Publicado: (2018)

Craig Interpolation in Program Verification
por: Rümmer, Philipp
Publicado: (2026)

Sharing and Linear Logic with Restricted Access (Extended Version)
por: Barenbaum, Pablo, et al.
Publicado: (2025)

First-Order LTLf Synthesis with Lookback (Extended Version)
por: Winkler, Sarah
Publicado: (2025)

Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
por: Acclavio, Matteo, et al.
Publicado: (2025)

A Hyperlogic for Strategies in Stochastic Games (Extended Version)
por: Gerlach, Lina, et al.
Publicado: (2025)

Towards Proving Liveness on Weak Memory (Extended Version)
por: Bargmann, Lara, et al.
Publicado: (2026)