research-article

Computation of minimal counterexamples by using black box techniques and symbolic methods

Authors:

Christoph Scholl,

Bernd BeckerAuthors Info & Claims

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

Pages 273 - 280

Published: 05 November 2007 Publication History

Abstract

Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals.

Here we use the concept of Black Boxes --- parts of the design with unknown behavior --- to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of 'uniform counterexamples' 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.

References

[1]

A. Sistla and E. Clarke, "The complexity of propositional linear temporal logics," Journal of the ACM, vol. 32, no. 3, pp. 733--749, 1985.

Digital Library

[2]

E. Clarke, E. Emerson, and A. Sistla, "Automatic Verification of Finite--State Concurrent Systems Using Temporal Logic Specifications," ACM Trans. on Programming Languages and Systems, vol. 8, no. 2, pp. 244--263, 1986.

Digital Library

[3]

J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 10²⁰ States and Beyond," Information and Computation, vol. 98(2), pp. 142--170, 1992.

Digital Library

[4]

K. McMillan, Symbolic Model Checking. Kluwer Academic Publisher, 1993.

Digital Library

[5]

R. Bryant, "Graph - based algorithms for Boolean function manipulation," IEEE Trans. on Comp., vol. 35, no. 8, pp. 677--691, 1986.

Digital Library

[6]

M. Ganai, A. Gupta, and P. Ashar, "Efficient SAT-based unbounded symbolic model checking using circuit cofactoring," in Int'l Conf. on Computer-Aided Design, 2004, pp. 510--517.

Digital Library

[7]

H.-J. Kang and I.-C. Park, "Sat-based unbounded symbolic model checking," IEEE Trans. on CAD, vol. 24, no. 2, pp. 129--140, February 2005.

Digital Library

[8]

F. Pigorsch, C. Scholl, and S. Disch, "Advanced unbounded model checking based on aigs, bdd sweeping, and quantifier scheduling," in Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD). IEEE Computer Society Press, Nov 2006, pp. 89--96.

Digital Library

[9]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic model checking without BDDs," in Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS, vol. 1579. Springer Verlag, 1999.

Digital Library

[10]

A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu, "Symbolic model checking using SAT procedures instead of BDDs," in Design Automation Conf., 1999.

Digital Library

[11]

M. Sheeran, S. Singh, and G. Stalmarck, "Checking Safety Properties Using Induction and a SAT-solver," in FMCAD, ser. LNCS, W. H. Jr. and S. Johnson, Eds., vol. 1954. Springer, 2000, pp. 407--420.

Digital Library

[12]

K. McMillan, "Interpolation and sat-based model checking," in Computer Aided Verification, vol. 2725. Springer Verlag, 2003, pp. 1--13.

[13]

K. Ravi and F. Somenzi, "Minimal assignments for bounded model checking," in TACAS, vol. 2988. Springer, 2004, pp. 31--45.

[14]

S. Shen, Y. Qin, and S. Li, "Minimizing counterexample with unit core extraction and incremental sat," in VMCAI, vol. 3385. Springer, 2005, pp. 298--312.

Digital Library

[15]

T. Nopper and C. Scholl, "Approximate symbolic model checking for incomplete designs," in Formal Methods in Computer-Aided Design, ser. LNCS, A. J. Hu and A. K. Martin, Eds., vol. 3312. Austin, Texas: Springer Verlag, Nov 2004, pp. 290--305.

[16]

C. Pixley, "A theory and implementation of sequential hardware equivalence," IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 11, no. 12, pp. 1469--1478, 1992.

Digital Library

[17]

T. Kropf and H.-J. Wunderlich, "A Common Approach to Test Generation and Hardware Verification Based on Temporal Logic," in Int'l Test Conf., 1991, pp. 57--66.

Digital Library

[18]

C.-J. H. Seger and R. E. Bryant, "Formal verification by symbolic evaluation of partially-ordered trajectories," Formal Methods in System Design: An International Journal, vol. 6, no. 2, pp. 147--189, March 1995.

Digital Library

[19]

C.-J. H. Seger, R. B. Jones, J. W. O'Leary, T. F. Melham, M. Aagaard, C. Barrett, and D. Syme, "An industrially effective environment for formal hardware verification." IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 24, no. 9, pp. 1381--1405, 2005.

Digital Library

[20]

R. Tzoref and O. Grumberg, "Automatic refinement and vacuity detection for symbolic trajectory evaluation." in CAV, ser. LNCS, T. Ball and R. B. Jones, Eds., vol. 4144. Springer Verlag, 2006, pp. 190--204.

Digital Library

[21]

F. Copty, A. Irron, O. Weissberg, N. P. Kropp, and G. Kamhi, "Efficient debugging in a formal verification environment," in Correct Hardware Design and Verification Methods (CHARME), ser. LNCS, T. Margaria and T. F. Melham, Eds., vol. 2144. Springer Verlag, September 2001, pp. 275--292.

Digital Library

[22]

T. Nopper and C. Scholl, "Flexible modeling of unknowns in model checking for incomplete designs," in 8. GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", April 2005.

[23]

M. Abramovici, M. Breuer, and A. Friedman, Digital Systems Testing and Testable Design. Computer Science Press, 1990.

[24]

O. Coudert, C. Berthet, and J. Madre, "Verification of synchronous sequential machines based on symbolic execution," in Automatic Verification Methods for Finite State Systems, ser. LNCS, vol. 407. Springer Verlag, 1989, pp. 365--373.

Digital Library

[25]

C. Scholl and B. Becker, "Checking equivalence for partial implementations," in Design Automation Conf., 2001, pp. 238--243.

Digital Library

[26]

M. Herbstritt, B. Becker, and C. Scholl, "Advanced SAT-techniques for bounded model checking of blackbox designs," in Proc. of Microprocessor Test and Verification Workshop (MTV). IEEE Computer Society, 2006.

Digital Library

[27]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engeneering an efficient SAT solver," in Design Automation Conf., 2001.

Digital Library

[28]

N. Een and N. Sörensson, "An extensible sat-solver," in Theory and Applications of Satisfiability Testing, 6th InternationalConference, SAT 2003. Santa Margherita Ligure, Italy, May 5--8, 2003 Selected Revised Papers, ser. Lecture Notes in Computer Science, vol. 2919. Springer, 2003, pp. 541--638.

[29]

The VIS Group, "VIS: A system for verification and synthesis," in Computer Aided Verification, ser. LNCS, vol. 1102. Springer Verlag, 1996, pp. 428--432.

Digital Library

[30]

F. Somenzi, CUDD: CU Decision Diagram Package Release 2.3.1. University of Colorado at Boulder, 2001.

[31]

T. Filkorn, "Functional extension of symbolic model checking," in CAV '91: Proceedings of the 3rd International Workshop on Computer Aided Verification. Springer, 1992, pp. 225--232.

Digital Library

[32]

P. Williams, A. Biere, E. Clarke, and A. Gupta, "Combining decision diagrams and SAT procedures for efficient symbolic model checking," in Computer Aided Verification, ser. LNCS, vol. 1855. Springer Verlag, 2000, pp. 124--138.

Digital Library

Cited By

Wimmer RHahn EHermanns HBecker B(2011)Reachability analysis for incomplete networks of Markov decision processesProceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2011.5970522(151-160)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1109/MEMCOD.2011.5970522
Miller CKupferschmid SLewis MBecker B(2010)Encoding techniques, craig interpolants and bounded model checking for incomplete designsProceedings of the 13th international conference on Theory and Applications of Satisfiability Testing10.1007/978-3-642-14186-7_17(194-208)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-14186-7_17

Computation of minimal counterexamples by using black box techniques and symbolic methods
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Learning-based black box checking for k-safety hyperproperties
Abstract
The L ∗ algorithm proposed by Angluin is a standard approach to automata learning of unknown systems that generate regular languages. Black box checking (BBC) based on the L ∗ algorithm is a promising formal verification of unknown systems. On ...
Graphical abstract

Display Omitted
Highlights
- Automata learning based black box checking algorithm for k-safety hyperproperties.
- Generation of k-bad prefix automata with L ∗ algorithm.
- Demonstration of black box checking of mobile robot path planning.
Induction in CEGAR for Detecting Counterexamples
FMCAD '07: Proceedings of the Formal Methods in Computer Aided Design

Induction has been studied in model checking for proving the validity of safety properties, i.e., showing the absence of counterexamples. To our knowledge, induction has not been used to refute safety properties. Existing algorithms including bounded ...
Shortest counterexamples for symbolic model checking of LTL with past
TACAS'05: Proceedings of the 11th international conference on Tools and Algorithms for the Construction and Analysis of Systems

Shorter counterexamples are typically easier to understand. The length of a counterexample, as reported by a model checker, depends on both the algorithm used for state space exploration and the way the property is encoded. We provide necessary and ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Sponsors

CEDA: Council on Electronic Design Automation
SIGDA: ACM Special Interest Group on Design Automation
IEEE CASS/CANDE
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Research-article

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
123
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wimmer RHahn EHermanns HBecker B(2011)Reachability analysis for incomplete networks of Markov decision processesProceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2011.5970522(151-160)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1109/MEMCOD.2011.5970522
Miller CKupferschmid SLewis MBecker B(2010)Encoding techniques, craig interpolants and bounded model checking for incomplete designsProceedings of the 13th international conference on Theory and Applications of Satisfiability Testing10.1007/978-3-642-14186-7_17(194-208)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-14186-7_17

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten