ABSTRACT
No abstract available.
Recommendations
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with ...
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata
Proceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 10206Ultimate Automizer is a software verifier that implements an automata-based approach for the verification of safety and liveness properties. A central new feature that speeded up the abstraction refinement of the tool is an on-demand construction of ...
Floyd--hoare logic for quantum programs
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build ...
Comments