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

Fuld beskrivelse

Bibliografiske detaljer
Main Authors:	Kaiser, A, Kroening, D, Wahl, T
Andre forfattere:	Koutny, M
Format:	Conference item
Udgivet:	Springer 2012

Lignende værker

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

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

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

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

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

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

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

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

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

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

Efficient holographic proofs
af: Russell, Alexander Craig
Udgivet: (2007)

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

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

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

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

Super-efficient rational proofs
af: Azar, Pablo Daniel
Udgivet: (2015)

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

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

Strengthening properties using abstraction refinement
af: Purandare, M, et al.
Udgivet: (2009)

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

Propositional proof systems : efficiency and automatizability
af: Alekhnovitch, Mikhail, 1978-
Udgivet: (2005)

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

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

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

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

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

Efficient Computation of Recurrence Diameters
af: Kroening, D, et al.
Udgivet: (2003)

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

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

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

Context-aware counter abstraction.
af: Basler, G, et al.
Udgivet: (2010)

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

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

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

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

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

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

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

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

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