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

Descrizione completa

Dettagli Bibliografici
Autori principali:	Kroening, D, Lewis, M, Weissenbacher, G
Altri autori:	Bjørner, N
Natura:	Conference item
Pubblicazione:	Springer 2015

Documenti analoghi

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

Computing Over−Approximations with Bounded Model Checking
di: Kroening, D
Pubblicazione: (2006)

Computing over-approximations with bounded model checking
di: Kroening, D
Pubblicazione: (2006)

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

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

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

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

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

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

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

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

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

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

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

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

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

Equivalence checking using trace partitioning
di: Mukherjee, R, et al.
Pubblicazione: (2015)

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

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

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

On the complexity of model checking counter automata
di: Haase, C
Pubblicazione: (2012)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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