Proving safety with trace automata and bounded model checking

Proving safety with trace automata and bounded model checking

Loop under-approximation enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up bug detection significantly, it introduces redundant execution traces which may complicate the verification of the program. This...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính:	Kroening, D, Lewis, M, Weissenbacher, G
Tác giả khác:	Bjørner, N
Định dạng:	Conference item
Được phát hành:	Springer 2015

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

A Complete Bounded Model Checking Algorithm for Pushdown Systems
Bằng: Basler, G, et al.
Được phát hành: (2007)

Computing Over−Approximations with Bounded Model Checking
Bằng: Kroening, D
Được phát hành: (2006)

Computing over-approximations with bounded model checking
Bằng: Kroening, D
Được phát hành: (2006)

Model Checking Concurrent Linux Device Drivers
Bằng: Witkowski, T, et al.
Được phát hành: (2007)

Model checking concurrent linux device drivers
Bằng: Witkowski, T, et al.
Được phát hành: (2007)

Computational Challenges in Bounded Model Checking
Bằng: Clarke, E, et al.
Được phát hành: (2015)

Computational challenges in bounded model checking
Bằng: Clarke, E, et al.
Được phát hành: (2005)

Completeness and Complexity of Bounded Model Checking
Bằng: Clarke, E, et al.
Được phát hành: (2004)

Computational challenges in bounded model checking.
Bằng: Clarke, E, et al.
Được phát hành: (2005)

Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
Bằng: Rui Wang, et al.
Được phát hành: (2013-01-01)

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

Towards automated bounded model checking of API implementations
Bằng: Neville, D, et al.
Được phát hành: (2016)

Linear Completeness Thresholds for Bounded Model Checking.
Bằng: Kroening, D, et al.
Được phát hành: (2011)

Property-driven fence insertion using reorder bounded model checking
Bằng: Joshi, S, et al.
Được phát hành: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
Bằng: Joshi, S, et al.
Được phát hành: (2015)

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

Equivalence checking using trace partitioning
Bằng: Mukherjee, R, et al.
Được phát hành: (2015)

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks
Bằng: Agnieszka M. Zbrzezny, et al.
Được phát hành: (2022-12-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
Bằng: Kroening, D, et al.
Được phát hành: (2003)

Active learning of abstract system models from traces using model checking
Bằng: Yogananda Jeppu, N, et al.
Được phát hành: (2022)

On the complexity of model checking counter automata
Bằng: Haase, C
Được phát hành: (2012)

Model Checking Probabilistic Pushdown Automata
Bằng: Javier Esparza, et al.
Được phát hành: (2006-03-01)

JBMC: a bounded model checking tool for verifying Java bytecode
Bằng: Cordeiro, L, et al.
Được phát hành: (2018)

Model-Checking of Ordered Multi-Pushdown Automata
Bằng: Mohamed Faouzi Atig
Được phát hành: (2012-09-01)

Antichains for the Automata-Based Approach to Model-Checking
Bằng: Laurent Doyen, et al.
Được phát hành: (2009-03-01)

Model Checking One-clock Priced Timed Automata
Bằng: Patricia Bouyer, et al.
Được phát hành: (2008-06-01)

Proving the Correctness of Pipelined Micro−Architectures
Bằng: Kroening, D, et al.
Được phát hành: (2000)

Bounded Parikh Automata
Bằng: Michaël Cadilhac, et al.
Được phát hành: (2011-08-01)

Branching-Time Model-Checking of Probabilistic Pushdown Automata.
Bằng: Brázdil, T, et al.
Được phát hành: (2009)

Model Checking Succinct and Parametric One-Counter Automata.
Bằng: Göller, S, et al.
Được phát hành: (2010)

Model Checking Succinct and Parametric One−Counter Automata
Bằng: Göller, S, et al.
Được phát hành: (2010)

Timed Automata Robustness Analysis via Model Checking
Bằng: Jaroslav Bendík, et al.
Được phát hành: (2022-07-01)

How the Upper Bound Conjecture Was Proved
Bằng: Stanley, Richard P.
Được phát hành: (2015)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
Bằng: Melham, T
Được phát hành: (2004)

Translating timed I/O automata specifications for theorem proving in PVs
Bằng: Lim, Hongping
Được phát hành: (2007)

Accurate Theorem Proving for Program Verification
Bằng: Cook, B, et al.
Được phát hành: (2006)

Automata‚ Model Checking and Synthesis for Linear Time Temporal Logics
Bằng: Hague, M
Được phát hành: (2006)

Cogent: Accurate theorem proving for program verification
Bằng: Cook, B, et al.
Được phát hành: (2005)

Extensions of Presburger arithmetic and model checking one-counter automata
Bằng: Lechner, A
Được phát hành: (2016)

Model checking flat freeze LTL on one-counter automata
Bằng: Lechner, A, et al.
Được phát hành: (2016)