Copertina

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Beyer, Dirk, Lee, Nian-Ze, Wendler, Philipp
Natura:	Preprint
Pubblicazione:	2022
Soggetti:	Software Engineering Programming Languages D.2.4; F.3.1
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

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

MoXIchecker: An Extensible Model Checker for MoXI
di: Ates, Salih, et al.
Pubblicazione: (2024)

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

QuickCheck for VDM
di: Battle, Nick, et al.
Pubblicazione: (2024)

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

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

Formal Verification of Imperative First-Class Functions in Move
di: Grieskamp, Wolfgang, et al.
Pubblicazione: (2026)

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

Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
di: Lahiri, Shuvendu K.
Pubblicazione: (2026)

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

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

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

Model Checking Probabilistic Operator Precedence Automata
di: Pontiggia, Francesco, et al.
Pubblicazione: (2024)

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

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

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

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

A New Interaction Concept for Interactive and Autoactive Program Verification
di: Pfeifer, Wolfram, et al.
Pubblicazione: (2026)

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

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

On the Decidability of Verification under Release/Acquire
di: Conrado, Giovanna Kobus, et al.
Pubblicazione: (2026)

Verifying Correctness of PLC Software during System Evolution using Model Containment Approach
di: Bandyopadhyay, Soumyadip, et al.
Pubblicazione: (2025)

Weak-linearity, globality and in-place update
di: Gramaglia, Hector
Pubblicazione: (2024)

Contract-based Verification of Digital Twins
di: Naeem, Muhammad, et al.
Pubblicazione: (2025)

Array-Carrying Symbolic Execution for Function Contract Generation
di: Lu, Weijie, et al.
Pubblicazione: (2026)

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

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

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

Quantitative Verification with Neural Networks
di: Abate, Alessandro, et al.
Pubblicazione: (2023)

Seamless, Correct, and Generic Programming over Serialised Data
di: Allais, Guillaume
Pubblicazione: (2023)

From Separate Compilation to Sound Language Composition
di: Bruzzone, Federico, et al.
Pubblicazione: (2026)

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
di: Lin, Hongyu, et al.
Pubblicazione: (2026)

Ownership in low-level intermediate representation
di: Priya, Siddharth, et al.
Pubblicazione: (2024)

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

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
di: Frenkel, Eden, et al.
Pubblicazione: (2026)

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

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

The pitfalls of verifying floating-point computations
di: Monniaux, David
Pubblicazione: (2007)

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

Generative transformations and patterns in LLM-native approaches for software verification and falsification
di: Braberman, Víctor A., et al.
Pubblicazione: (2024)