Abstract
We discuss how to combine 01X-logic and quantified boolean formulas (QBF) within a homogeneous SAT/QBF-framework in the context of bounded model checking of blackbox designs. The proposed combination allows a flexible handling of blackboxes w.r.t. computational resources. Preliminary results show the scalability of the approach.
This work was partly supported by the German Research Council (DFG) as part of SFB/TR 14 AVACS “Automatic Verification and Analysis of Complex Systems” (www.avacs.org).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58 (2003)
Herbstritt, M., Becker, B., Scholl, C.: Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs. In: Proc. of MTV, pp. 37–44. IEEE CS, Los Alamitos (2006)
Herbstritt, M., Becker, B.: On SAT-based Bounded Invariant Checking of Blackbox Designs. In: Proc. of MTV, pp. 23–28. IEEE CS, Los Alamitos (2005)
Jain, A., et al.: Testing, Verification, and Diagnosis in the Presence of Unknowns. In: VLSI Test Symp., pp. 263–269 (2000)
Nopper, T., Scholl, C.: Flexible modeling of unknowns in model checking for incomplete designs. In: GI/ITG/GMM Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (2005)
Brand, D.: Verification of large synthesized designs. In: Proc. of ICCAD (1993)
Tseitin, G.: On the complexity of derivations in propositional calculus. Studies in Constructive Mathematics and Mathematical Logics (1968)
Marques-Silva, J., Sakallah, K.: Boolean Satisfiability in Electronic Design Automation. In: Proc. of DAC, pp. 675–680 (2000)
Marques-Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. on Comp. 48(5), 506–521 (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engeneering an Efficient SAT Solver. In: Proc. of DAC (2001)
Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving. In: Proc. of ASP-DAC (2007)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 201–213. Springer, Heidelberg (2004)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)
Narizzano, M., Pulina, L., Tacchella, A.: QBF Evaluation 2006 (2006) [2006-08-02], Available on-line at www.qbflib.org/qbfeval
The VIS Group: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herbstritt, M., Becker, B. (2007). On Combining 01X-Logic and QBF. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds) Computer Aided Systems Theory – EUROCAST 2007. EUROCAST 2007. Lecture Notes in Computer Science, vol 4739. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75867-9_67
Download citation
DOI: https://doi.org/10.1007/978-3-540-75867-9_67
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75866-2
Online ISBN: 978-3-540-75867-9
eBook Packages: Computer ScienceComputer Science (R0)