2010

 back to the year overview

• Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
  Exploiting Different Strategies for the Parallelization of an SMT Solver
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer Verlag, pages: 97 - 106
  » show abstract« hide abstract
  Abstract

  In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.

2009

 back to the year overview

• Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
  Picoso - A Parallel Interval Constraint Solver
  2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, CSREA Press, pages: 473 - 479
  » show abstract« hide abstract
  Abstract

  This paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
  Challenges in Constraint-Based Analysis of Hybrid Systems
  2009 Recent Advances in Constraints, Springer, volume: 5655, pages: 51 - 65
  » show abstract« hide abstract
  Abstract

  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.

2008

 back to the year overview

• 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
  » show abstract« hide abstract
  Abstract

  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.
• Bernd Becker, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf Wimmer
  Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  2008 IEEE Int'l Conf. on Computer Design, IEEE Computer Society Press, pages: 52 - 59
  » show abstract« hide abstract
  Abstract

  Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w.\,r.\,t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210\% and a speed-up of the CPU runtime up to 390\% compared to the relation-oriented approach are achieved. But there are also relevant examples, e.\,g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300\% in terms of CPU-time, showing that both approaches are efficient for different scenarios.