Copertina

Automated Verification of Silq Quantum Programs using SMT Solvers

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Lewis, Marco, Zuliani, Paolo, Soudjani, Sadegh
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Quantum Physics Logic in Computer Science Software Engineering
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Formal Verification of Quantum Programs: Theory, Tools and Challenges
di: Lewis, Marco, et al.
Pubblicazione: (2021)

Verification of Quantum Circuits through Discrete-Time Barrier Certificates
di: Lewis, Marco, et al.
Pubblicazione: (2024)

Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach
di: Hu, Siwei, et al.
Pubblicazione: (2025)

High-level quantum algorithm programming using Silq
di: Bezganovic, Viktorija, et al.
Pubblicazione: (2024)

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

Traq: Estimating the Quantum Cost of Classical Programs
di: Peduri, Anurudh, et al.
Pubblicazione: (2025)

Portus: Linking Alloy with SMT-based Finite Model Finding
di: Dancy, Ryan, et al.
Pubblicazione: (2024)

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

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

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

QbC: Quantum Correctness by Construction
di: Peduri, Anurudh, et al.
Pubblicazione: (2023)

Theta as a Horn Solver
di: Bajczi, Levente, et al.
Pubblicazione: (2025)

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

Finding Photonics Circuits via $δ$-weakening SMT
di: Lewis, Marco, et al.
Pubblicazione: (2025)

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis
di: Lu, Zhengyang, et al.
Pubblicazione: (2024)

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

Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP
di: Murugesan, Anitha, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

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)

PROMISE: Proof Automation as Structural Imitation of Human Reasoning
di: Ahn, Youngjoo, et al.
Pubblicazione: (2026)

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

Separation Logic for Verifying Physical Collisions of CNC Programs
di: Lee, Yeonseok
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)

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

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

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
di: Dobos-Kovács, Mihály, et al.
Pubblicazione: (2025)

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

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

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)

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

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

From Proof to Program: Characterizing Tool-Induced Reasoning Hallucinations in Large Language Models
di: Bayat, Farima Fatahi, et al.
Pubblicazione: (2025)