Copertina

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Gross, Jason, Erbsen, Andres, Philipoom, Jade, Agrawal, Rajashree, Chlipala, Adam
Natura:	Preprint
Pubblicazione:	2022
Soggetti:	Programming Languages F.3.1; D.2.4; F.4.2; D.3.4
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Verified VCG and Verified Compiler for Dafny
di: Nezamabadi, Daniel, et al.
Pubblicazione: (2025)

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
di: Knothe, David, et al.
Pubblicazione: (2026)

TensorRight: Automated Verification of Tensor Graph Rewrites
di: Arora, Jai, et al.
Pubblicazione: (2025)

LR Parsing of Permutation Phrases
di: Kostičová, Jana
Pubblicazione: (2024)

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment
di: Jilissen, Kevin H. J., et al.
Pubblicazione: (2024)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
di: Suwa, Takashi, et al.
Pubblicazione: (2026)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
di: Accattoli, Beniamino, et al.
Pubblicazione: (2025)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
di: Baier, Daniel, et al.
Pubblicazione: (2024)

MoXIchecker: An Extensible Model Checker for MoXI
di: Ates, Salih, et al.
Pubblicazione: (2024)

CBCL: Safe Self-Extending Agent Communication
di: O'Connor, Hugo
Pubblicazione: (2026)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
di: Sextl, Florian, et al.
Pubblicazione: (2023)

Space-time process algebra with asynchronous communication
di: Bergstra, J. A., et al.
Pubblicazione: (2024)

Weak-linearity, globality and in-place update
di: Gramaglia, Hector
Pubblicazione: (2024)

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis
di: Waldinger, Richard
Pubblicazione: (2025)

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
di: Prebet, Enguerrand, et al.
Pubblicazione: (2026)

Uniform Substitution for Differential Refinement Logic
di: Prebet, Enguerrand, et al.
Pubblicazione: (2024)

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
di: Amusuo, Paschal C., et al.
Pubblicazione: (2025)

QuickCheck for VDM
di: Battle, Nick, et al.
Pubblicazione: (2024)

Bottom-up computation using trees of sublists (Functional Pearl)
di: Mu, Shin-Cheng
Pubblicazione: (2023)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
di: Guan, Yawen, et al.
Pubblicazione: (2025)

A Unit Proofing Framework for Code-level Verification: A Research Agenda
di: Amusuo, Paschal C., et al.
Pubblicazione: (2024)

Mechanizing Operads with Event-B
di: Attiogbé, Christian
Pubblicazione: (2025)

Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
di: McCann, Alan L.
Pubblicazione: (2026)

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
di: Parrinha, Francisco, et al.
Pubblicazione: (2026)

Verifying Device Drivers with Pancake
di: Zhao, Junming, et al.
Pubblicazione: (2025)

Baking for Dafny: A CakeML Backend for Dafny
di: Nezamabadi, Daniel, et al.
Pubblicazione: (2025)

Prioritizing Configuration Relevance via Compiler-Based Refined Feature Ranking
di: Bruzzone, Federico, et al.
Pubblicazione: (2026)

NeuroLog: Reasoning You Can Audit -- Neuro-Symbolic Vulnerability Discovery via LLM Facts, Datalog, and SMT
di: Rawat, Sanjay
Pubblicazione: (2026)

Complementing an imperative process algebra with a rely/guarantee logic
di: Middelburg, C. A.
Pubblicazione: (2025)

Probabilistic imperative process algebra
di: Middelburg, C. A.
Pubblicazione: (2026)

Verification of E-Voting Algorithms in Dafny
di: Büttner, Robert, et al.
Pubblicazione: (2025)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
di: Chiari, Michele, et al.
Pubblicazione: (2024)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
di: Esen, Zafer, et al.
Pubblicazione: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
di: Reinhard, Tobias
Pubblicazione: (2024)

Automatic Function Annotations for Hoare Logic
di: Matichuk, Danielle
Pubblicazione: (2012)

FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
di: Zhang, Xindi, et al.
Pubblicazione: (2025)

DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
di: Cheval, Vincent, et al.
Pubblicazione: (2022)

Automatic verification of Finite Variant Property beyond convergent equational theories
di: Cheval, Vincent, et al.
Pubblicazione: (2024)

Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
di: Beg, Arshad, et al.
Pubblicazione: (2026)

Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
di: Beg, Arshad, et al.
Pubblicazione: (2025)