Cover Image

MoXIchecker: An Extensible Model Checker for MoXI

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ates, Salih, Beyer, Dirk, Chien, Po-Chun, Lee, Nian-Ze
Format:	Preprint
Published:	2024
Subjects:	Software Engineering Programming Languages D.2.4; F.3.1; D.3.1; F.4.3
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
by: Beyer, Dirk, et al.
Published: (2022)

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
by: Amusuo, Paschal C., et al.
Published: (2025)

QuickCheck for VDM
by: Battle, Nick, et al.
Published: (2024)

A Unit Proofing Framework for Code-level Verification: A Research Agenda
by: Amusuo, Paschal C., et al.
Published: (2024)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Mechanizing Operads with Event-B
by: Attiogbé, Christian
Published: (2025)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
by: Ye, Kangfeng, et al.
Published: (2024)

The concept of class invariant in object-oriented programming
by: Meyer, Bertrand, et al.
Published: (2021)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
by: Suwa, Takashi, et al.
Published: (2026)

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
by: Parrinha, Francisco, et al.
Published: (2026)

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
by: Amusuo, Paschal C., et al.
Published: (2026)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
by: Gross, Jason, et al.
Published: (2022)

Constrained LTL Specification Learning from Examples
by: Zhang, Changjian, et al.
Published: (2024)

Weak-linearity, globality and in-place update
by: Gramaglia, Hector
Published: (2024)

A Graded Modal Type Theory for Pulse Schedules
by: Adams, Robin, et al.
Published: (2025)

Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
by: McCann, Alan L.
Published: (2026)

Cryptographic Registry Provenance: Structural Defense Against Dependency Confusion in AI Package Ecosystems
by: McCann, Alan L.
Published: (2026)

Quantifying Confidence in Assurance 2.0 Arguments
by: Bloomfield, Robin, et al.
Published: (2026)

Bottom-up computation using trees of sublists (Functional Pearl)
by: Mu, Shin-Cheng
Published: (2023)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
by: Guan, Yawen, et al.
Published: (2025)

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

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
by: Prebet, Enguerrand, et al.
Published: (2026)

Uniform Substitution for Differential Refinement Logic
by: Prebet, Enguerrand, et al.
Published: (2024)

The pitfalls of verifying floating-point computations
by: Monniaux, David
Published: (2007)

Complementing an imperative process algebra with a rely/guarantee logic
by: Middelburg, C. A.
Published: (2025)

Probabilistic imperative process algebra
by: Middelburg, C. A.
Published: (2026)

Towards Automatic Error Recovery in Parsing Expression
by: de Medeiros, Sérgio Queiroz, et al.
Published: (2025)

On the Soundness and Consistency of LLM Agents for Executing Test Cases Written in Natural Language
by: Salva, Sébastien, et al.
Published: (2025)

Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
by: Beg, Arshad, et al.
Published: (2026)

Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
by: Beg, Arshad, et al.
Published: (2025)

A Short Survey on Formalising Software Requirements using Large Language Models
by: Beg, Arshad, et al.
Published: (2025)

Exploring Large Language Models for Access Control Policy Synthesis and Summarization
by: Vatsa, Adarsh, et al.
Published: (2025)

FalseCrashReducer: Mitigating False Positive Crashes in OSS-Fuzz-Gen Using Agentic AI
by: Amusuo, Paschal C., et al.
Published: (2025)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
by: Sextl, Florian, et al.
Published: (2023)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
by: Chiari, Michele, et al.
Published: (2024)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
by: Esen, Zafer, et al.
Published: (2025)

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