Paolo Marin, PhD
Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 051 79110 Freiburg im Breisgau Deutschland
Gebäude 51, Raum 01..030
+49 (0)761 203 8154
+49 (0)761 203 8142
paolo@informatik.uni-freiburg.de
Nach Vereinbarung
Liste filtern : Jahre: 2014 |
2013 |
2012 |
2011 |
2010 |
2009 |
2008 | alle anzeigen nach oben zur Jahresübersicht Sven Reimer, Matthias Sauer, Paolo Marin, Bernd BeckerQBF with Soft Variables 2014 International Workshop on Automated Verification of Critical Systems (AVOCS) Christian Miller, Paolo Marin, Bernd BeckerVerification of Partial Designs Using Incremental QBF 2014 Accepted for publication in AI Commun » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, for some applications SAT formulas are not expressive enough, whereas a description via Quantified Boolean Formulas (QBF) is much more adequate, for instance when dealing with partial designs. Motivated by the success of incremental SAT, in this paper we explore various approaches to solve QBF problems in an incremental fashion and thereby make this technology usable as a core component of BMC. Firstly, we realized an incremental QBF solver based on the state-of-the-art QBF solver QuBE: Taking profit from the reuse of some information from previous iterations, the search space can be pruned, in some cases, to even less than a quarter. However, the need for preprocessing QBF formulas prior to the solving phase, that in general cannot be paired with incremental solving because of the non-predictable elimination of variables in the future incremental steps, posed the question of incremental QBF preprocessing. In this context we present an approach for retaining the QBF formula being preprocessed while extending its clauses and prefix incrementally. This procedure results in a significant size reduction of the QBF formulas, hence leading to a reduced solving time. As this may come together with a high preprocessing time, we analyze various heuristics to dynamically disable incremental preprocessing when its overhead raises over a certain threshold and is not compensated by the reduced solving time anymore. For proving the efficacy of our methods experimentally, as an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes which represent unknown parts). Here, we disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. We examine all these incremental approaches from both the point of view of the effectiveness of the single procedure and the benefits that a range of QBF solvers can take from it. On a domain of partial design benchmarks, engaging incremental QBF methods significant performance gains over non incremental BMC can be achieved. nach oben zur Jahresübersicht Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd BeckerApplying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits 2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to identify functional input sequences
in sequential circuits. The properties required are inserted as target of
a bounded model checking (BMC) problem, by using Craig interpolants
it can be stated whether sequences justifying the properties exist or
not. The initial state is either completely or partially unknown, and for
the latter we engage a MAX-SAT formulation to retrieve the shortest
sequence if a maximal subset of the initial state bits are unknown.
We apply this method to problems arising from digital circuit testing
domain, in which usually an arbitrary initial state is assumed, i.e., that
the circuit’s sequential elements (ﬂip-ﬂops) are assumed to be fully con-
trollable. However, since some of these states may be unreachable during
normal operation, this results in undesired secondary test conditions.
In this paper BMC is used to (1) test timing faults in a digital circuit,
thereby the test requirements are encoded as target properties. Our
method yields the shortest functional test-sequences that justify the target
properties or it proves that such a sequence does not exist. Furthermore,
(2) the initialization of circuits is considered. We analyze the length of
such sequences depending on the number of controllable ﬂip-ﬂops. nach oben zur Jahresübersicht Christian Miller, Paolo Marin, Bernd BeckerA Dynamic QBF Preprocessing Approach for the Verification of Incomplete Designs
2012 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion , Band : 19» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is a major verification technique for finding errors in sequential circuits by unfolding the design iteratively and converting the BMC instances into Boolean satisfiability (SAT) formulas. When considering incomplete designs (i.e. those containing so-called blackboxes), we need the logic of Quantified Boolean Formulas (QBF) to obtain a precise modeling of the unknown behavior of the blackbox. The incremental nature of the BMC problem can be exploited by means of incremental preprocessing of the QBF formulas. It was shown that applying incremental preprocessing produces smaller QBF formulas, but with the price of moving computation time from the solver to the preprocessor, which can rise significantly. In this paper we show how we can take advantage of incremental preprocessing limiting this inconvenient overhead. We start applying incremental preprocessing, and switch to conventional BMC when the
preprocessing effectiveness does not compensate for the time spent. We present multiple switching heuristics, and evaluate the overall performance by running several state-of-the-art QBF solvers as back-end. Comparing these results to those obtained by standard and incremental BMC procedures it turns out that dynamic preprocessing leads to the best overall performance of the whole verification process. Bernd Becker, Ruediger Ehlers, Matthew Lewis, Paolo MarinALLQBF Solving by Computational Learning 2012 Automated Technology for Verification and Analysis , Springer, Band : 7561, Seiten : 370 - 384» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In the last years, search-based QBF solvers have become essential formany applications in the formal methods domain. The exploitation oftheir reasoning efficiency has however been restricted to applicationsin which a ``satisfiable/unsatisfiable'' answer or one model of anopen quantified Boolean formula suffices as an outcome, whereasapplications in which a compact representation of all models isrequired could not be tackled with QBF solvers so far. In this paper,we describe how computational learning provides a remedy to thisproblem. Our algorithms employ a search-based QBF solver and learn theset of all models of a given open QBF problem in a CNF (conjunctivenormal form), DNF (disjunctive normal form), or CDNF (conjunction ofDNFs) representation. We evaluate our approach experimentally usingbenchmarks from synthesis of finite-state systems from temporal logicand monitor computation. Paolo Marin, Christian Miller, Bernd BeckerIncremental QBF Preprocessing for Partial Design Verification - (Poster Presentation) 2012 Int'l Conf. on Theory and Applications of Satisfiability Testing , Springer, Band : 7317, Seiten : 473 - 474» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded Model Checking (BMC) is a major verification method for finding errors in sequential circuits. BMC accomplishes this by iteratively unfolding a circuit k times, adding the negated property, and finally converting the BMC instance into a sequence of satisfiability (SAT) problems. When considering incomplete designs (i.e. those containing so-called blackboxes), we rather need the logic of Quantified Boolean Formulas (QBF) to obtain a more precise modeling of the unknown behavior of the blackbox. Here, we answer the question of unrealizability of a property, where finding a path of length k proves that the property is violated regardless of the implementation of the blackbox. To boost this task, solving blackbox BMC problems incrementally has been shown to be feasible [3], although the restrictions required in the preprocessing phase reduce its effectiveness. In this paper we enhance the verification procedure when using an off-the-shelf QBF solver, through a stronger preprocessing of the QBF formulas applied in an incremental fashion. Paolo Marin, Christian Miller, Matthew Lewis, Bernd BeckerVerification of Partial Designs Using Incremental QBF Solving 2012 Conf. on Design, Automation and Test in Europe , Seiten : 623 - 628» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate.In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing. nach oben zur Jahresübersicht Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaParallel QBF Solving with Advanced Knowledge Sharing 2011 Fundamenta Informaticae , Band : 107, Nummer : 2-3, Seiten : 139 - 166» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results. nach oben zur Jahresübersicht Paolo Marin, Enrico Giunchiglia, Massimo NarizzanoConflict and Solution Driven Constraint Learning in QBF 2010 Doctoral Programme CP 2010 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we describe the Conflict and Solution Driven Constraint
Learning (CSDCL) developed in , a modern search-based QBF
solver which incorporates the latest SAT techniques in terms of data
structures, search heuristics and learning mechanisms, extending them
to the QBF case.
The new learning mechanism implemented in
improves the effectiveness of
non-chronological backtracking by producing asserting clauses and
terms that lead to longer back-jumps and greater reduction in the
search space to be explored. We also report the positive impact given
by modifying the heuristic function, so that it assigns a variable
with the polarity it had before the last backtrack, also called
progress saving in RSat.
In the experimental analysis we compare in the current and
previous versions, showing that the new algorithm is far more
effective in reducing the search space to explore, especially when
combined with progress saving, resulting in
greater efficiency and more solved problems. The comparison with
other state-of-the-art solvers shows that is the fastest
search based QBF solver. Enrico Giunchiglia, Paolo Marin, Massimo NarizzanoQuBE7.0, System Description 2010 Journal of Satisfiability , Band : 7, Nummer : 8, Seiten : 83 - 88» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we outline QuBE7’s main features, describing first the options of the preprocessors, and then giving some details about how the core search-based solver (i) performs unit and pure literal propagation; and (ii) performs the “Conflict Analysis procedure” for non-chronological backtracking, generalised from the SAT to the QBF case. We conclude with the experimental evaluation, showing that QuBE7.0 is the a state-of-the-art single-engine QBF solver. Enrico Giunchiglia, Paolo Marin, Massimo NarizzanosQueezeBF: An effective preprocessor for QBFs 2010 Theory and Applications of Satisfiability Testing , Springer Verlag, Band : 6175, Seiten : 85 - 98» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing. nach oben zur Jahresübersicht Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, Bernd BeckerComparison of Knowledge Sharing Strategies in a Parallel QBF Solver 2009 High-Performance Computing and Simulation Conference , Seiten : 161 - 167 Paolo Marin, Matthew Lewis, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaEvaluation of Knowledge Sharing Strategies in a Parallel QBF Solver 2009 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico GiunchigliaPaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing 2009 Int'l Conf. on Theory and Applications of Satisfiability Testing , Band : 5584, Seiten : 509 - 523 nach oben zur Jahresübersicht Enrico Giunchiglia, Paolo Marin, Massimo NarizzanoAn Effective Preprocessor for QBF pre-reasoning 2008 Int'l Workshop on Quantification in Constraint Programming