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

Detaylı Bibliyografya
Asıl Yazarlar:	Kroening, D, Lewis, M, Weissenbacher, G
Diğer Yazarlar:	Bjørner, N
Materyal Türü:	Conference item
Baskı/Yayın Bilgisi:	Springer 2015

Benzer Materyaller

A Complete Bounded Model Checking Algorithm for Pushdown Systems
Yazar:: Basler, G, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Computing Over−Approximations with Bounded Model Checking
Yazar:: Kroening, D
Baskı/Yayın Bilgisi: (2006)

Computing over-approximations with bounded model checking
Yazar:: Kroening, D
Baskı/Yayın Bilgisi: (2006)

Model Checking Concurrent Linux Device Drivers
Yazar:: Witkowski, T, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Model checking concurrent linux device drivers
Yazar:: Witkowski, T, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Computational Challenges in Bounded Model Checking
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

Computational challenges in bounded model checking
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Completeness and Complexity of Bounded Model Checking
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Computational challenges in bounded model checking.
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
Yazar:: Rui Wang, ve diğerleri
Baskı/Yayın Bilgisi: (2013-01-01)

Incremental bounded model checking for embedded software
Yazar:: Schrammel, P, ve diğerleri
Baskı/Yayın Bilgisi: (2017)

Towards automated bounded model checking of API implementations
Yazar:: Neville, D, ve diğerleri
Baskı/Yayın Bilgisi: (2016)

Linear Completeness Thresholds for Bounded Model Checking.
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2011)

Property-driven fence insertion using reorder bounded model checking
Yazar:: Joshi, S, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
Yazar:: Joshi, S, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

Partial orders for efficient bounded model checking of concurrent software
Yazar:: Alglave, J, ve diğerleri
Baskı/Yayın Bilgisi: (2013)

Equivalence checking using trace partitioning
Yazar:: Mukherjee, R, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks
Yazar:: Agnieszka M. Zbrzezny, ve diğerleri
Baskı/Yayın Bilgisi: (2022-12-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2003)

Active learning of abstract system models from traces using model checking
Yazar:: Yogananda Jeppu, N, ve diğerleri
Baskı/Yayın Bilgisi: (2022)

On the complexity of model checking counter automata
Yazar:: Haase, C
Baskı/Yayın Bilgisi: (2012)

Model Checking Probabilistic Pushdown Automata
Yazar:: Javier Esparza, ve diğerleri
Baskı/Yayın Bilgisi: (2006-03-01)

JBMC: a bounded model checking tool for verifying Java bytecode
Yazar:: Cordeiro, L, ve diğerleri
Baskı/Yayın Bilgisi: (2018)

Model-Checking of Ordered Multi-Pushdown Automata
Yazar:: Mohamed Faouzi Atig
Baskı/Yayın Bilgisi: (2012-09-01)

Antichains for the Automata-Based Approach to Model-Checking
Yazar:: Laurent Doyen, ve diğerleri
Baskı/Yayın Bilgisi: (2009-03-01)

Model Checking One-clock Priced Timed Automata
Yazar:: Patricia Bouyer, ve diğerleri
Baskı/Yayın Bilgisi: (2008-06-01)

Proving the Correctness of Pipelined Micro−Architectures
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2000)

Bounded Parikh Automata
Yazar:: Michaël Cadilhac, ve diğerleri
Baskı/Yayın Bilgisi: (2011-08-01)

Branching-Time Model-Checking of Probabilistic Pushdown Automata.
Yazar:: Brázdil, T, ve diğerleri
Baskı/Yayın Bilgisi: (2009)

Model Checking Succinct and Parametric One-Counter Automata.
Yazar:: Göller, S, ve diğerleri
Baskı/Yayın Bilgisi: (2010)

Model Checking Succinct and Parametric One−Counter Automata
Yazar:: Göller, S, ve diğerleri
Baskı/Yayın Bilgisi: (2010)

Timed Automata Robustness Analysis via Model Checking
Yazar:: Jaroslav Bendík, ve diğerleri
Baskı/Yayın Bilgisi: (2022-07-01)

How the Upper Bound Conjecture Was Proved
Yazar:: Stanley, Richard P.
Baskı/Yayın Bilgisi: (2015)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
Yazar:: Melham, T
Baskı/Yayın Bilgisi: (2004)

Translating timed I/O automata specifications for theorem proving in PVs
Yazar:: Lim, Hongping
Baskı/Yayın Bilgisi: (2007)

Accurate Theorem Proving for Program Verification
Yazar:: Cook, B, ve diğerleri
Baskı/Yayın Bilgisi: (2006)

Automata‚ Model Checking and Synthesis for Linear Time Temporal Logics
Yazar:: Hague, M
Baskı/Yayın Bilgisi: (2006)

Cogent: Accurate theorem proving for program verification
Yazar:: Cook, B, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Extensions of Presburger arithmetic and model checking one-counter automata
Yazar:: Lechner, A
Baskı/Yayın Bilgisi: (2016)

Model checking flat freeze LTL on one-counter automata
Yazar:: Lechner, A, ve diğerleri
Baskı/Yayın Bilgisi: (2016)