ABSTRACT. This paper presents \emph{differential-algebraic logic} (\dAL), an axiomatic framework for the deductive verification of \emph{differential-algebraic programs} (DAPs), which extend hybrid dynamical systems with differential-algebraic equations (DAEs). In particular, this paper develops a refinement calculus that allows for the sound comparison between trajectories of differential-algebraic equations, crucially utilizing a novel trace-based semantics. Such a refinement calculus then allows for the incremental verification/simplification of complicated DAEs, while ensuring correctness at each step by the soundness of the axiomatization. In addition, this paper presents an application of the axiomatization by establishing its completeness in certifying index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.

ABSTRACT. Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need of repeatedly rechecking their safety in full after every change. We present a method for proving that system refactorings preserve their required properties by transferring the proof along the modification. It is based on differential refinement logic (dRL), with which one can simultaneously and rigorously refer to properties of the systems and the relation between a refactored system with its original version. Refinements represent a uniform way of expressing different types of hybrid system refactorings, including those that introduce auxiliary variables. Furthermore, we show how these refactorings can be proved automatically, and/or reduce to a modular proof solely about the local change rather than about the whole system.

ABSTRACT. This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. By small, natural, and practically meaningful syntactic restrictions, specifications are ensured (by construction) to be topologically open and, thus, robust with respect to infinitesimal perturbations without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. The proof is constructive, self-contained, and demonstrates how robustly-correct hybrid systems reachability specifications can be automatically verified through proof.

ABSTRACT. We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable for automated reasoning. Using the new notion of inductive lvalues, our technique can handle loops where previous techniques fail, and it unifies acceleration for arrays and scalar variables by regarding scalars as arrays of dimension 0. Moreover, our approach uses λs instead of quantifiers. Then the resulting SMT problems can be solved via lemmas on demand. An empirical evaluation of our implementation in the tool LoAT shows the power of our approach.

ABSTRACT. The fluted fragment lacks the Craig Interpolation Property. In this paper we establish a weakened form of interpolation. Given an entailment in the fluted fragment, we distinguish predicates that only take an argument sequence starting with $x_1$ from those that do not. A predicate of the former kind is allowed to appear in a weak interpolant only if it occurs in both the premise and the conclusion; and any predicate of the latter kind can be used in a weak interpolant no matter whether it is in the shared signature. Our proof also shows that the weakened interpolation holds in every finite variable subfragment of the fluted fragment. In addition, this work provides a generalization of A. Herzig's translation of the ordered fragment, as well as a new proof of the finite model property of the fluted fragment.