2013

 nach oben zur Jahresübersicht

• Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker
  Applying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits
  2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  such sequences depending on the number of controllable flip-flops.
• Karsten Scheibler, Stefan Kupferschmid, Bernd Becker
  Recent Improvements in the SMT Solver iSAT
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Over the past decades embedded systems have become more and more complex. Furthermore, besides digital components they now often contain additional analog parts -- making them to embedded hybrid systems. If such systems are used in safety critical environments, a formal correctness proof is highly desirable. The SMT solver iSAT aims at solving boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. To keep up with the ever increasing complexity of these systems we present recent improvements in various parts of iSAT. Experiments demonstrate that iSAT with all the presented improvements integrated typically gains a speedup between one and two orders of magnitude.
• Der Andere Verlag, Seite: 266
  Über Craigsche Interpolation und deren Anwendung in der formalen Modellprüfung
  ISBN: 978-3-86247-411-0
  Stefan Kupferschmid

2012

 nach oben zur Jahresübersicht

• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Sudhakar M. Reddy, Bernd Becker
  Analysis of Reachable Sensitisable Paths in Sequential Circuits with SAT and Craig Interpolation
  2012 Int'l Conf. on VLSI Design
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Test pattern generation for sequential circuits benefits from scanning strategies as these allow the justification of arbitrary circuit states. However, some of these states may be unreachable during normal operation. This results in non-functional operation which may lead to abnormal circuit behaviour and result in over-testing. In this work, we present a versatile approach that combines a highly adaptable SAT-based path-enumeration algorithm with a model-checking solver for invariant properties that relies on the theory of Craig interpolants to prove the unreachability of circuit states. The method enumerates a set of longest sensitisable paths and yields test sequences of minimal length able to sensitise the found paths starting from a given circuit state. We present detailed experimental results on the reach ability of sensitisable paths in ITC 99 circuits.
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker
  Functional Justification in Sequential Circuits using SAT and Craig Interpolation
  2012 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker
  Functional Test of Small-Delay Faults using SAT and Craig Interpolation
  2012 Int'l Test Conf., Seiten: 1 - 8
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present SATSEQ, a timing-aware ATPG system for small-delay faults in non-scan circuits. The tool identifies the longest paths suitable for functional fault propagation and generates the shortest possible sub-sequences per fault. Based on advanced model-checking techniques, SATSEQ provides detection of small-delay faults through the longest functional paths. All test sequences start at the circuit's initial state; therefore, overtesting is avoided. Moreover, potential invalidation of the fault detection is taken into account. Experimental results show high detection and better performance than scan testing in terms of test application time and overtesting-avoidance.

2011

 nach oben zur Jahresübersicht

• Stefan Kupferschmid, Bernd Becker
  Craig interpolation in the presence of non-linear constraints
  2011 Formal Modeling and Analysis of Timed Systems, Springer, Seiten: 240 - 255
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  An increasing number of applications in particular in the verification area leverages Craig interpolation. Craig interpolants (CIs) can be computed for many different theories such as: propositional logic, linear inequalities over the reals, and the combination of the preceding theories with uninterpreted function symbols. To the best of our knowledge all previous tools that provide CIs are addressing decidable theories. With this paper we make Craig interpolation available for an in general undecidable theory that contains Boolean combinations of linear and non-linear constraints including transcendental functions like $\sin(\cdot)$ and $\cos(\cdot)$. Such formulae arise e.g.~during the verification of hybrid systems. We show how the construction rules for CIs can be extended to handle non-linear constraints. To do so, an existing SMT solver based on a close integration of SAT and Interval Constraint Propagation is enhanced to construct CIs on the basis of proof trees. We provide first experimental results demonstrating the usefulness of our approach: With the help of Craig interpolation we succeed in proving safety in cases where the basic solver could not provide a complete answer. Furthermore, we point out the (heuristic) decisions we made to obtain suitable CIs and discuss further possibilities to increase the flexibility of the CI construction.
• Stefan Kupferschmid, Bernd Becker
  Craigsche Interpolation für Boolesche Kombinationen linearer und nichtlinearer Ungleichungen
  2011 OFFIS-Institut für Informatik, Seiten: 279 - 288
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Die vorliegende Arbeit behandelt die Berechnung Craigscher Interpolanten für beliebige boolesche Kombinationen linearer und nichtlinearer Gleichungen, einschließlich transzendenter Funktionen wie sin(x) und cos(x). Craigsche Interpolanten sind in der computergestützten Verifikation weit verbreitet und können für viele verschiedene Theorien berechnet werden, zum Beispiel: Aussagenlogik, lineare Arithmetik über rationale Zahlen sowie die Theorie mit uninterpretierten Funktionsymbolen. Nach bestem Wissen berechnen alle uns bekannten Interpolationsprogramme Craigsche Interpolanten für entscheidbare Theorien. In dieser Arbeit stellen wir einen Ansatz vor, der für eine im Allgemeinem nicht entscheidbare Theorie Craigsche Interpolanten berechnen kann. Wir erlauben neben linearen und nichtlinearen Gleichungen auch transzendente Funktionen. Solche Formeln entstehen bei der Analyse und Verifikation hybrider Systeme. Der in dieser Arbeit vorgestellte Ansatz wurde mithilfe des Sat-Modulo-Theorie Solvers iSAT implementiert. Erste Ergebnisse zeigen, dass Craigsche Interpolanten bei der Verifikation solcher Systeme erfolgreich eingesetzt werden können.
• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
  Incremental preprocessing methods for use in BMC
  2011 Formal Methods in System Design, Band: 39, Seiten: 185 - 204
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  . Unfortunately, many preprocessing techniques such as variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be integrated into other SAT based BMC tools to achieve similar speedups.
• Ernst Althaus, Bernd Becker, Daniel Dumitriu, Stefan Kupferschmid
  Integration of an LP solver into interval constraint propagation
  2011 Int'l Conf. on Combinatorial optimization and applications, Springer, Seiten: 343 - 356
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper describes the integration of an LP solver into iSAT, a Satisfiability Modulo Theories solver that can solve Boolean combinations of linear and nonlinear constraints. iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation allowing it to reason about linear and nonlinear constraints. As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT.
• Stefan Kupferschmid, Bernd Becker, Tino Teige, Martin Fränzle
  Proof Certificates and Non-linear Arithmetic Constraints
  2011 IEEE Design and Diagnostics of Electronic Circuits and Systems, Seiten: 429 - 434
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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. Satisfiabilityresults of a solver can usually be checked by probing the computed solution. This isin general not the case for unsatisfiability results. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-lineararithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete/continuous systems. Furthermore, we test our approach by enhancing the iSATconstraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing theeffectiveness of our techniques are given.
• Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach
  Superposition modulo non-linear arithmetic
  2011 Int'l Symp. on Frontiers of Combining Systems, Springer, Seiten: 119 - 134
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable.Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, resulting in ``unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of ``unknown'' answers.The resulting approach is implemented as SUP(NLA) by a system combination of SPASS\ and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that SPASS(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.

2010

 nach oben zur Jahresübersicht

• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
  Incremental Preprocessing Methods for use in BMC
  2010 Int'l Workshop on Hardware Verification
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). However, modern solvers depend on advanced preprocessing procedures to obtain high levels of performance. Unfortunately,many preprocessing techniques such as a variable and (blocked) clauseelimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver onboth SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantagethat Craig interpolation was able to find the fixed point sooner,reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be extended to other SAT based BMC tools to achieve similar speedups.
• Christian Miller, Stefan Kupferschmid, Bernd Becker
  Exploiting Craig Interpolants in Bounded Model Checking for Incomplete Designs
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Band: 13, Seiten: 77 - 86
• Christian Miller, Stefan Kupferschmid, Matthew Lewis, Bernd Becker
  Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
  2010 Theory and Applications of Satisfiability Testing, Springer, Seiten: 194 - 208
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper focuses on bounded invariant checking for partially specified circuits – designs containing so-called blackboxes – using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is fast, but rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the Craig interpolant or unsat-core can be used to determine heuristically which blackbox outputs to model in a more precise way. We then compare 01X, QBF and multiple hybrid modeling methods. Finally, our total workflow along with multiple state-of-the-art QBF-solvers are shown to perform well on a range of industrial blackbox circuit problems.

2009

 nach oben zur Jahresübersicht

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  2009 Tools and Algorithms for the Construction and Analysis of Systems, Springer, Band: 5505, Seiten: 383 - 397
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a method which computes optimized representationsfor non-convex polyhedra. Our method detects so-called redundantlinear constraints in these representations by using an incremental SMT(Satisfiability Modulo Theories) solver and then removes the redundantconstraints based on Craig interpolation. The approach is motivated byapplications in the context of model checking for Linear Hybrid Automata.Basically, it can be seen as an optimization method for formulasincluding arbitrary boolean combinations of linear constraints andboolean variables. We show that our method provides an essential stepmaking quantifier elimination for linear arithmetic much more efficient.Experimental results clearly show the advantages of our approach incomparison to state-of-the-art solvers.
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
  Challenges in Constraint-Based Analysis of Hybrid Systems
  2009 Recent Advances in Constraints, Springer, Band: 5655, Seiten: 51 - 65
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the analysis of hybrid discrete-continuous systems, rich arithmeticconstraint formulae with complex Boolean structure arise naturally. The iSATalgorithm, a solver for such formulae, is aimed at bounded model checking ofhybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhancethe iSAT algorithm. First, we propose an extension of iSAT to directly handleordinary differential equations as constraints. Second, we outline the recentlyintroduced generalization of the iSAT algorithm to deal with probabilistichybrid systems and some open research issues in that context. Third, wepresent ideas on how to move from bounded to unbounded model checking by usingthe concept of interpolation. Finally, we discuss the adaption of someparallelization techniques to the iSAT case, which will hopefully lead toperformance gains in the future.By presenting these open research questions, this paper aims at fosteringdiscussions on these extensions of constraint solving.
• Stefan Kupferschmid, Tino Teige, Bernd Becker, Martin Fränzle
  Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae
  2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 27 - 36
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Symbolic methods in computer-aidedverification rely on appropriate constraint solvers. Correctness and reliabilityof solvers are a vital requirement in the analysis of safety-critical systems,e.g., in the automotive context. Satisfiability results of a solver can usuallybe checked by probing the computed solution. However, efficient validation of anuncertified unsatisfiability result for some constraint formula is nearlyimpossible. In this paper, we propose a certification method for unsatisfiability resultsfor mixed Boolean and non-linear arithmetic constraint formulae. Such formulaearise in the analysis of hybrid discrete-continuous systems.

2008

 nach oben zur Jahresübersicht

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra
  2008 Int'l Workshop on Satisfiability Modulo Theories, Seiten: 18 - 26
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
  Challenges in Constraint-based Analysis of Hybrid Systems
  2008 ERCIM Workshop on Constraint Solving and Constraint Logic Programming
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the analysis of hybrid discrete-continuous systems, rich arithmeticconstraint formulae with complex Boolean structure arise naturally. The iSATalgorithm, a solver for such formulae, is aimed at bounded model checking ofhybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose anextension of iSAT to directly handleordinary differential equations as constraints. Second, we outline the recentlyintroduced generalization of the iSAT algorithm to deal with probabilistichybrid systems and some open research issues in that context. Third, wepresent ideas on how to move from bounded to unbounded model checking by usingthe concept of interpolation. Finally, we discuss the adaption of someparallelization techniques to the iSAT case, which will hopefully lead toperformance gains in the future.By presenting these open research questions, this paper aims at fosteringdiscussions on these extensions of constraint solving.