View: session overviewtalk overview

10:30 | Abstract Execution PRESENTER: Dominic Steinhöfel ABSTRACT. We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. For each abstract symbol, we faithfully represent each possible concrete execution resulting from its substitution with concrete code. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight well-known statement-level refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semantics-preserving. Most preconditions are not mentioned in the literature. |

11:00 | Static Analysis for Detecting High-Level Races in RTOS Kernels ABSTRACT. We propose a static analysis based approach for detecting high-level races in RTOS kernels popularly used in safety-critical embedded software. High-Level races are indicators of atomicity violations and can lead to erroneous software behaviour with serious consequences. Hitherto techniques for detecting high-level races have relied on model-checking approaches, which are inefficient and apriori unsound. In contrast we propose a technique based on static analysis that is both efficient and sound. The technique is based on the notion of disjoint blocks recently introduced in Chopra et al [8]. We evaluate our technique on three popular RTOS kernels and show that it is effective in detecting races, many of them harmful, with a high rate of precision. |

11:30 | Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic ABSTRACT. Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly model such systems and to ensure they function correctly according to safety requirements. Differential dynamic logic is a powerful logic to model hybrid systems and to prove their correctness. We contribute a component-based modeling and reasoning framework to differential dynamic logic that separates models into components with timing guarantees, such as reactivity of controllers and controllability of continuous dynamics. Components operate in parallel, with coarse-grained interleaving, periodic execution and communication. We present techniques to automate system safety proofs from isolated, modular, and possibly mechanized proofs of component properties parameterized with timing and scheduling characteristics. |

12:00 | An Axiomatic Approach to Liveness for Differential Equations ABSTRACT. This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties prevent the generalization of well-known discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions rarely exist in closed-form, they may blow up in finite time, or their progress towards the goal may converge to zero. Our approach handles these subtleties by successively refining ODE liveness properties using ODE invariance properties which have a well-understood deductive proof theory. This approach is widely applicable: we survey several liveness arguments in the literature and derive them as special instances of our axiomatic refinement approach. We also correct several soundness errors in the surveyed arguments, which further highlights the subtlety of ODE liveness reasoning and the utility of our deductive approach. The library of common refinement steps identified through our approach enables both the sound development and justification of new ODE liveness proof rules from our axioms. |