Copertina

Minuska: Towards a Formally Verified Programming Language Framework

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Tušil, Jan, Obdržálek, Jan
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
di: Parthasarathy, Gaurav, et al.
Pubblicazione: (2024)

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
di: Pedersen, Jan, et al.
Pubblicazione: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
di: Yang, Chengxi, et al.
Pubblicazione: (2025)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
di: Cao, Jialun, et al.
Pubblicazione: (2025)

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
di: Shen, Gan, et al.
Pubblicazione: (2024)

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

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
di: Tekriwal, Mohit, et al.
Pubblicazione: (2025)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
di: Dane, Serra Z., et al.
Pubblicazione: (2026)

Formally Verified Linear-Time Invertible Lexing
di: Chassot, Samuel, et al.
Pubblicazione: (2025)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
di: Dardinier, Thibault, et al.
Pubblicazione: (2024)

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

Linguine: A Natural-Language Programming Language with Formal Semantics and a Clean Compiler Pipeline
di: Hu, Lifan
Pubblicazione: (2025)

Proceedings 16th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
di: Derakhshan, Farzaneh, et al.
Pubblicazione: (2025)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
di: Wu, Jinhua, et al.
Pubblicazione: (2025)

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
di: Wang, Shuling, et al.
Pubblicazione: (2024)

Dependent Session Types for Verified Concurrent Programming
di: Fu, Qiancheng, et al.
Pubblicazione: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
di: Schröer, Philipp, et al.
Pubblicazione: (2026)

Don't Call Us, We'll Call You: Towards Mixed-Initiative Interactive Proof Assistants for Programming Language Theory
di: Verter, Jan Liam, et al.
Pubblicazione: (2024)

Practical Formal Verification for MLIR Programs
di: Tucker, Emily, et al.
Pubblicazione: (2026)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
di: Ravi, Nikil, et al.
Pubblicazione: (2026)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
di: Huyghebaert, Sander, et al.
Pubblicazione: (2023)

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)

Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages
di: Mora, Federico, et al.
Pubblicazione: (2024)

A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
di: Tobler, James, et al.
Pubblicazione: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
di: Baumann, Jonathan, et al.
Pubblicazione: (2026)

Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
di: Lundén, Daniel, et al.
Pubblicazione: (2023)

Qafny: A Quantum-Program Verifier
di: Li, Liyi, et al.
Pubblicazione: (2022)

From Algebraic Word Problem to Program: A Formalized Approach
di: Wiemerslage, Adam, et al.
Pubblicazione: (2020)

Crux, a Precise Verifier for Rust and Other Languages
di: Pernsteiner, Stuart, et al.
Pubblicazione: (2024)

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

Formal Simulation and Visualisation of Hybrid Programs
di: Mendes, Pedro, et al.
Pubblicazione: (2024)

An Intermediate Program Representation for Optimizing Stream-Based Languages
di: Baumeister, Jan, et al.
Pubblicazione: (2025)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
di: Bucev, Mario, et al.
Pubblicazione: (2024)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
di: Reitz, Antonin, et al.
Pubblicazione: (2024)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
di: Fedchin, Aleksandr, et al.
Pubblicazione: (2025)

LoRe: A Programming Model for Verifiably Safe Local-First Software
di: Haas, Julian, et al.
Pubblicazione: (2023)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
di: Foo, Darius, et al.
Pubblicazione: (2023)

A Natural Formalized Proof Language
di: Xie, Lihan, et al.
Pubblicazione: (2024)

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
di: Pezeshkpour, Pouya, et al.
Pubblicazione: (2026)