Buchumschlag

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
1. Verfasser:	Monniaux, David
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Logic in Computer Science Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

A Formally Verified Procedure for Width Inference in FIRRTL
von: Wang, Keyin, et al.
Veröffentlicht: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
von: Coglio, Alessandro, et al.
Veröffentlicht: (2025)

Verifying Peephole Rewriting In SSA Compiler IRs
von: Bhat, Siddharth, et al.
Veröffentlicht: (2024)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
von: Ileri, Atalay Mert, et al.
Veröffentlicht: (2024)

Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
von: Agarwal, Shubham, et al.
Veröffentlicht: (2026)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
von: Thakur, Amitayush, et al.
Veröffentlicht: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
von: Li, Guchan, et al.
Veröffentlicht: (2026)

Verifying Floating-Point Programs in Stainless
von: Gilot, Andrea, et al.
Veröffentlicht: (2026)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
von: Lee, Jaeseo, et al.
Veröffentlicht: (2025)

Verifying Lock-free Search Structure Templates
von: Patel, Nisarg, et al.
Veröffentlicht: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
von: Murphy, Charlie, et al.
Veröffentlicht: (2024)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
von: Bryant, Randal E., et al.
Veröffentlicht: (2025)

Verifying Functional Correctness Properties At the Level of Java Bytecode
von: Paganoni, Marco, et al.
Veröffentlicht: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
von: Webb, Brae J., et al.
Veröffentlicht: (2021)

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

A Graded Modal Dependent Type Theory with Erasure, Formalized
von: Abel, Andreas, et al.
Veröffentlicht: (2026)

Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
von: Farjami, Ali, et al.
Veröffentlicht: (2026)

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

Verifying Asynchronous Hyperproperties in Reactive Systems
von: Beutner, Raven, et al.
Veröffentlicht: (2025)

Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems
von: Lang, Frédéric, et al.
Veröffentlicht: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
von: Ukhanov, Evgeny
Veröffentlicht: (2025)

Formally Verified Approximate Policy Iteration
von: Schäffeler, Maximilian, et al.
Veröffentlicht: (2024)

A Formally Verified Lightning Network
von: Fabiański, Grzegorz, et al.
Veröffentlicht: (2025)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
von: Kutsia, Temur, et al.
Veröffentlicht: (2024)

Formalization of Differential Privacy in Isabelle/HOL
von: Sato, Tetsuya, et al.
Veröffentlicht: (2024)

Formally Verified Certification of Unsolvability of Temporal Planning Problems
von: Wang, David, et al.
Veröffentlicht: (2025)

Verified VCG and Verified Compiler for Dafny
von: Nezamabadi, Daniel, et al.
Veröffentlicht: (2025)

Formally Verified Animation for RoboChart using Interaction Trees
von: Ye, Kangfeng, et al.
Veröffentlicht: (2023)

Four Formal Models of IEEE 1394 Link Layer
von: Garavel, Hubert, et al.
Veröffentlicht: (2024)

Verified Purely Functional Catenable Real-Time Deques
von: Viennot, Jules, et al.
Veröffentlicht: (2025)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
von: Kasibatla, Saketh Ram, et al.
Veröffentlicht: (2024)

Proceedings 9th edition of Working Formal Methods Symposium
von: Arusoaie, Andrei, et al.
Veröffentlicht: (2025)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
von: Hansen, Zachary
Veröffentlicht: (2025)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
von: Dvorak, Martin, et al.
Veröffentlicht: (2025)

Can Proof Assistants Verify Multi-Agent Systems?
von: Mendez, Julian Alfredo, et al.
Veröffentlicht: (2025)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
von: Yubeaton, Patrick, et al.
Veröffentlicht: (2025)

Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
von: Garavel, Hubert
Veröffentlicht: (2026)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
von: Rustenholz, Louis, et al.
Veröffentlicht: (2024)

Customizing Static Analysis using Codesearch
von: Hayoun, Avi, et al.
Veröffentlicht: (2024)