Satisfiability solvers are static analysers

Satisfiability solvers are static analysers

Show other versions (1)

This paper shows that several propositional satisfiability algorithms compute approximations of fixed points using lattice-based abstractions. The Boolean Constraint Propagation algorithm (bcp) is a greatest fixed point computation over a lattice of partial assignments. The original algorithm of Dav...

Bibliografske podrobnosti
Main Authors:	D'Silva, V, Haller, L, Kroening, D
Drugi avtorji:	Miné, A
Format:	Conference item
Izdano:	Springer 2012

Podobne knjige/članki

Satisfiability Solvers are Static Analysers
od: D'Silva, V, et al.
Izdano: (2012)

Optimization of Boolean satisfiability solver by caching intermediate results
od: S. Vartanov, et al.
Izdano: (2018-10-01)

A framework for Satisfiability Modulo Theories.
od: Kroening, D, et al.
Izdano: (2009)

Bit‐level evaluation of piccolo block cipher by satisfiability problem solver
od: Shion Utsumi, et al.
Izdano: (2023-07-01)

Verifying the structure and behavior in UML/OCL models using satisfiability solvers
od: Nils Przigoda, et al.
Izdano: (2016-11-01)

Abstract conflict driven learning.
od: D'Silva, V, et al.
Izdano: (2013)

Abstract Conflict Driven Learning
od: D'Silva, V, et al.
Izdano: (2013)

Abstract Satisfaction
od: D'Silva, V, et al.
Izdano: (2014)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
od: Kroening, D, et al.
Izdano: (2004)

Leveraging Satisfiability Modulo Theory Solvers for Verification of Neural Networks in Predictive Maintenance Applications
od: Dario Guidotti, et al.
Izdano: (2023-07-01)

Strengthening Induction−Based Race Checking with Lightweight Static Analysis
od: Donaldson, A, et al.
Izdano: (2011)

Numeric bounds analysis with conflict-driven learning
od: D'Silva, V, et al.
Izdano: (2012)

Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers.
od: Zinovik, I, et al.
Izdano: (2008)

Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT−Solvers
od: Zinovik, I, et al.
Izdano: (2015)

An Abstract Interpretation of DPLL(T)
od: Brain, M, et al.
Izdano: (2013)

Deciding floating−point logic with abstract conflict driven clause learning
od: Brain, M, et al.
Izdano: (2013)

An abstract interpretation of DPLL(T)
od: Brain, M, et al.
Izdano: (2013)

Interpolation−based verification of floating−point programs with abstract CDCL
od: Brain, M, et al.
Izdano: (2013)

Interpolation-based verification of floating-point programs with abstract CDCL
od: Brain, M, et al.
Izdano: (2013)

Satisfiability checking meets symbolic computation
od: Abraham, E, et al.
Izdano: (2016)

Relieving capacity limits on FPGA−based SAT−solvers
od: Haller, L, et al.
Izdano: (2010)

Abstraction of Syntax
od: D'Silva, V, et al.
Izdano: (2013)

Fixed points for multi-cycle path detection
od: D'Silva, V, et al.
Izdano: (2009)

Fixed Points in Multi−Cycle Path Detection
od: D'Silva, V, et al.
Izdano: (2015)

A SAT Solver for Circuits Based on the Tableau Method
od: Egly, U, et al.
Izdano: (2010)

Satisfiability
od: Hoare, C
Izdano: (2015)

SC2: Satisfiability checking meets symbolic computation
od: Ábrahám, E, et al.
Izdano: (2016)

2 Step design for sandwich panel structure satisfying with restriction of static stress and eigen frequency
od: Shin SASAKI, et al.
Izdano: (2024-02-01)

Approximation Refinement for Interpolation−Based Model Checking
od: D'Silva, V, et al.
Izdano: (2008)

Approximation Refinement for Interpolation−Based Model Checking
od: D'Silva, V, et al.
Izdano: (2008)

A survey of automated techniques for formal software verification
od: D'Silva, V, et al.
Izdano: (2008)

A Survey of Automated Techniques for Formal Software Verification.
od: D'Silva, V, et al.
Izdano: (2008)

A Survey of Automated Techniques for Formal Software Verification
od: D'Silva, V, et al.
Izdano: (2008)

Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
od: Jakub Michaliszyn, et al.
Izdano: (2012-10-01)

Satisfied with dissatisfaction?
od: Key, A, et al.
Izdano: (1999)

Satisfying journey!
od: Balaji Manohar
Izdano: (2015-01-01)

Parents’ Perceptions of School Support During COVID-19: What Satisfies Parents?
od: Teresa Haller, et al.
Izdano: (2021-09-01)

Static Analysis to Enhance the Power of Model Checking for Concurrent Software
od: Clarke, E, et al.
Izdano: (2007)

The need for security of «the person consuming»: the ways to satisfy
od: D. V. Tombu
Izdano: (2015-10-01)

Sound static deadlock analysis for C/Pthreads
od: Kroening, D, et al.
Izdano: (2016)