2013

 back to the year overview

• Tobias Nopper, Christoph Scholl
  Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns
  2013 IEEE Trans. Computers, volume: 62, issue: 6, pages: 1234 - 1254

2010

 back to the year overview

• Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph Scholl
  SAT Modulo BDD – A Combined Verification Approach for Incomplete Designs
  2010 MBMV, Fraunhofer Verlag, pages: 107 - 116

2009

 back to the year overview

• Christian Miller, Tobias Nopper, Christoph Scholl
  Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions
  2009 MBMV, pages: 87 - 96

2008

 back to the year overview

• 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 ICCD, IEEE, pages: 52 - 59

2007

 back to the year overview

• Tobias Nopper, Christoph Scholl, Bernd Becker
  Computation of Minimal Counterexamples by Using Black Box Techniques and Symbolic Methods
  2007 San Jose International Conference on Computer Aided Design (ICCAD), IEEE Computer Society Press
  » show abstract« hide abstract
  Abstract

  to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.
• Tobias Nopper, Christoph Scholl
  Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns
  SFB/TR 14 AVACS Technical Report, issue: 31, 2007
• Tobias Nopper, Christoph Scholl
  tion for Incomplete Designs
  2007 Erlangen GI/ITG/GMM Workshop“Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Aachen, pages: 193 - 202
  » show abstract« hide abstract
  Abstract

  Counterexample generation is a crucial task for error diagnosis and debugging of sequential circuits.The simpler a counterexample is - i.e. more general and fewer assigned input values - the better it can be understood by humans. We will use the concept of Black Boxes - parts of the design with unknown behavior - to mask out components for counterexample computation. By this, the resulting counterexample will argue about a reduced number of components in the system in order to facilitate the task of understanding and correcting the error effect.

2005

 back to the year overview

• Tobias Nopper, Christoph Scholl
  Flexible Modeling of Unknowns in Model Checking for Incomplete Designs
  2005 8. GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  We consider the problem of checking whether an incomplete design (i.e. a design containing so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions.In this paper we extend a method based on a series of approximate, yet sound algorithms to prove or disprove CTL properties for incomplete designs. Each algorithm in the previous approach was able to model the effect of the unknown information at the outputs of the Black Boxes at a different level of accuracy (leading to different requirements for computational resources). In this paper we present a novel approach which is able to use different methods for modeling unknowns at the outputs of different Black Boxes within a single model checking run. This permits us to handle less relevant Black Boxes (in terms of the CTL formula) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods.Finally we give a series of experimental results demonstrating the effectiveness and feasibility of the new method.

2004

 back to the year overview

• Tobias Nopper, Christoph Scholl
  Approximate Symbolic Model Checking for Incomplete Designs
  2004 Austin, Texas Formal Methods in Computer-Aided Design, Springer Verlag, volume: 3312, pages: 290 - 305
  » show abstract« hide abstract
  Abstract

  We consider the problem of checking whether an incomplete design can still be extended to a complete design satisfying a given CTL formula and whether the property is satisfied for all possible extensions. Motivated by the fact that well-known model checkers like SMV or VIS produce incorrect results when handling unknowns by using the programs’ non-deterministic signals, we present a series of approximate, yet sound algorithms to process incomplete designs with increasing quality and computational resources. Finally we give a series of experimental results demonstrating the effectiveness and feasibility of the presented methods.
• Tobias Nopper, Christoph Scholl
  Approximate Symbolic Model Checking of Incomplete Designs
  2004 13th Int’l Workshop on Logic Synth., volume: 13, pages: 377 - 384
  » show abstract« hide abstract
  Abstract

  We consider the problem of checking whether an incomplete design can still be extended to a complete design satisfying a given CTL formula and whether the property is satisfied for all possible extensions.Motivated by the fact that well-known model checkers like SMV or VIS produce incorrect results when handling unknowns by using the programs’ non-deterministic signals, we present a series of approximate, yet sound algorithms to process incomplete designs with increasing quality and computational resources.Finally we give a series of experimental results demonstrating theeffectiveness and feasibility of the presented methods.
• Tobias Nopper, Christoph Scholl
  Symbolic Model Checking of Incomplete Designs
  Technical Report Albert-Ludwigs-University, issue: 201, 2004