Copertina

Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autore principale:	Zhang, Yuanrui
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Logic in Computer Science Software Engineering
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

On A Parameterized Theory of Dynamic Logic for Operationally-based Programs
di: Zhang, Yuanrui
Pubblicazione: (2026)

Separation Logic for Verifying Physical Collisions of CNC Programs
di: Lee, Yeonseok
Pubblicazione: (2026)

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

Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
di: Lee, Yeonseok
Pubblicazione: (2026)

Bounds for Quantum Circuits using Logic-Based Analysis
di: Fauseweh, Benedikt, et al.
Pubblicazione: (2024)

A Logic for Veracity
di: Reeves, Steve
Pubblicazione: (2023)

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

Declarative Scenario-based Testing with RoadLogic
di: Bartocci, Ezio, et al.
Pubblicazione: (2026)

Quantitative Monitoring of Signal First-Order Logic
di: Chalupa, Marek, et al.
Pubblicazione: (2026)

LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models
di: Wan, Yuxuan, et al.
Pubblicazione: (2024)

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

Tunable Automation in Automated Program Verification
di: Bai, Alexander Y., et al.
Pubblicazione: (2025)

Varanus: Runtime Verification for CSP
di: Luckcuck, Matt, et al.
Pubblicazione: (2025)

Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
di: Murphy, William, et al.
Pubblicazione: (2024)

Can Language Models Pretend Solvers? Logic Code Simulation with LLMs
di: Chen, Minyu, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
di: Kawamoto, Yusuke, et al.
Pubblicazione: (2024)

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

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
di: Somorjai, Márk, et al.
Pubblicazione: (2024)

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

Agentic Proving for Program Verification
di: Sosso, Alessandro, et al.
Pubblicazione: (2026)

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
di: Lanzinger, Florian, et al.
Pubblicazione: (2024)

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

Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming
di: Vašíček, Ondřej, et al.
Pubblicazione: (2024)

MacroSwarm: A Field-based Compositional Framework for Swarm Programming
di: Aguzzi, Gianluca, et al.
Pubblicazione: (2024)

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

AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
di: Tian, Enyuan, et al.
Pubblicazione: (2025)

Verifying DNN-based Semantic Communication Against Generative Adversarial Noise
di: Le, Thanh, et al.
Pubblicazione: (2026)

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

Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
di: Ferrando, Angelo
Pubblicazione: (2025)

Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)
di: Sigloch, Paul, et al.
Pubblicazione: (2026)

Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations
di: Zhang, Changjian, et al.
Pubblicazione: (2023)

Towards Automatic Transformations of Coq Proof Scripts
di: Magaud, Nicolas
Pubblicazione: (2024)

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

Programming Really Is Simple Mathematics
di: Meyer, Bertrand, et al.
Pubblicazione: (2025)