Partial orders for efficient bounded model checking of concurrent software

Partial orders for efficient bounded model checking of concurrent software

The number of interleavings of a concurrent program makes automatic analysis of such software very hard. Modern multiprocessors’ execution models make this problem even harder. Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient en...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Alglave, J, Kroening, D, Tautschnig, M
Rannpháirtithe:	Sharygina, N
Formáid:	Conference item
Foilsithe / Cruthaithe:	Springer 2013

Míreanna comhchosúla

Making Software Verification Tools Really Work
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2011)

Software Verification for Weak Memory via Program Transformation
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2013)

Software verification for weak memory via program transformation
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2013)

Static Analysis to Enhance the Power of Model Checking for Concurrent Software
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2007)

Incremental bounded model checking for embedded software
de réir: Schrammel, P, et al.
Foilsithe / Cruthaithe: (2017)

CBMC – C bounded model checker
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2014)

Computing Over−Approximations with Bounded Model Checking
de réir: Kroening, D
Foilsithe / Cruthaithe: (2006)

Computing over-approximations with bounded model checking
de réir: Kroening, D
Foilsithe / Cruthaithe: (2006)

Computational challenges in bounded model checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2005)

Completeness and Complexity of Bounded Model Checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Computational challenges in bounded model checking.
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2005)

Computational Challenges in Bounded Model Checking
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2015)

Model Checking Concurrent Linux Device Drivers
de réir: Witkowski, T, et al.
Foilsithe / Cruthaithe: (2007)

Model checking concurrent linux device drivers
de réir: Witkowski, T, et al.
Foilsithe / Cruthaithe: (2007)

Soundness of Data Flow Analyses for Weak Memory Models
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2011)

Soundness of data flow analyses for weak memory models
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2011)

Soundness of Data Flow Analyses for Weak Memory Models
de réir: Alglave, J, et al.
Foilsithe / Cruthaithe: (2011)

Linear Completeness Thresholds for Bounded Model Checking.
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2011)

Proving safety with trace automata and bounded model checking
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2015)

Towards automated bounded model checking of API implementations
de réir: Neville, D, et al.
Foilsithe / Cruthaithe: (2016)

Property-driven fence insertion using reorder bounded model checking
de réir: Joshi, S, et al.
Foilsithe / Cruthaithe: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
de réir: Joshi, S, et al.
Foilsithe / Cruthaithe: (2015)

A Complete Bounded Model Checking Algorithm for Pushdown Systems
de réir: Basler, G, et al.
Foilsithe / Cruthaithe: (2007)

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
de réir: Horn, A, et al.
Foilsithe / Cruthaithe: (2015)

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
de réir: Horn, A, et al.
Foilsithe / Cruthaithe: (2015)

Model checking boot code from AWS data centers
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2018)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2003)

JBMC: a bounded model checking tool for verifying Java bytecode
de réir: Cordeiro, L, et al.
Foilsithe / Cruthaithe: (2018)

Numeric bounds analysis with conflict-driven learning
de réir: D'Silva, V, et al.
Foilsithe / Cruthaithe: (2012)

Model-checking games for fixpoint logics with partial order models
de réir: Gutierrez, J, et al.
Foilsithe / Cruthaithe: (2010)

Model-checking games for fixpoint logics with partial order models
de réir: Gutierrez, J, et al.
Foilsithe / Cruthaithe: (2009)

Model-checking games for fixpoint logics with partial order models
de réir: Gutierrez, J, et al.
Foilsithe / Cruthaithe: (2011)

Concurrent logic games on partial orders
de réir: Gutierrez, J
Foilsithe / Cruthaithe: (2011)

Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking
de réir: Wenjie Zhong, et al.
Foilsithe / Cruthaithe: (2023-02-01)

Effective verification for low-level software with competing interrupts
de réir: Liang, L, et al.
Foilsithe / Cruthaithe: (2017)

The parameterized space complexity of model-checking bounded variable first-order logic
de réir: Yijia Chen, et al.
Foilsithe / Cruthaithe: (2019-09-01)

Model Checking with Abstraction for Web Services
de réir: Sharygina, N, et al.
Foilsithe / Cruthaithe: (2007)

On the Magnitude of Completeness Thresholds in Bounded Model Checking
de réir: Bundala, D, et al.
Foilsithe / Cruthaithe: (2012)

Coverage in interpolation-based model checking
de réir: Chockler, H, et al.
Foilsithe / Cruthaithe: (2010)

Checking Concurrent Contracts with Aspects
de réir: Kerfoot, E, et al.
Foilsithe / Cruthaithe: (2010)