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

Descripció completa

Dades bibliogràfiques
Autors principals:	Kroening, D, Lewis, M, Weissenbacher, G
Altres autors:	Bjørner, N
Format:	Conference item
Publicat:	Springer 2015

Ítems similars

A Complete Bounded Model Checking Algorithm for Pushdown Systems
per: Basler, G, et al.
Publicat: (2007)

Computing Over−Approximations with Bounded Model Checking
per: Kroening, D
Publicat: (2006)

Computing over-approximations with bounded model checking
per: Kroening, D
Publicat: (2006)

Model Checking Concurrent Linux Device Drivers
per: Witkowski, T, et al.
Publicat: (2007)

Model checking concurrent linux device drivers
per: Witkowski, T, et al.
Publicat: (2007)

Computational Challenges in Bounded Model Checking
per: Clarke, E, et al.
Publicat: (2015)

Computational challenges in bounded model checking
per: Clarke, E, et al.
Publicat: (2005)

Completeness and Complexity of Bounded Model Checking
per: Clarke, E, et al.
Publicat: (2004)

Computational challenges in bounded model checking.
per: Clarke, E, et al.
Publicat: (2005)

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

Incremental bounded model checking for embedded software
per: Schrammel, P, et al.
Publicat: (2017)

Towards automated bounded model checking of API implementations
per: Neville, D, et al.
Publicat: (2016)

Linear Completeness Thresholds for Bounded Model Checking.
per: Kroening, D, et al.
Publicat: (2011)

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

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

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

Equivalence checking using trace partitioning
per: Mukherjee, R, et al.
Publicat: (2015)

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

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

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

On the complexity of model checking counter automata
per: Haase, C
Publicat: (2012)

Model Checking Probabilistic Pushdown Automata
per: Javier Esparza, et al.
Publicat: (2006-03-01)

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

Model-Checking of Ordered Multi-Pushdown Automata
per: Mohamed Faouzi Atig
Publicat: (2012-09-01)

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

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

Proving the Correctness of Pipelined Micro−Architectures
per: Kroening, D, et al.
Publicat: (2000)

Bounded Parikh Automata
per: Michaël Cadilhac, et al.
Publicat: (2011-08-01)

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

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

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

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

How the Upper Bound Conjecture Was Proved
per: Stanley, Richard P.
Publicat: (2015)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
per: Melham, T
Publicat: (2004)

Translating timed I/O automata specifications for theorem proving in PVs
per: Lim, Hongping
Publicat: (2007)

Accurate Theorem Proving for Program Verification
per: Cook, B, et al.
Publicat: (2006)

Automata‚ Model Checking and Synthesis for Linear Time Temporal Logics
per: Hague, M
Publicat: (2006)

Cogent: Accurate theorem proving for program verification
per: Cook, B, et al.
Publicat: (2005)

Extensions of Presburger arithmetic and model checking one-counter automata
per: Lechner, A
Publicat: (2016)

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