Showing 1–14 of 14 results for author: Strejček, J

Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage (Technical Report)

Authors: Martin Jonáš, Jan Strejček, Marek Trtík, Lukáš Urban

Abstract: We present a novel gray-box fuzzing algorithm monitoring executions of instructions converting numerical values to Boolean ones. An important class of such instructions evaluate predicates, e.g., *cmp in LLVM. That alone allows us to infer the input dependency (c.f. the taint analysis) during the fuzzing on-the-fly with reasonable accuracy, which in turn enables an effective use of the gradient de… ▽ More We present a novel gray-box fuzzing algorithm monitoring executions of instructions converting numerical values to Boolean ones. An important class of such instructions evaluate predicates, e.g., *cmp in LLVM. That alone allows us to infer the input dependency (c.f. the taint analysis) during the fuzzing on-the-fly with reasonable accuracy, which in turn enables an effective use of the gradient descent on these instructions (to invert the result of their evaluation). Although the fuzzing attempts to maximize the coverage of the instructions, there is an interesting correlation with the standard branch coverage, which we are able to achieve indirectly. The evaluation on Test-Comp 2023 benchmarks shows that our approach, despite being a pure gray-box fuzzing, is able to compete with the leading tools in the competition, which combine fuzzing with other powerful techniques like model checking, symbolic execution, or abstract interpretation. △ Less

Submitted 23 January, 2024; originally announced January 2024.

Comments: 37 pages

Fast Computation of Strong Control Dependencies

Authors: Marek Chalupa, David Klaška, Jan Strejček, Lukáš Tomovič

Abstract: We introduce new algorithms for computing non-termination sensitive control dependence (NTSCD) and decisive order dependence (DOD). These relations on control flow graph vertices have many applications including program slicing and compiler optimizations. Our algorithms are asymptotically faster than the current algorithms. We also show that the original algorithms for computing NTSCD and DOD may… ▽ More We introduce new algorithms for computing non-termination sensitive control dependence (NTSCD) and decisive order dependence (DOD). These relations on control flow graph vertices have many applications including program slicing and compiler optimizations. Our algorithms are asymptotically faster than the current algorithms. We also show that the original algorithms for computing NTSCD and DOD may produce incorrect results. We implemented the new as well as fixed versions of the original algorithms for the computation of NTSCD and DOD and we experimentally compare their performance and outcome. Our algorithms dramatically outperform the original ones. △ Less

Submitted 3 November, 2020; originally announced November 2020.

LTL to Smaller Self-Loop Alternating Automata and Back

Authors: František Blahoudek, Juraj Major, Jan Strejček

Abstract: Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces consi… ▽ More Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae. △ Less

Submitted 16 October, 2019; v1 submitted 13 August, 2019; originally announced August 2019.

Comments: This is a full version of the paper accepted to ICTAC 2019

SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode

Authors: Martina Vitovská, Marek Chalupa, Jan Strejček

Abstract: The paper describes a member of the Symbiotic toolbox called sbt-instrumentation, which is a tool for configurable instrumentation of LLVM bitcode. The tool enables a user to specify patterns of instructions and to define functions whose calls will be inserted before or after instructions that match the patterns. Moreover, the tool offers additional functionality. First, the instrumentation can be… ▽ More The paper describes a member of the Symbiotic toolbox called sbt-instrumentation, which is a tool for configurable instrumentation of LLVM bitcode. The tool enables a user to specify patterns of instructions and to define functions whose calls will be inserted before or after instructions that match the patterns. Moreover, the tool offers additional functionality. First, the instrumentation can be divided into phases in order to pass information acquired in an earlier phase to the later phases. Second, it can utilize results of some external static analysis by connecting it as a plugin. The sbt-instrumentation tool has been developed as the part of Symbiotic responsible for inserting memory safety checks. However, its configurability opens the way to use it for many various purposes. △ Less

Submitted 30 October, 2018; originally announced October 2018.

Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science

Authors: Jan Bouda, Lukáš Holík, Jan Kofroň, Jan Strejček, Adam Rambousek

Abstract: MEMICS provides a forum for doctoral students interested in applications of mathematical and engineering methods in computer science. Besides a rich technical programme (including invited talks, regular papers, and presentations), MEMICS also offers friendly social activities and exciting opportunities for meeting like-minded people. MEMICS submissions traditionally cover all areas of computer sci… ▽ More MEMICS provides a forum for doctoral students interested in applications of mathematical and engineering methods in computer science. Besides a rich technical programme (including invited talks, regular papers, and presentations), MEMICS also offers friendly social activities and exciting opportunities for meeting like-minded people. MEMICS submissions traditionally cover all areas of computer science (such as parallel and distributed computing, computer networks, modern hardware and its design, non-traditional computing architectures, information systems and databases, multimedia and graphics, verification and testing, computer security, as well as all related areas of theoretical computer science). △ Less

Submitted 13 December, 2016; originally announced December 2016.

Journal ref: EPTCS 233, 2016

On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding

Authors: Martin Jonáš, Jan Strejček

Abstract: We study the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors with binary-encoded bit-widths and constants. This problem is known to be in EXPSPACE and to be NEXPTIME-hard. We show that this problem is complete for the complexity class AEXP(poly) -- the class of problems decidable by an alternating Turing machi… ▽ More We study the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors with binary-encoded bit-widths and constants. This problem is known to be in EXPSPACE and to be NEXPTIME-hard. We show that this problem is complete for the complexity class AEXP(poly) -- the class of problems decidable by an alternating Turing machine using exponential time, but only a polynomial number of alternations between existential and universal states. △ Less

Submitted 2 May, 2018; v1 submitted 5 December, 2016; originally announced December 2016.

Journal ref: Published in Information Processing Letters, 2018, vol. 135C

Tighter Loop Bound Analysis (Technical report)

Authors: Pavel Čadek, Jan Strejček, Marek Trtík

Abstract: We present a new algorithm for computing upper bounds on the number of executions of each program instruction during any single program run. The upper bounds are expressed as functions of program input values. The algorithm is primarily designed to produce bounds that are relatively tight, i.e. not unnecessarily blown up. The upper bounds for instructions allow us to infer loop bounds, i.e.~upper… ▽ More We present a new algorithm for computing upper bounds on the number of executions of each program instruction during any single program run. The upper bounds are expressed as functions of program input values. The algorithm is primarily designed to produce bounds that are relatively tight, i.e. not unnecessarily blown up. The upper bounds for instructions allow us to infer loop bounds, i.e.~upper bounds on the number of loop iterations. Experimental results show that the algorithm implemented in a prototype tool Looperman often produces tighter bounds than current tools for loop bound analysis. △ Less

Submitted 11 May, 2016; originally announced May 2016.

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

Authors: Tomáš Babiak, František Blahoudek, Mojmír Křetínský, Jan Strejček

Abstract: Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternatin… ▽ More Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae. △ Less

Submitted 6 November, 2013; v1 submitted 19 June, 2013; originally announced June 2013.

Comments: Full version of the paper accepted to ATVA 2013

On Synergy of Metal, Slicing, and Symbolic Execution

Authors: Jiří Slabý, Jan Strejček, Marek Trtík

Abstract: We introduce a novel technique for finding real errors in programs. The technique is based on a synergy of three well-known methods: metacompilation, slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various kinds of errors. Next we slice the program to reduce its size without affecting runs of state machines.… ▽ More We introduce a novel technique for finding real errors in programs. The technique is based on a synergy of three well-known methods: metacompilation, slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various kinds of errors. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positives from an output of another bug-finding tool. We provide several examples demonstrating the practical applicability of our technique. △ Less

Submitted 23 January, 2012; originally announced January 2012.

Compact Symbolic Execution

Authors: Jiří Slabý, Jan Strejček, Marek Trtík

Abstract: We present a generalisation of King's symbolic execution technique called compact symbolic execution. It proceeds in two steps. First, we analyse cyclic paths in the control flow graph of a given program, independently from the rest of the program. Our goal is to compute a so called template for each such a cyclic path. A template is a declarative parametric description of all possible program sta… ▽ More We present a generalisation of King's symbolic execution technique called compact symbolic execution. It proceeds in two steps. First, we analyse cyclic paths in the control flow graph of a given program, independently from the rest of the program. Our goal is to compute a so called template for each such a cyclic path. A template is a declarative parametric description of all possible program states, which may leave the analysed cyclic path after any number of iterations along it. In the second step, we execute the program symbolically with the templates in hand. The result is a compact symbolic execution tree. A compact tree always carry the same information in all its leaves as the corresponding classic symbolic execution tree. Nevertheless, a compact tree is typically substantially smaller than the corresponding classic tree. There are even programs for which compact symbolic execution trees are finite while classic symbolic execution trees are infinite. △ Less

Submitted 17 September, 2013; v1 submitted 23 January, 2012; originally announced January 2012.

Comments: This is a full version of the paper accepted to ATVA 2013

LTL to Büchi Automata Translation: Fast and More Deterministic

Authors: Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček

Abstract: We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in f… ▽ More We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially. △ Less

Submitted 29 March, 2012; v1 submitted 3 January, 2012; originally announced January 2012.

Comments: Full version of the paper presented at TACAS 2012

Abstracting Path Conditions

Authors: Jan Strejček, Marek Trtík

Abstract: We present a symbolic-execution-based algorithm that for a given program and a given program location produces a nontrivial necessary condition on input values to drive the program execution to the given location. We also propose an application of necessary conditions in contemporary bug-finding and test-generation tools. Experimental results show that the presented technique can significantly imp… ▽ More We present a symbolic-execution-based algorithm that for a given program and a given program location produces a nontrivial necessary condition on input values to drive the program execution to the given location. We also propose an application of necessary conditions in contemporary bug-finding and test-generation tools. Experimental results show that the presented technique can significantly improve performance of the tools. △ Less

Submitted 10 December, 2016; v1 submitted 23 December, 2011; originally announced December 2011.

Comments: a shorter version published at ISSTA 2012. arXiv admin note: text overlap with arXiv:1112.4703

A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness

Authors: Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček

Abstract: We identify a subtle error in LTL formulas reduction method used as one optimization step in an LTL to Büchi automata translation. The error led to some incorrect answers of the established model checker DiVinE. This paper should help authors of other model checkers to avoid this error. We identify a subtle error in LTL formulas reduction method used as one optimization step in an LTL to Büchi automata translation. The error led to some incorrect answers of the established model checker DiVinE. This paper should help authors of other model checkers to avoid this error. △ Less

Submitted 16 December, 2010; v1 submitted 18 November, 2010; originally announced November 2010.

Almost Linear Büchi Automata

Authors: Tomáš Babiak, Vojtěch Řehák, Jan Strejček

Abstract: We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is dire… ▽ More We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Buechi automata studied in this context and we indicate possible applications. △ Less

Submitted 10 November, 2009; originally announced November 2009.

Journal ref: EPTCS 8, 2009, pp. 16-25