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

Fuld beskrivelse

Bibliografiske detaljer
Main Authors:	Alglave, J, Kroening, D, Tautschnig, M
Andre forfattere:	Sharygina, N
Format:	Conference item
Udgivet:	Springer 2013

Lignende værker

Making Software Verification Tools Really Work
af: Alglave, J, et al.
Udgivet: (2011)

Software Verification for Weak Memory via Program Transformation
af: Alglave, J, et al.
Udgivet: (2013)

Software verification for weak memory via program transformation
af: Alglave, J, et al.
Udgivet: (2013)

Static Analysis to Enhance the Power of Model Checking for Concurrent Software
af: Clarke, E, et al.
Udgivet: (2007)

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

CBMC – C bounded model checker
af: Kroening, D, et al.
Udgivet: (2014)

Computing Over−Approximations with Bounded Model Checking
af: Kroening, D
Udgivet: (2006)

Computing over-approximations with bounded model checking
af: Kroening, D
Udgivet: (2006)

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

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

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

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

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

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

Soundness of Data Flow Analyses for Weak Memory Models
af: Alglave, J, et al.
Udgivet: (2011)

Soundness of data flow analyses for weak memory models
af: Alglave, J, et al.
Udgivet: (2011)

Soundness of Data Flow Analyses for Weak Memory Models
af: Alglave, J, et al.
Udgivet: (2011)

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

Proving safety with trace automata and bounded model checking
af: Kroening, D, et al.
Udgivet: (2015)

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

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

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

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

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
af: Horn, A, et al.
Udgivet: (2015)

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
af: Horn, A, et al.
Udgivet: (2015)

Model checking boot code from AWS data centers
af: Cook, B, et al.
Udgivet: (2018)

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

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

Numeric bounds analysis with conflict-driven learning
af: D'Silva, V, et al.
Udgivet: (2012)

Model-checking games for fixpoint logics with partial order models
af: Gutierrez, J, et al.
Udgivet: (2010)

Model-checking games for fixpoint logics with partial order models
af: Gutierrez, J, et al.
Udgivet: (2009)

Model-checking games for fixpoint logics with partial order models
af: Gutierrez, J, et al.
Udgivet: (2011)

Concurrent logic games on partial orders
af: Gutierrez, J
Udgivet: (2011)

Concurrent software fine‐coarse‐grained automatic modelling by Coloured Petri Nets for model checking
af: Wenjie Zhong, et al.
Udgivet: (2023-02-01)

Effective verification for low-level software with competing interrupts
af: Liang, L, et al.
Udgivet: (2017)

The parameterized space complexity of model-checking bounded variable first-order logic
af: Yijia Chen, et al.
Udgivet: (2019-09-01)

Model Checking with Abstraction for Web Services
af: Sharygina, N, et al.
Udgivet: (2007)

On the Magnitude of Completeness Thresholds in Bounded Model Checking
af: Bundala, D, et al.
Udgivet: (2012)

Coverage in interpolation-based model checking
af: Chockler, H, et al.
Udgivet: (2010)

Checking Concurrent Contracts with Aspects
af: Kerfoot, E, et al.
Udgivet: (2010)