Image de couverture de livre

An ACL2s Interface to Z3

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Walter, Andrew T., Manolios, Panagiotis
Format:	Preprint
Publié:	2025
Sujets:	Logic in Computer Science D.2.4
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Parf: Adaptive Parameter Refining for Abstract Interpretation
par: Wang, Zhongyi, et autres
Publié: (2024)

Reachability and Safety Games under TSO Semantics
par: Spengler, Stephan
Publié: (2024)

On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
par: Abdulla, Parosh Aziz, et autres
Publié: (2026)

Why does it fail? Explanation of verification failures
par: Eriksson, Lars-Henrik
Publié: (2026)

Verification Challenge: Fractional Cascading for Multi-Nuclide Grid Lookup
par: Siegel, Andrew R.
Publié: (2025)

A Graphical Interface for Category Theory Proofs in Coq
par: Chabassier, Luc
Publié: (2025)

Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection
par: Mustafa, Daham, et autres
Publié: (2026)

Satisfiability.jl: Satisfiability Modulo Theories in Julia
par: Soroka, Emiko, et autres
Publié: (2023)

Verifying Procedural Programs via Constrained Rewriting Induction
par: Fuhs, Carsten, et autres
Publié: (2014)

Type Inference for Isabelle2Cpp
par: Jiang, Dongchen, et autres
Publié: (2024)

Reachability and Safety Games under TSO Semantics (Extended Version)
par: Spengler, Stephan
Publié: (2024)

Path-optimal symbolic execution of heap-manipulating programs
par: Braione, Pietro, et autres
Publié: (2024)

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment
par: Jilissen, Kevin H. J., et autres
Publié: (2024)

Axis-Aligned Semantics for ODRL: Resolving Dimensional Ambiguity in Policy Constraints
par: Mustafa, Daham, et autres
Publié: (2026)

Verification of E-Voting Algorithms in Dafny
par: Büttner, Robert, et autres
Publié: (2025)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
par: Esen, Zafer, et autres
Publié: (2025)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
par: Sextl, Florian, et autres
Publié: (2023)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
par: Chiari, Michele, et autres
Publié: (2024)

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

Automatic Function Annotations for Hoare Logic
par: Matichuk, Danielle
Publié: (2012)

A Note on the Parameterised Complexity of Coverability in Vector Addition Systems
par: Pilipczuk, Michał, et autres
Publié: (2025)

Space-time process algebra with asynchronous communication
par: Bergstra, J. A., et autres
Publié: (2024)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
par: Stepanenko, Sergei, et autres
Publié: (2025)

Uniqueness is Separation
par: O'Connor, Liam, et autres
Publié: (2026)

An Enumerative Embedding of the Python Type System in ACL2s
par: Xifaras, Samuel, et autres
Publié: (2025)

Ground Stratification for a Logic of Definitions with Induction
par: Guermond, Nathan, et autres
Publié: (2025)

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
par: Knothe, David, et autres
Publié: (2026)

Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
par: Gamboa, Ruben, et autres
Publié: (2025)

Provably Correct Systems: Community, connections, and citations
par: Bowen, Jonathan P.
Publié: (2015)

Baking for Dafny: A CakeML Backend for Dafny
par: Nezamabadi, Daniel, et autres
Publié: (2025)

Leveraging Slither and Interval Analysis to build a Static Analysis Tool
par: Susan, Stefan-Claudiu
Publié: (2024)

Scott's Representation Theorem and the Univalent Karoubi Envelope
par: van der Leer, Arnoud, et autres
Publié: (2025)

Quantifying Confidence in Assurance 2.0 Arguments
par: Bloomfield, Robin, et autres
Publié: (2026)

Modal Verification Patterns for Systems Software
par: Kuru, Ismail, et autres
Publié: (2025)

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

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
par: Prebet, Enguerrand, et autres
Publié: (2026)

Towards Weak Stratification for Logics of Definitions
par: Guermond, Nathan
Publié: (2026)

Uniform Substitution for Differential Refinement Logic
par: Prebet, Enguerrand, et autres
Publié: (2024)

VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI
par: Hovland, Paul D.
Publié: (2025)

Automated Consistency Analysis for Legal Contracts
par: Khoja, Alan, et autres
Publié: (2025)