Name
Title | ||
|---|---|---|
Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae. |
Abstract | ||
|---|---|---|
Symbolic methods in computer-aided verification rely on appropriate constraint solvers. Correctness and reliability of solvers are a vital requirement in the analysis of safety-critical systems, e.g., in the automotive context. Satisfiability results of a solver can usually be checked by probing the computed solution. However, efficient validation of an uncertified unsatisfiability result for some constraint formula is nearly impossible. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-linear arithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete-continuous systems. |
Year | Venue | Field |
|---|---|---|
2009 | MBMV | Nonlinear system,Satisfiability,Correctness,Arithmetic,Mathematical proof,Boolean algebra,Solver,Mathematics,Automotive industry |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
9 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefan Kupferschmid | 1 | 72 | 7.05 |
| Tino Teige | 2 | 258 | 17.56 |
| Bernd Becker | 3 | 0 | 0.34 |
| Martin Fränzle | 4 | 786 | 61.58 |