Cover Image

Minuska: Towards a Formally Verified Programming Language Framework

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Tušil, Jan, Obdržálek, Jan
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

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