Imagen de Portada

Tunable Automation in Automated Program Verification

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Bai, Alexander Y., Hawblitzel, Chris, Lattuada, Andrea
Formato:	Preprint
Publicado:	2025
Materias:	Software Engineering Logic in Computer Science Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Agentic Proving for Program Verification
por: Sosso, Alessandro, et al.
Publicado: (2026)

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
por: De Angelis, Emanuele, et al.
Publicado: (2025)

Programming Really Is Simple Mathematics
por: Meyer, Bertrand, et al.
Publicado: (2025)

Flexible Correct-by-Construction Programming
por: Runge, Tobias, et al.
Publicado: (2022)

Verification Modulo Tested Library Contracts
por: Uppar, Abhishek, et al.
Publicado: (2026)

Formalizing UML State Machines for Automated Verification -- A Survey
por: André, Étienne, et al.
Publicado: (2024)

Automated Verification of Silq Quantum Programs using SMT Solvers
por: Lewis, Marco, et al.
Publicado: (2024)

Dafny as Verification-Aware Intermediate Language for Code Generation
por: Li, Yue Chen, et al.
Publicado: (2025)

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

AutoDeduct: A Tool for Automated Deductive Verification of C Code
por: Amilon, Jesper, et al.
Publicado: (2025)

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
por: Barth, Max, et al.
Publicado: (2025)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
por: Dobos-Kovács, Mihály, et al.
Publicado: (2025)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
por: Deng, Haotian, et al.
Publicado: (2025)

Establishing tool support for a concept DSL
por: Jakobsen, Nikolaj Kühne
Publicado: (2025)

An Enumerative Embedding of the Python Type System in ACL2s
por: Xifaras, Samuel, et al.
Publicado: (2025)

GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
por: Chakraborty, Soham, et al.
Publicado: (2025)

GNU Aris: a web application for students
por: Attri, Saksham, et al.
Publicado: (2025)

Proceedings 9th edition of Working Formal Methods Symposium
por: Arusoaie, Andrei, et al.
Publicado: (2025)

Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
por: Garavel, Hubert
Publicado: (2026)

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

Customizing Static Analysis using Codesearch
por: Hayoun, Avi, et al.
Publicado: (2024)

Contract Usage and Evolution in Android Mobile Applications
por: Ferreira, David R., et al.
Publicado: (2024)

Context-Sensitive Abstract Interpretation of Dynamic Languages
por: Piszcz, Franciszek
Publicado: (2024)

Leveraging Large Language Models to Boost Dafny's Developers Productivity
por: Silva, Álvaro, et al.
Publicado: (2024)

Traq: Estimating the Quantum Cost of Classical Programs
por: Peduri, Anurudh, et al.
Publicado: (2025)

Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
por: Ganguly, Debargha, et al.
Publicado: (2025)

PROMISE: Proof Automation as Structural Imitation of Human Reasoning
por: Ahn, Youngjoo, et al.
Publicado: (2026)

From Proof to Program: Characterizing Tool-Induced Reasoning Hallucinations in Large Language Models
por: Bayat, Farima Fatahi, et al.
Publicado: (2025)

Inferring multiple helper Dafny assertions with LLMs
por: Silva, Álvaro, et al.
Publicado: (2025)

Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
por: Fan, Wen, et al.
Publicado: (2024)

QbC: Quantum Correctness by Construction
por: Peduri, Anurudh, et al.
Publicado: (2023)

Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
por: Zhang, Yuanrui
Publicado: (2024)

Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP
por: Murugesan, Anitha, et al.
Publicado: (2024)

VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
por: Brandfonbrener, David, et al.
Publicado: (2024)

Automated Software Verification of Hyperliveness
por: Beutner, Raven
Publicado: (2024)

Automated Test Data Generation for Enterprise Protobuf Systems: A Metaclass-Enhanced Statistical Approach
por: Du, Y.
Publicado: (2025)

Proceedings of the Fourteenth and Fifteenth International Workshop on Graph Computation Models
por: Endrullis, Jörg, et al.
Publicado: (2025)

Enhanced Data Race Prediction Through Modular Reasoning
por: Ang, Zhendong, et al.
Publicado: (2025)

Proceedings 16th International Workshop on Graph Computation Models
por: Lambers, Leen, et al.
Publicado: (2026)

Varanus: Runtime Verification for CSP
por: Luckcuck, Matt, et al.
Publicado: (2025)