Imagen de Portada

Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Kaufmann, Matt, Moore, J Strother
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science Mathematical Software
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling
por: Altuntas, Alper, et al.
Publicado: (2025)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
por: Munive, Jonathan Julián Huerta y, et al.
Publicado: (2024)

Extended Abstract: Mutable Objects with Several Implementations
por: Kaufmann, Matt, et al.
Publicado: (2025)

LeanBET: Formally-verified surface area calculations in Lean
por: Ugwuanyi, Ejike D., et al.
Publicado: (2026)

A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics
por: Fages, François
Publicado: (2024)

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

Satisfiability.jl: Satisfiability Modulo Theories in Julia
por: Soroka, Emiko, et al.
Publicado: (2023)

Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
por: Zhang, Junchao
Publicado: (2025)

Proceedings 14th International Conference on Automated Deduction in Geometry
por: Quaresma, Pedro, et al.
Publicado: (2024)

Compositionality of Systems and Partially Ordered Runs
por: Fettke, Peter, et al.
Publicado: (2026)

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

FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller
por: Farrell, Marie, et al.
Publicado: (2021)

TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System
por: Dai, Steve, et al.
Publicado: (2025)

ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
por: Dantas, Pierre, et al.
Publicado: (2026)

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

Foundations for an Abstract Proof Theory in the Context of Horn Rules
por: Lyon, Tim S., et al.
Publicado: (2023)

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
por: Gheorghiu, Alexander V., et al.
Publicado: (2023)

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

Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
por: Li, Letitia W., et al.
Publicado: (2026)

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
por: Hassnain, Muhammad, et al.
Publicado: (2025)

Relevant HAL Interface Requirements for Embedded Systems
por: Bentele, Manuel, et al.
Publicado: (2025)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
por: Bryant, Dustin, et al.
Publicado: (2025)

Approximate Optimal Active Learning of Decision Trees
por: Huang, Zunchen, et al.
Publicado: (2025)

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

Autonomous Task Completion Based on Goal-directed Answer Set Programming
por: Tudor, Alexis R.
Publicado: (2025)

Preguss: It Analyzes, It Specifies, It Verifies
por: Wang, Zhongyi, et al.
Publicado: (2025)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
por: Wojtak, Connor, et al.
Publicado: (2025)

Theta as a Horn Solver
por: Bajczi, Levente, et al.
Publicado: (2025)

Checking the HAL Interface Specification Continuously, Right from the Start
por: Bentele, Manuel, et al.
Publicado: (2025)

Early Validation of High-level Requirements on Cyber-Physical Systems
por: Vašíček, Ondřej
Publicado: (2025)

Smart Contracts Formal Verification: A Systematic Literature Review
por: Davila, Rene, et al.
Publicado: (2025)

Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
por: Lopez-Miguel, Ignacio D., et al.
Publicado: (2025)

A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
por: Wang, Zhongyi, et al.
Publicado: (2025)

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
por: Cristiá, Maximiliano, et al.
Publicado: (2021)

Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs
por: Brancas, Ricardo, et al.
Publicado: (2024)

Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems
por: ter Beek, Maurice H., et al.
Publicado: (2026)

Circular Induction
por: Lucanu, Dorel, et al.
Publicado: (2026)

Inferring Message Flows From System Communication Traces
por: Nadimi, Bardia, et al.
Publicado: (2024)

Equational Anti-Unification over Absorption Theories
por: Ayala-Rincon, Mauricio, et al.
Publicado: (2023)

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