相关论文: Differential Hoare Logics and Refinement Calculi f…

We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…

Kleene algebra with tests (KAT) is an equational system for program verification, which is the combination of Boolean algebra (BA) and Kleene algebra (KA), the algebra of regular expressions. In particular, KAT subsumes the propositional…

We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with…

We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…

Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by…

Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and computations to be related facilitates use of simpler relational…

An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…

In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correctness of intermediate states of the program must be…

We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…

We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a…

This paper presents differential-algebraic refinement logic (dARL) with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) that extend hybrid dynamical systems with…

Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for…

We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof…

We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution…

We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers \`a la Dijkstra and through the lens of Kleene algebra with top…

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various…

Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct…

The Isabelle/HOL proof assistant has a powerful library for continuous analysis, which provides the foundation for verification of hybrid systems. However, Isabelle lacks automated proof support for continuous artifacts, which means that…

Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular…

This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid…