Approximation Refinement for Interpolation−Based Model Checking

Approximation Refinement for Interpolation−Based Model Checking

Показать другие версии (1)

Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from the SAT solver to progress. If an over-approximation leads to a satisfiable formula, the co...

Полное описание

Библиографические подробности
Главные авторы:	D'Silva, V, Purandare, M, Kroening, D
Другие авторы:	Logozzo, F
Формат:	Conference item
Опубликовано:	Springer 2008

Схожие документы

Approximation Refinement for Interpolation−Based Model Checking
по: D'Silva, V, и др.
Опубликовано: (2008)

Coverage in interpolation-based model checking
по: Chockler, H, и др.
Опубликовано: (2010)

Computing mutation coverage in interpolation-based model checking
по: Chockler, H, и др.
Опубликовано: (2012)

Interpolant Strength
по: D'Silva, V, и др.
Опубликовано: (2010)

Restructuring Resolution Refutations for Interpolation
по: D'Silva, V, и др.
Опубликовано: (2008)

Computing Over−Approximations with Bounded Model Checking
по: Kroening, D
Опубликовано: (2006)

Computing over-approximations with bounded model checking
по: Kroening, D
Опубликовано: (2006)

Formalizing and checking thread refinement for data-race-free execution models
по: Poetzl, D, и др.
Опубликовано: (2016)

Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
по: Kroening, D, и др.
Опубликовано: (2016)

Strengthening properties using abstraction refinement
по: Purandare, M, и др.
Опубликовано: (2009)

Interpolation−based verification of floating−point programs with abstract CDCL
по: Brain, M, и др.
Опубликовано: (2013)

Interpolation-based verification of floating-point programs with abstract CDCL
по: Brain, M, и др.
Опубликовано: (2013)

Applying models of spatial interpolation for the approximation of responses in the refinement of parameters of finite element models
по: Pikhalov Anatoly, и др.
Опубликовано: (2018-01-01)

Propositional Interpolation and Abstract Interpretation
по: D'Silva, V
Опубликовано: (2010)

More effective interpolations in software model checking
по: Tian, C, и др.
Опубликовано: (2017)

Interpolation and approximation/
по: Davis, Philip J., 1923-
Опубликовано: (1975)

Abstraction refinement for large scale model checking /
по: 405051 Wang, Chao, и др.
Опубликовано: (2006)

Model Checking with Abstraction for Web Services
по: Sharygina, N, и др.
Опубликовано: (2007)

ACSAR: Software Model Checking with Transfinite Refinement
по: Seghir, M, и др.
Опубликовано: (2007)

Improving Bounded Model Checking Exploiting Interpolation-Based Learning and Strengthening
по: Gianpiero Cabodi, и др.
Опубликовано: (2024-01-01)

Preface: Special Issue on Interpolation
по: Kroening, D, и др.
Опубликовано: (2016)

Refinement checking for privacy policies.
по: Papanikolaou, N, и др.
Опубликовано: (2012)

Refinement checking for privacy policies
по: Papanikolaou, N, и др.
Опубликовано: (2012)

Rational approximation and interpolation /
по: Varga, Richard S., и др.
Опубликовано: (1984)

Race analysis for systemC using model checking
по: Blanc, N, и др.
Опубликовано: (2010)

Interpolant-Based Transition Relation Approximation
по: Ranjit Jhala, и др.
Опубликовано: (2007-11-01)

Refinement Checking for Privacy Policies
по: Goldsmith, S
Опубликовано: (2011)

Refinement Checking for Privacy Policies
по: Goldsmith, S
Опубликовано: (2011)

Lifting Propositional Interpolants to the Word−Level
по: Kroening, D, и др.
Опубликовано: (2007)

Symbolic model checking for asynchronous Boolean programs
по: Cook, B, и др.
Опубликовано: (2005)

Property-driven fence insertion using reorder bounded model checking
по: Joshi, S, и др.
Опубликовано: (2015)

Property-Driven Fence Insertion using Reorder Bounded Model Checking
по: Joshi, S, и др.
Опубликовано: (2015)

Proving safety with trace automata and bounded model checking
по: Kroening, D, и др.
Опубликовано: (2015)

Computational challenges in bounded model checking
по: Clarke, E, и др.
Опубликовано: (2005)

Completeness and Complexity of Bounded Model Checking
по: Clarke, E, и др.
Опубликовано: (2004)

Computational challenges in bounded model checking.
по: Clarke, E, и др.
Опубликовано: (2005)

Computational Challenges in Bounded Model Checking
по: Clarke, E, и др.
Опубликовано: (2015)

DRVI: Dual Refinement for Video Interpolation
по: Xuanyi Wu, и др.
Опубликовано: (2021-01-01)

Towards automated bounded model checking of API implementations
по: Neville, D, и др.
Опубликовано: (2016)

Model Checking Concurrent Linux Device Drivers
по: Witkowski, T, и др.
Опубликовано: (2007)