Name
Abstract | ||
|---|---|---|
Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance 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. This is in general not the case for un-satisfiability results. 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. Furthermore, we test our approach by enhancing the iSAT constraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing the effectiveness of our techniques are given. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/DDECS.2011.5783131 | Design and Diagnostics of Electronic Circuits & Systems |
Keywords | Field | DocType |
Boolean functions,computability,constraint handling,continuous systems,cryptography,discrete systems,formal verification,safety-critical software,symbol manipulation,theorem proving,automotive context,certification method,computer-aided verification,constraint solvers,hybrid discrete/continuous systems,iSAT constraint solver,mixed Boolean arithemetic constraint formula,nonlinear arithmetic constraint formulae,nonlinear arithmetic constraints,proof certificates,safety-critical systems,symbolic methods,un-satisfiability results,unsatisfiability proofs | Boolean function,Computer science,Correctness,Satisfiability,Arithmetic,Algorithm,Constraint satisfaction problem,Theoretical computer science,Mathematical proof,Boolean algebra,Solver,Formal verification | Conference |
ISSN | ISBN | Citations |
2334-3133 | 978-1-4244-9755-3 | 4 |
PageRank | References | Authors |
0.45 | 11 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefan Kupferschmid | 1 | 72 | 7.05 |
| Bernd Becker | 2 | 855 | 73.74 |
| Tino Teige | 3 | 258 | 17.56 |
| Martin Franzle | 4 | 26 | 2.69 |