Author name cluster

Jaroslav Bendík

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

LPAR Conference 2023 Conference Paper

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification

Petra Hozzová
Jaroslav Bendík
Alexander Nutz
Yoav Rodeh

The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.

Details

AAAI Conference 2021 Conference Paper

Counting Maximal Satisfiable Subsets

Jaroslav Bendík
Kuldeep S. Meel

Given an unsatisfiable set of constraints F, a maximal satisfiable subset (MSS) is a maximal subset of constraints C ⊆ F such that C is satisfiable. Over the past two decades, the steady improvement in runtime performance of algorithms for finding MSSes has led to increased adoption of MSSbased techniques in a wide variety of domains. Motivated by the progress in finding an MSS, the past decade has witnessed a surge of interest in the design of algorithmic techniques to enumerate all the MSSes, which has subsequently led to a discovery of new applications utilizing enumeration of MSSes. The development of techniques for finding and enumeration of MSSes mirrors a similar phenomenon of finding and enumeration of SAT solutions in the early 2000s, which subsequently motivated the design of algorithmic techniques for model counting. In a similar spirit, we undertake a study to investigate the feasibility of MSS counting techniques. In particular, the focus point of our investigation is to answer whether one can design efficient MSS counting techniques that do not rely on explicit MSS enumeration. The primary contribution of this work is an affirmative answer to the above question in the form of a novel algorithm. The algorithm uses a novel architecture of a wrapper W and a remainder R such that the desired MSS count can be expressed as |W|−|R|. To efficiently compute |W| and |R|, the algorithm relies on the advances in projected model counting. Our empirical evaluation demonstrates that our approach can scale to instances clearly beyond the reach of enumeration-based techniques.

PDF Details

LPAR Conference 2020 Conference Paper

Rotation Based MSS/MCS Enumeration

Jaroslav Bendík
Ivana Cerna

Given an unsatisfiable Boolean Formula F in CNF, i. e. , a set of clauses, one is often interested in identifying Maximal Satisfiable Subsets (MSSes) of F or, equivalently, the complements of MSSes called Minimal Correction Subsets (MCSes). Since MSSes (MC- Ses) find applications in many domains, e. g. diagnosis, ontologies debugging, or axiom pinpointing, several MSS enumeration algorithms have been proposed. Unfortunately, finding even a single MSS is often very hard since it naturally subsumes repeatedly solving the satisfiability problem. Moreover, there can be up to exponentially many MSSes, thus their complete enumeration is often practically intractable. Therefore, the algorithms tend to identify as many MSSes as possible within a given time limit. In this work, we present a novel MSS enumeration algorithm called RIME. Compared to existing algorithms, RIME is much more frugal in the number of performed satisfiability checks which we witness via an experimental comparison. Moreover, RIME is several times faster than existing tools.

Details

LPAR Conference 2018 Conference Paper

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Jaroslav Bendík
Ivana Cerna

In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i. e. , one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches. In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evalu- ation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.

Details