Efficient coverability analysis by proof minimization

Efficient coverability analysis by proof minimization

We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the coverability problem for well-structured transition systems (WSTS). In this paper, we present a novel, sou...

書誌詳細
主要な著者:	Kaiser, A, Kroening, D, Wahl, T
その他の著者:	Koutny, M
フォーマット:	Conference item
出版事項:	Springer 2012

類似資料

Lost in abstraction: monotonicity in multi-threaded programs
著者:: Kaiser, A, 等
出版事項: (2016)

Lost in abstraction: monotonicity in multi-threaded programs
著者:: Kaiser, A, 等
出版事項: (2014)

A widening approach to multithreaded program verification
著者:: Kaiser, A, 等
出版事項: (2014)

Proof-graphs for Minimal Implicational Logic
著者:: Marcela Quispe-Cruz, 等
出版事項: (2014-03-01)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
著者:: Kroening, D, 等
出版事項: (2007)

Model and proof generation for heap-manipulating programs
著者:: Brain, M, 等
出版事項: (2014)

Model and Proof Generation for Heap−Manipulating Programs
著者:: Brain, M, 等
出版事項: (2014)

Synthesising interprocedural bit-precise termination proofs
著者:: Chen, H, 等
出版事項: (2016)

A First Step Towards a Unified Proof Checker for QBF
著者:: Jussila, T, 等
出版事項: (2007)

Audiomotor Integration in Minimally Conscious State: Proof of Concept!
著者:: Antonino Naro, 等
出版事項: (2015-01-01)

Efficient holographic proofs
著者:: Russell, Alexander Craig
出版事項: (2007)

Efficient Standard of Proof
著者:: Iraj Babaei, 等
出版事項: (2021-12-01)

Projective covers and minimal free resolutions
著者:: Mark A. Goddard
出版事項: (1996-01-01)

The minimal covering set in large tournaments
著者:: Scott, A, 等
出版事項: (2012)

High-performance noise proof cover using acoustic tube
著者:: Daisuke MUTO, 等
出版事項: (2014-10-01)

Super-efficient rational proofs
著者:: Azar, Pablo Daniel
出版事項: (2015)

Depth-efficient proofs of quantumness
著者:: Zhenning Liu, 等
出版事項: (2022-09-01)

SCMC: An Efficient Scheme for Minimizing Energy in WSNs Using a Set Cover Approach
著者:: Ahmed Redha Mahlous
出版事項: (2017-12-01)

Strengthening properties using abstraction refinement
著者:: Purandare, M, 等
出版事項: (2009)

Water rapid hardening polyurethane for minimally invasive surgery: proof-of-concept
著者:: Neo, Jordon Ting Xuan
出版事項: (2024)

Propositional proof systems : efficiency and automatizability
著者:: Alekhnovitch, Mikhail, 1978-
出版事項: (2005)

Beyond quantifier-free interpolation in extensions of presburger arithmetic
著者:: Brillout, A, 等
出版事項: (2011)

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
著者:: Brillout, A, 等
出版事項: (2011)

Reduction of acoustic mode in noise-proof cover with interference wave inducing apertures
著者:: Daisuke MUTO, 等
出版事項: (2015-06-01)

Efficient Computation of Recurrence Diameters
著者:: Kroening, D, 等
出版事項: (2003)

Efficient Consistency Proofs on a Committed Database
著者:: Ostrovsky, Rafail, 等
出版事項: (2023)

Highly insulated crawl spaces with controlled minimal ventilation – proof of concept by field measurements
著者:: Airaksinen Miimu, 等
出版事項: (2020-01-01)

Infinite Analysis, Lucky Proof, and Guaranteed Proof in Leibniz
著者:: Rodriguez-Pereyra, G, 等
出版事項: (2011)

Finding Lean Induced Cycles in Binary Hypercubes
著者:: Chebiryak, Y, 等
出版事項: (2009)

Context-aware counter abstraction.
著者:: Basler, G, 等
出版事項: (2010)

An efficient SAT encoding of circuit codes
著者:: Chebiryak, Y, 等
出版事項: (2008)

New construction of minimal (v,3,2)-coverings
著者:: Nikolić Nebojša
出版事項: (2016-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
著者:: Donaldson, A, 等
出版事項: (2012)

Efficient construction of machine-checked symbolic protocol security proofs
著者:: Meier, S, 等
出版事項: (2013)

Analysis : with an introduction to proof /
著者:: 233723 Lay, Steven R.
出版事項: (2004)

Computationally efficient error-correcting codes and holographic proofs
著者:: Spielman, Daniel Alan
出版事項: (2007)

Computationally Efficient Error-Correcting Codes and Holographic Proofs
著者:: Spielman, Daniel Alan
出版事項: (2023)

Efficient inner product arguments and their applications in range proofs
著者:: Zibo Zhou, 等
出版事項: (2023-05-01)

More efficient proof-search for sequents of temporal logic
著者:: Romas Alonderis
出版事項: (2022-12-01)

Cryptocurrencies: Miner Heterogeneity, Botnets, and Proof-of-Work Efficiency
著者:: Fabian Schär
出版事項: (2020-04-01)