Effective verification for low-level software with competing interrupts

Effective verification for low-level software with competing interrupts

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an exponential blow-up in the number of cases to consider. We present a new formal approach to verifying interrupt-driven...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính:	Liang, L, Melham, T, Kroening, DHF, Schrammel, P, Tautschnig, M
Định dạng:	Journal article
Được phát hành:	Association for Computing Machinery 2017

Những quyển sách tương tự

Unbounded Safety Verification for Hardware Using Software Analyzers
Bằng: Mukherjee, R, et al.
Được phát hành: (2015)

Formal co−validation of low−level hardware/software interfaces
Bằng: Horn, A, et al.
Được phát hành: (2013)

Formal Co-Validation of Low-Level Hardware/Software Interfaces
Bằng: Horn, A, et al.
Được phát hành: (2013)

Hardware verification using software analyzers
Bằng: Mukherjee, R, et al.
Được phát hành: (2015)

Lifting CDCL to template-based abstract domains for program verification
Bằng: Mukherjee, R, et al.
Được phát hành: (2017)

Making Software Verification Tools Really Work
Bằng: Alglave, J, et al.
Được phát hành: (2011)

Software Verification for Weak Memory via Program Transformation
Bằng: Alglave, J, et al.
Được phát hành: (2013)

Software verification for weak memory via program transformation
Bằng: Alglave, J, et al.
Được phát hành: (2013)

Generating test case chains for reactive systems
Bằng: Schrammel, P, et al.
Được phát hành: (2016)

Chaining Test Cases for Reactive System Testing
Bằng: Schrammel, P, et al.
Được phát hành: (2013)

Safety verification and refutation by k-invariants and k-induction
Bằng: Brain, M, et al.
Được phát hành: (2015)

Software Verification Using k−Induction
Bằng: Donaldson, A, et al.
Được phát hành: (2011)

Software verification using k-induction
Bằng: Donaldson, A, et al.
Được phát hành: (2011)

Verification of tree-based hierarchical read-copy update in the Linux kernel
Bằng: Liang, L, et al.
Được phát hành: (2018)

Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
Bằng: Cattaruzza, D, et al.
Được phát hành: (2020)

Partial orders for efficient bounded model checking of concurrent software
Bằng: Alglave, J, et al.
Được phát hành: (2013)

Assisted coverage closure.
Bằng: Nellis, A, et al.
Được phát hành: (2016)

Assisted coverage closure
Bằng: Nellis, A, et al.
Được phát hành: (2016)

Algebraic Techniques in Software Verification : Challenges and Opportunities
Bằng: Brain, M, et al.
Được phát hành: (2016)

Incremental bounded model checking for embedded software
Bằng: Schrammel, P, et al.
Được phát hành: (2017)

Formal techniques for effective co-verification of hardware/software co-designs
Bằng: Mukherjee, R, et al.
Được phát hành: (2017)

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
Bằng: Kroening, D, et al.
Được phát hành: (2005)

A survey of automated techniques for formal software verification
Bằng: D'Silva, V, et al.
Được phát hành: (2008)

A Survey of Automated Techniques for Formal Software Verification.
Bằng: D'Silva, V, et al.
Được phát hành: (2008)

A Survey of Automated Techniques for Formal Software Verification
Bằng: D'Silva, V, et al.
Được phát hành: (2008)

Formal Verification at Higher Levels of Abstraction
Bằng: Kroening, D, et al.
Được phát hành: (2007)

Challenges in Decomposing Encodings of Verification Problems
Bằng: Peter Schrammel
Được phát hành: (2016-07-01)

Abstraction Mechanisms for Hardware Verification
Bằng: Melham, T
Được phát hành: (1990)

Abstraction Mechanisms for Hardware Verification
Bằng: Melham, T
Được phát hành: (1988)

Abstraction Mechanisms for Hardware Verification
Bằng: Melham, T
Được phát hành: (1987)

Higher Order Logic and Hardware Verification
Bằng: Melham, T
Được phát hành: (1993)

ExpliSAT: Guiding SAT−Based Software Verification with Explicit States
Bằng: Barner, S, et al.
Được phát hành: (2007)

Design and Verification of On−Chip Communication Protocols
Bằng: Böhm, P, et al.
Được phát hành: (2015)

Design and Verification of On−Chip Communication Protocols
Bằng: Böhm, P, et al.
Được phát hành: (2015)

Design and Verification of On−Chip Communication Protocols
Bằng: Böhm, P, et al.
Được phát hành: (2008)

CBMC – C bounded model checker
Bằng: Kroening, D, et al.
Được phát hành: (2014)

Verification of Data Races in Concurrent Interrupt Handlers
Bằng: Guy Martin Tchamgoue, et al.
Được phát hành: (2013-11-01)

Abstract: Experience with Practical Formal Verification at an Industrial Scale
Bằng: Melham, T
Được phát hành: (2003)

Logico−Numerical Abstract Acceleration and Application to the Verification of Data−Flow Programs
Bằng: Schrammel, P, et al.
Được phát hành: (2011)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
Bằng: Melham, T
Được phát hành: (1989)