Copertina

Verifying Functional Correctness Properties At the Level of Java Bytecode

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Paganoni, Marco, Furia, Carlo A.
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Programming Languages Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Reasoning About Exceptional Behavior At the Level of Java Bytecode
di: Paganoni, Marco, et al.
Pubblicazione: (2024)

Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
di: Losavio, Lidia, et al.
Pubblicazione: (2025)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
di: Monniaux, David
Pubblicazione: (2024)

Verifying Floating-Point Programs in Stainless
di: Gilot, Andrea, et al.
Pubblicazione: (2026)

Verifying Lock-free Search Structure Templates
di: Patel, Nisarg, et al.
Pubblicazione: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
di: Murphy, Charlie, et al.
Pubblicazione: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
di: Bhat, Siddharth, et al.
Pubblicazione: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
di: Wang, Keyin, et al.
Pubblicazione: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
di: Gregersen, Simon Oddershede, et al.
Pubblicazione: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
di: Coglio, Alessandro, et al.
Pubblicazione: (2025)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
di: de Vilhena, Paulo Emílio, et al.
Pubblicazione: (2021)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
di: Grandury, Marcos, et al.
Pubblicazione: (2025)

Verified Purely Functional Catenable Real-Time Deques
di: Viennot, Jules, et al.
Pubblicazione: (2025)

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

Intrinsically Correct Algorithms and Recursive Coalgebras
di: Alexandru, Cass, et al.
Pubblicazione: (2025)

Kleene algebra with commutativity conditions is undecidable
di: de Amorim, Arthur Azevedo, et al.
Pubblicazione: (2024)

Internalizing Representation Independence with Univalence
di: Angiuli, Carlo, et al.
Pubblicazione: (2020)

Reasoning about Weak Isolation Levels in Separation Logic
di: Mathiasen, Anders Alnor, et al.
Pubblicazione: (2025)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
di: Lööw, Andreas, et al.
Pubblicazione: (2024)

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

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
di: Zilberstein, Noam, et al.
Pubblicazione: (2023)

Abstractions of Sequences, Functions and Operators
di: Rustenholz, Louis, et al.
Pubblicazione: (2025)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
di: Rowicki, Radosław Jan, et al.
Pubblicazione: (2025)

Verifying Asynchronous Hyperproperties in Reactive Systems
di: Beutner, Raven, et al.
Pubblicazione: (2025)

Extensional and Non-extensional Functions as Processes
di: Sakayori, Ken, et al.
Pubblicazione: (2024)

The Functional Machine Calculus III: Control
di: Heijltjes, Willem
Pubblicazione: (2025)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
di: Chatterjee, Krishnendu, et al.
Pubblicazione: (2024)

Functional Array Programming in an Extended Pi-Calculus
di: Hüttel, Hans, et al.
Pubblicazione: (2024)

A Probabilistic Choreography Language for PRISM
di: Carbone, Marco, et al.
Pubblicazione: (2025)

Higher Order Automatic Differentiation of Higher Order Functions
di: Huot, Mathieu, et al.
Pubblicazione: (2021)

Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
di: Zhu, Shaowei, et al.
Pubblicazione: (2024)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
di: Ileri, Atalay Mert, et al.
Pubblicazione: (2024)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
di: Klinkenberg, Lutz, et al.
Pubblicazione: (2023)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
di: Montesi, Fabrizio, et al.
Pubblicazione: (2026)

Domain Reasoning in TopKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2024)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
di: Matsuoka, Satoshi
Pubblicazione: (2026)

Towards a Higher-Order Bialgebraic Denotational Semantics
di: Goncharov, Sergey, et al.
Pubblicazione: (2026)

Verifying Tree-Manipulating Programs via CHCs
di: Faella, Marco, et al.
Pubblicazione: (2025)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2026)

Semantic Properties of Computations Defined by Elementary Inference Systems
di: Lucas, Salvador
Pubblicazione: (2025)