Zobrazeno 1 - 10
of 89
pro vyhledávání: '"Strejček, Jan"'
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
Externí odkaz:
http://arxiv.org/abs/2401.12643
Autor:
Jonáš, Martin, Strejček, Jan
Publikováno v:
In Theoretical Computer Science 1 September 2024 1008
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 optimizat
Externí odkaz:
http://arxiv.org/abs/2011.01564
Self-loop alternating automata (SLAA) with B\"uchi or co-B\"uchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei
Externí odkaz:
http://arxiv.org/abs/1908.04645
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 b
Externí odkaz:
http://arxiv.org/abs/1810.12617
Publikováno v:
EPTCS 233, 2016
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
Externí odkaz:
http://arxiv.org/abs/1612.04037
Autor:
Jonáš, Martin, Strejček, Jan
Publikováno v:
Published in Information Processing Letters, 2018, vol. 135C
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 NEXP
Externí odkaz:
http://arxiv.org/abs/1612.01263
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 p
Externí odkaz:
http://arxiv.org/abs/1605.03636
Autor:
Strejček, Jan
This thesis study deals with the development of supplier relationship model, connection to the system concept of this relationship and the use of the fuzzy logic in the supplier evaluation. Thesis study focus on the evaluation of the supplier relatio
Externí odkaz:
http://www.nusl.cz/ntk/nusl-234018
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 appli
Externí odkaz:
http://arxiv.org/abs/1306.4636