In the last years the formal verification technique "property checking" was used to prove the correctness of microchip designs. This technique checks all possible input pattern which satisfy the design if these also valid for the given property. Such a property is given in a formal language, such as Verilog or VHDL, and describes certain aspects of a chip design. The "property checking" method brought a huge improvement compared to the simulation technique. This technique, however, just verifies a chip design point-wise, such that the global correctness of a design still is unproven. In case a property is faulty, it is of interest the know the number input patterns which lead to in incorrect output.

The goal of this project is to analyze these problems from the mathematical point view to check whether the number faulty input pattern is computable in a reasonable time. Therefore, the focus is on the techniques developed in the Valse-XT project. In particular in which way these are extendable, to solve the counting problems efficiently.

Publications

2008
Constraint Integer Programming: A New Approach to Integrate CP and MIP Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008, Laurent Perron, Michael Trick (Eds.), pp. 6-20, Vol.5015, Lecture Notes in Computer Science, 2008 (preprint available as ZIB-Report 08-01) Tobias Achterberg, Timo Berthold, Thorsten Koch, Kati Wolter PDF (ZIB-Report)
BibTeX
DOI
Counting Solutions in the Field of Verification
Constraint Integer Programming: Techniques and Applications ZIB-Report 08-43 Tobias Achterberg, Timo Berthold, Stefan Heinz, Thorsten Koch, Kati Wolter PDF
BibTeX
URN
Counting Solutions in the Field of Verification
Counting Solutions of Integer Programs Using Unrestricted Subtree Detection Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008, Laurent Perron, Michael Trick (Eds.), pp. 278-282, Vol.5015, Lecture Notes in Computer Science, 2008 (preprint available as ZIB-Report 08-09) Tobias Achterberg, Stefan Heinz, Thorsten Koch PDF (ZIB-Report)
BibTeX
Counting Solutions in the Field of Verification
Using Model Counting to Find Optimal Distinguishing Tests ZIB-Report 08-32 (Appeared in: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems : 6th International Conference, CPAIOR 2009, Lecture Notes in Computer Science 5547, pp. 117-131, 2009) Stefan Heinz, Martin Sachenbacher PDF
BibTeX
URN
Counting Solutions in the Field of Verification
Wegeprobleme der Graphentheorie ZIB-Report 08-26 Johanna Ridder PDF
BibTeX
URN
Counting Solutions in the Field of Verification
2007
Constraint Integer Programming Doctoral thesis, Technische Universität Berlin, Martin Grötschel, Robert E. Bixby (Advisors), 2007 Tobias Achterberg PDF
PDF
BibTeX
URN
Counting Solutions in the Field of Verification
Property Checking with Constraint Integer Programming ZIB-Report 07-37 Tobias Achterberg, Raik Brinkmann, Markus Wedler PDF
BibTeX
URN
Counting Solutions in the Field of Verification