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...

书目详细资料
Main Authors:	Kroening, D, Lewis, M, Weissenbacher, G
其他作者:	Bjørner, N
格式:	Conference item
出版:	Springer 2015

相似书籍

A Complete Bounded Model Checking Algorithm for Pushdown Systems
由: Basler, G, et al.
出版: (2007)

Computing Over−Approximations with Bounded Model Checking
由: Kroening, D
出版: (2006)

Computing over-approximations with bounded model checking
由: Kroening, D
出版: (2006)

Model Checking Concurrent Linux Device Drivers
由: Witkowski, T, et al.
出版: (2007)

Model checking concurrent linux device drivers
由: Witkowski, T, et al.
出版: (2007)

Computational Challenges in Bounded Model Checking
由: Clarke, E, et al.
出版: (2015)

Computational challenges in bounded model checking
由: Clarke, E, et al.
出版: (2005)

Completeness and Complexity of Bounded Model Checking
由: Clarke, E, et al.
出版: (2004)

Computational challenges in bounded model checking.
由: Clarke, E, et al.
出版: (2005)

Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
由: Rui Wang, et al.
出版: (2013-01-01)

Incremental bounded model checking for embedded software
由: Schrammel, P, et al.
出版: (2017)

Towards automated bounded model checking of API implementations
由: Neville, D, et al.
出版: (2016)

Linear Completeness Thresholds for Bounded Model Checking.
由: Kroening, D, et al.
出版: (2011)

Property-driven fence insertion using reorder bounded model checking
由: Joshi, S, et al.
出版: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
由: Joshi, S, et al.
出版: (2015)

Partial orders for efficient bounded model checking of concurrent software
由: Alglave, J, et al.
出版: (2013)

Equivalence checking using trace partitioning
由: Mukherjee, R, et al.
出版: (2015)

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks
由: Agnieszka M. Zbrzezny, et al.
出版: (2022-12-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
由: Kroening, D, et al.
出版: (2003)

Active learning of abstract system models from traces using model checking
由: Yogananda Jeppu, N, et al.
出版: (2022)

On the complexity of model checking counter automata
由: Haase, C
出版: (2012)

Model Checking Probabilistic Pushdown Automata
由: Javier Esparza, et al.
出版: (2006-03-01)

JBMC: a bounded model checking tool for verifying Java bytecode
由: Cordeiro, L, et al.
出版: (2018)

Model-Checking of Ordered Multi-Pushdown Automata
由: Mohamed Faouzi Atig
出版: (2012-09-01)

Antichains for the Automata-Based Approach to Model-Checking
由: Laurent Doyen, et al.
出版: (2009-03-01)

Model Checking One-clock Priced Timed Automata
由: Patricia Bouyer, et al.
出版: (2008-06-01)

Proving the Correctness of Pipelined Micro−Architectures
由: Kroening, D, et al.
出版: (2000)

Bounded Parikh Automata
由: Michaël Cadilhac, et al.
出版: (2011-08-01)

Branching-Time Model-Checking of Probabilistic Pushdown Automata.
由: Brázdil, T, et al.
出版: (2009)

Model Checking Succinct and Parametric One-Counter Automata.
由: Göller, S, et al.
出版: (2010)

Model Checking Succinct and Parametric One−Counter Automata
由: Göller, S, et al.
出版: (2010)

Timed Automata Robustness Analysis via Model Checking
由: Jaroslav Bendík, et al.
出版: (2022-07-01)

How the Upper Bound Conjecture Was Proved
由: Stanley, Richard P.
出版: (2015)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
由: Melham, T
出版: (2004)

Translating timed I/O automata specifications for theorem proving in PVs
由: Lim, Hongping
出版: (2007)

Accurate Theorem Proving for Program Verification
由: Cook, B, et al.
出版: (2006)

Automata‚ Model Checking and Synthesis for Linear Time Temporal Logics
由: Hague, M
出版: (2006)

Cogent: Accurate theorem proving for program verification
由: Cook, B, et al.
出版: (2005)

Extensions of Presburger arithmetic and model checking one-counter automata
由: Lechner, A
出版: (2016)

Model checking flat freeze LTL on one-counter automata
由: Lechner, A, et al.
出版: (2016)