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

Szczegółowa specyfikacja

Opis bibliograficzny
Główni autorzy:	Kroening, D, Lewis, M, Weissenbacher, G
Kolejni autorzy:	Bjørner, N
Format:	Conference item
Wydane:	Springer 2015

Podobne zapisy

A Complete Bounded Model Checking Algorithm for Pushdown Systems
od: Basler, G, i wsp.
Wydane: (2007)

Computing Over−Approximations with Bounded Model Checking
od: Kroening, D
Wydane: (2006)

Computing over-approximations with bounded model checking
od: Kroening, D
Wydane: (2006)

Model Checking Concurrent Linux Device Drivers
od: Witkowski, T, i wsp.
Wydane: (2007)

Model checking concurrent linux device drivers
od: Witkowski, T, i wsp.
Wydane: (2007)

Computational Challenges in Bounded Model Checking
od: Clarke, E, i wsp.
Wydane: (2015)

Computational challenges in bounded model checking
od: Clarke, E, i wsp.
Wydane: (2005)

Completeness and Complexity of Bounded Model Checking
od: Clarke, E, i wsp.
Wydane: (2004)

Computational challenges in bounded model checking.
od: Clarke, E, i wsp.
Wydane: (2005)

Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
od: Rui Wang, i wsp.
Wydane: (2013-01-01)

Incremental bounded model checking for embedded software
od: Schrammel, P, i wsp.
Wydane: (2017)

Towards automated bounded model checking of API implementations
od: Neville, D, i wsp.
Wydane: (2016)

Linear Completeness Thresholds for Bounded Model Checking.
od: Kroening, D, i wsp.
Wydane: (2011)

Property-driven fence insertion using reorder bounded model checking
od: Joshi, S, i wsp.
Wydane: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
od: Joshi, S, i wsp.
Wydane: (2015)

Partial orders for efficient bounded model checking of concurrent software
od: Alglave, J, i wsp.
Wydane: (2013)

Equivalence checking using trace partitioning
od: Mukherjee, R, i wsp.
Wydane: (2015)

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks
od: Agnieszka M. Zbrzezny, i wsp.
Wydane: (2022-12-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
od: Kroening, D, i wsp.
Wydane: (2003)

Active learning of abstract system models from traces using model checking
od: Yogananda Jeppu, N, i wsp.
Wydane: (2022)

On the complexity of model checking counter automata
od: Haase, C
Wydane: (2012)

Model Checking Probabilistic Pushdown Automata
od: Javier Esparza, i wsp.
Wydane: (2006-03-01)

JBMC: a bounded model checking tool for verifying Java bytecode
od: Cordeiro, L, i wsp.
Wydane: (2018)

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

Antichains for the Automata-Based Approach to Model-Checking
od: Laurent Doyen, i wsp.
Wydane: (2009-03-01)

Model Checking One-clock Priced Timed Automata
od: Patricia Bouyer, i wsp.
Wydane: (2008-06-01)

Proving the Correctness of Pipelined Micro−Architectures
od: Kroening, D, i wsp.
Wydane: (2000)

Bounded Parikh Automata
od: Michaël Cadilhac, i wsp.
Wydane: (2011-08-01)

Branching-Time Model-Checking of Probabilistic Pushdown Automata.
od: Brázdil, T, i wsp.
Wydane: (2009)

Model Checking Succinct and Parametric One-Counter Automata.
od: Göller, S, i wsp.
Wydane: (2010)

Model Checking Succinct and Parametric One−Counter Automata
od: Göller, S, i wsp.
Wydane: (2010)

Timed Automata Robustness Analysis via Model Checking
od: Jaroslav Bendík, i wsp.
Wydane: (2022-07-01)

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

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

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

Accurate Theorem Proving for Program Verification
od: Cook, B, i wsp.
Wydane: (2006)

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

Cogent: Accurate theorem proving for program verification
od: Cook, B, i wsp.
Wydane: (2005)

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

Model checking flat freeze LTL on one-counter automata
od: Lechner, A, i wsp.
Wydane: (2016)