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

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Kaiser, A, Kroening, D, Wahl, T
Rannpháirtithe:	Koutny, M
Formáid:	Conference item
Foilsithe / Cruthaithe:	Springer 2012

Míreanna comhchosúla

Lost in abstraction: monotonicity in multi-threaded programs
de réir: Kaiser, A, et al.
Foilsithe / Cruthaithe: (2016)

Lost in abstraction: monotonicity in multi-threaded programs
de réir: Kaiser, A, et al.
Foilsithe / Cruthaithe: (2014)

A widening approach to multithreaded program verification
de réir: Kaiser, A, et al.
Foilsithe / Cruthaithe: (2014)

Proof-graphs for Minimal Implicational Logic
de réir: Marcela Quispe-Cruz, et al.
Foilsithe / Cruthaithe: (2014-03-01)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2007)

Model and proof generation for heap-manipulating programs
de réir: Brain, M, et al.
Foilsithe / Cruthaithe: (2014)

Model and Proof Generation for Heap−Manipulating Programs
de réir: Brain, M, et al.
Foilsithe / Cruthaithe: (2014)

Synthesising interprocedural bit-precise termination proofs
de réir: Chen, H, et al.
Foilsithe / Cruthaithe: (2016)

A First Step Towards a Unified Proof Checker for QBF
de réir: Jussila, T, et al.
Foilsithe / Cruthaithe: (2007)

Audiomotor Integration in Minimally Conscious State: Proof of Concept!
de réir: Antonino Naro, et al.
Foilsithe / Cruthaithe: (2015-01-01)

Efficient holographic proofs
de réir: Russell, Alexander Craig
Foilsithe / Cruthaithe: (2007)

Efficient Standard of Proof
de réir: Iraj Babaei, et al.
Foilsithe / Cruthaithe: (2021-12-01)

Projective covers and minimal free resolutions
de réir: Mark A. Goddard
Foilsithe / Cruthaithe: (1996-01-01)

The minimal covering set in large tournaments
de réir: Scott, A, et al.
Foilsithe / Cruthaithe: (2012)

High-performance noise proof cover using acoustic tube
de réir: Daisuke MUTO, et al.
Foilsithe / Cruthaithe: (2014-10-01)

Super-efficient rational proofs
de réir: Azar, Pablo Daniel
Foilsithe / Cruthaithe: (2015)

Depth-efficient proofs of quantumness
de réir: Zhenning Liu, et al.
Foilsithe / Cruthaithe: (2022-09-01)

SCMC: An Efficient Scheme for Minimizing Energy in WSNs Using a Set Cover Approach
de réir: Ahmed Redha Mahlous
Foilsithe / Cruthaithe: (2017-12-01)

Strengthening properties using abstraction refinement
de réir: Purandare, M, et al.
Foilsithe / Cruthaithe: (2009)

Water rapid hardening polyurethane for minimally invasive surgery: proof-of-concept
de réir: Neo, Jordon Ting Xuan
Foilsithe / Cruthaithe: (2024)

Propositional proof systems : efficiency and automatizability
de réir: Alekhnovitch, Mikhail, 1978-
Foilsithe / Cruthaithe: (2005)

Reduction of acoustic mode in noise-proof cover with interference wave inducing apertures
de réir: Daisuke MUTO, et al.
Foilsithe / Cruthaithe: (2015-06-01)

Beyond quantifier-free interpolation in extensions of presburger arithmetic
de réir: Brillout, A, et al.
Foilsithe / Cruthaithe: (2011)

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
de réir: Brillout, A, et al.
Foilsithe / Cruthaithe: (2011)

Highly insulated crawl spaces with controlled minimal ventilation – proof of concept by field measurements
de réir: Airaksinen Miimu, et al.
Foilsithe / Cruthaithe: (2020-01-01)

Efficient Consistency Proofs on a Committed Database
de réir: Ostrovsky, Rafail, et al.
Foilsithe / Cruthaithe: (2023)

Efficient Computation of Recurrence Diameters
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2003)

Infinite Analysis, Lucky Proof, and Guaranteed Proof in Leibniz
de réir: Rodriguez-Pereyra, G, et al.
Foilsithe / Cruthaithe: (2011)

New construction of minimal (v,3,2)-coverings
de réir: Nikolić Nebojša
Foilsithe / Cruthaithe: (2016-01-01)

Finding Lean Induced Cycles in Binary Hypercubes
de réir: Chebiryak, Y, et al.
Foilsithe / Cruthaithe: (2009)

Context-aware counter abstraction.
de réir: Basler, G, et al.
Foilsithe / Cruthaithe: (2010)

An efficient SAT encoding of circuit codes
de réir: Chebiryak, Y, et al.
Foilsithe / Cruthaithe: (2008)

Efficient construction of machine-checked symbolic protocol security proofs
de réir: Meier, S, et al.
Foilsithe / Cruthaithe: (2013)

Counterexample-guided abstraction refinement for symmetric concurrent programs
de réir: Donaldson, A, et al.
Foilsithe / Cruthaithe: (2012)

Analysis : with an introduction to proof /
de réir: 233723 Lay, Steven R.
Foilsithe / Cruthaithe: (2004)

Computationally efficient error-correcting codes and holographic proofs
de réir: Spielman, Daniel Alan
Foilsithe / Cruthaithe: (2007)

Computationally Efficient Error-Correcting Codes and Holographic Proofs
de réir: Spielman, Daniel Alan
Foilsithe / Cruthaithe: (2023)

Efficient inner product arguments and their applications in range proofs
de réir: Zibo Zhou, et al.
Foilsithe / Cruthaithe: (2023-05-01)

More efficient proof-search for sequents of temporal logic
de réir: Romas Alonderis
Foilsithe / Cruthaithe: (2022-12-01)

Cryptocurrencies: Miner Heterogeneity, Botnets, and Proof-of-Work Efficiency
de réir: Fabian Schär
Foilsithe / Cruthaithe: (2020-04-01)