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

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	Kaiser, A, Kroening, D, Wahl, T
Awduron Eraill:	Koutny, M
Fformat:	Conference item
Cyhoeddwyd:	Springer 2012

Eitemau Tebyg

Lost in abstraction: monotonicity in multi-threaded programs
gan: Kaiser, A, et al.
Cyhoeddwyd: (2016)

Lost in abstraction: monotonicity in multi-threaded programs
gan: Kaiser, A, et al.
Cyhoeddwyd: (2014)

A widening approach to multithreaded program verification
gan: Kaiser, A, et al.
Cyhoeddwyd: (2014)

Proof-graphs for Minimal Implicational Logic
gan: Marcela Quispe-Cruz, et al.
Cyhoeddwyd: (2014-03-01)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
gan: Kroening, D, et al.
Cyhoeddwyd: (2007)

Model and proof generation for heap-manipulating programs
gan: Brain, M, et al.
Cyhoeddwyd: (2014)

Model and Proof Generation for Heap−Manipulating Programs
gan: Brain, M, et al.
Cyhoeddwyd: (2014)

Synthesising interprocedural bit-precise termination proofs
gan: Chen, H, et al.
Cyhoeddwyd: (2016)

A First Step Towards a Unified Proof Checker for QBF
gan: Jussila, T, et al.
Cyhoeddwyd: (2007)

Audiomotor Integration in Minimally Conscious State: Proof of Concept!
gan: Antonino Naro, et al.
Cyhoeddwyd: (2015-01-01)

Efficient holographic proofs
gan: Russell, Alexander Craig
Cyhoeddwyd: (2007)

Efficient Standard of Proof
gan: Iraj Babaei, et al.
Cyhoeddwyd: (2021-12-01)

Projective covers and minimal free resolutions
gan: Mark A. Goddard
Cyhoeddwyd: (1996-01-01)

The minimal covering set in large tournaments
gan: Scott, A, et al.
Cyhoeddwyd: (2012)

High-performance noise proof cover using acoustic tube
gan: Daisuke MUTO, et al.
Cyhoeddwyd: (2014-10-01)

Super-efficient rational proofs
gan: Azar, Pablo Daniel
Cyhoeddwyd: (2015)

Depth-efficient proofs of quantumness
gan: Zhenning Liu, et al.
Cyhoeddwyd: (2022-09-01)

SCMC: An Efficient Scheme for Minimizing Energy in WSNs Using a Set Cover Approach
gan: Ahmed Redha Mahlous
Cyhoeddwyd: (2017-12-01)

Strengthening properties using abstraction refinement
gan: Purandare, M, et al.
Cyhoeddwyd: (2009)

Water rapid hardening polyurethane for minimally invasive surgery: proof-of-concept
gan: Neo, Jordon Ting Xuan
Cyhoeddwyd: (2024)

Propositional proof systems : efficiency and automatizability
gan: Alekhnovitch, Mikhail, 1978-
Cyhoeddwyd: (2005)

Reduction of acoustic mode in noise-proof cover with interference wave inducing apertures
gan: Daisuke MUTO, et al.
Cyhoeddwyd: (2015-06-01)

Beyond quantifier-free interpolation in extensions of presburger arithmetic
gan: Brillout, A, et al.
Cyhoeddwyd: (2011)

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
gan: Brillout, A, et al.
Cyhoeddwyd: (2011)

Highly insulated crawl spaces with controlled minimal ventilation – proof of concept by field measurements
gan: Airaksinen Miimu, et al.
Cyhoeddwyd: (2020-01-01)

Efficient Consistency Proofs on a Committed Database
gan: Ostrovsky, Rafail, et al.
Cyhoeddwyd: (2023)

Efficient Computation of Recurrence Diameters
gan: Kroening, D, et al.
Cyhoeddwyd: (2003)

Infinite Analysis, Lucky Proof, and Guaranteed Proof in Leibniz
gan: Rodriguez-Pereyra, G, et al.
Cyhoeddwyd: (2011)

New construction of minimal (v,3,2)-coverings
gan: Nikolić Nebojša
Cyhoeddwyd: (2016-01-01)

Finding Lean Induced Cycles in Binary Hypercubes
gan: Chebiryak, Y, et al.
Cyhoeddwyd: (2009)

Context-aware counter abstraction.
gan: Basler, G, et al.
Cyhoeddwyd: (2010)

An efficient SAT encoding of circuit codes
gan: Chebiryak, Y, et al.
Cyhoeddwyd: (2008)

Efficient construction of machine-checked symbolic protocol security proofs
gan: Meier, S, et al.
Cyhoeddwyd: (2013)

Counterexample-guided abstraction refinement for symmetric concurrent programs
gan: Donaldson, A, et al.
Cyhoeddwyd: (2012)

Analysis : with an introduction to proof /
gan: 233723 Lay, Steven R.
Cyhoeddwyd: (2004)

Computationally efficient error-correcting codes and holographic proofs
gan: Spielman, Daniel Alan
Cyhoeddwyd: (2007)

Computationally Efficient Error-Correcting Codes and Holographic Proofs
gan: Spielman, Daniel Alan
Cyhoeddwyd: (2023)

Efficient inner product arguments and their applications in range proofs
gan: Zibo Zhou, et al.
Cyhoeddwyd: (2023-05-01)

More efficient proof-search for sequents of temporal logic
gan: Romas Alonderis
Cyhoeddwyd: (2022-12-01)

Cryptocurrencies: Miner Heterogeneity, Botnets, and Proof-of-Work Efficiency
gan: Fabian Schär
Cyhoeddwyd: (2020-04-01)