We present abstract acceleration techniques for computing loop invariants numerical programs with linear assignments and conditionals. Whereas interpretation typically over-approximate the set of reachable states iteratively, captures effect a single, non-iterative transfer function applied to initial at head. In contrast previous techniques, our approach applies any without restrictions. Its novelty lies in use Jordan normal form decomposition body derive symbolic expressions entries matrix...

Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities denial-of-service attacks. To make checks scale large systems, interprocedural analysis seems essential, which a largely unexplored area research in analysis, where most effort has focussed on difficult single-procedure problems. We present modular for C using template-based summarisation. Our combines context-sensitive, over-approximating forward...

We present a static deadlock analysis approach for C/pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our is sound (i.e., misses no deadlocks) programs that have defined behaviour according C standard and pthreads specification, precise enough prove deadlock-freedom large number such programs. consists pipeline several analyses build on new context- thread-sensitive abstract interpretation framework. further lightweight dependency identify...

Abstract Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification behavioural requirements, finding runtime errors and test case generation are some most common applications automated tools based bounded model checking (BMC). Existing industrial for software use an off-the-shelf checker apply it iteratively to verify program with increasing number unwindings. This approach unnecessarily wastes time repeating work that has already been done...

Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems be analysed in parallel. We exploit this here and use parametrizable code-to-code translation generate set of simpler instances, each capturing reduced the original program's interleavings. These instances then checked independently Our approach does not depend on tool that is chosen final analysis, compatible with weak memory models, amplifies effectiveness existing...

As product life-cycles become shorter and the scale complexity of systems increase, accelerating execution large test suites gains importance. Existing research has primarily focussed on techniques that reduce size suite. By contrast, we propose a technique accelerates execution, allowing to run in fraction original time, by parallel with Graphics Processing Unit (GPU).

Hybrid systems are used to model embedded computing interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like Simulink, which for simulation, and automata, the most suitable representation safety verification. Indeed, in simulation interaction discrete continuous execution steps specified using concept of zero-crossings, whereas automata exploit notion staying conditions. We describe translation from data-flow language...

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested subject priorities. Interrupts arrive at arbitrary times, leading an explosion in the number of cases considered. We present a new formal approach verifying interrupt-driven based on symbolic execution. The leverages recent advances encoding execution traces interacting, concurrent threads. assess performance our method benchmarks drawn from embedded systems code device drivers, experimentally...

Non-termination is the root cause of a variety program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove absence bugs highly desirable. To scale termination checks to large systems, interprocedural seems essential. largely unexplored area research in analysis, where most effort has focussed on small but difficult single-procedure problems. We present modular for C using template-based summarisation. Our combines...

We present abstract acceleration techniques for computing loop invariants numerical programs with linear assignments and conditionals. Whereas interpretation typically over-approximate the set of reachable states iteratively, captures effect a single, non-iterative transfer function applied to initial at head. In contrast previous techniques, our approach applies any without restrictions. Its novelty lies in use Jordan normal form decomposition body derive symbolic expressions entries matrix...

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested subject priorities. Interrupts arrive at arbitrary times, leading an explosion in the number of cases considered. We present a new formal approach verifying interrupt-driven based on symbolic execution. The leverages recent advances encoding execution traces interacting, concurrent threads. assess performance our method benchmarks drawn from embedded systems code device drivers, experimentally...

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested subject priorities. Interrupts arrive at arbitrary times, leading an exponential blow-up in the number of cases consider. We present a new formal approach verifying interrupt-driven based on symbolic execution. The leverages recent advances encoding execution traces interacting, concurrent threads. assess performance our method benchmarks drawn from embedded systems code device drivers,...