Search

Your search keyword '"Slabý, Jiří"' showing total 45 results
Start Over Author "Slabý, Jiří"
45 results on '"Slabý, Jiří"'

2. STANSE: Bug-finding Framework for C Programs

Author

Obdržálek, Jan, Slabý, Jiří, and Trtík, Marek

Subjects
Computer Science - Software Engineering
Abstract

STANSE is a free (available under the GPLv2 license) modular framework for finding bugs in C programs using static analysis. Its two main design goals are 1) ability to process large software projects like the Linux kernel and 2) extensibility with new bug-finding techniques with a minimal effort. Currently there are four bug-finding algorithms implemented within STANSE: AutomatonChecker checks properties described in an automata-based formalism, ThreadChecker detects deadlocks among multiple threads, LockChecker finds locking errors based on statistics, and ReachabilityChecker looks for unreachable code. STANSE has been tested on the Linux kernel, where it has found dozens of previously undiscovered bugs.

Published
2012

3. On Synergy of Metal, Slicing, and Symbolic Execution

Author

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

Subjects
Computer Science - Programming Languages
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. 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.

Published
2012

4. Compact Symbolic Execution

Author

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

Subjects
Computer Science - Programming Languages
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 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., Comment: This is a full version of the paper accepted to ATVA 2013

Published
2012

5. Symbiotic 4: Beyond Reachability : (Competition Contribution)

Author

Chalupa, Marek, Vitovská, Martina, Jonáš, Martin, Slaby, Jiri, Strejček, Jan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Legay, Axel, editor, and Margaria, Tiziana, editor

Published
2017
Full Text
View/download PDF

6. Symbiotic 3: New Slicer and Error-Witness Generation : (Competition Contribution)

Author

Chalupa, Marek, Jonáš, Martin, Slaby, Jiri, Strejček, Jan, Vitovská, Martina, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Chechik, Marsha, editor, and Raskin, Jean-François, editor

Published
2016
Full Text
View/download PDF

8. ClabureDB: Classified Bug-Reports Database : Tool for Developers of Program Analysis Tools

Author

Slaby, Jiri, Strejček, Jan, Trtík, Marek, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Giacobazzi, Roberto, editor, Berdine, Josh, editor, and Mastroeni, Isabella, editor

Published
2013
Full Text
View/download PDF

10. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution

Author

Slabý, Jiří, Strejček, Jan, Trtík, Marek, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Stoelinga, Mariëlle, editor, and Pinger, Ralf, editor

Published
2012
Full Text
View/download PDF

12. Symbiotic 2: More Precise Slicing : (Competition Contribution)

Author

Slaby, Jiri, Strejček, Jan, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Ábrahám, Erika, editor, and Havelund, Klaus, editor

Published
2014
Full Text
View/download PDF

14. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution : (Competition Contribution)

Author

Slaby, Jiri, Strejček, Jan, Trtík, Marek, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Piterman, Nir, editor, and Smolka, Scott A., editor

Published
2013
Full Text
View/download PDF

17. Integration of the Expelled Germans in Bavaria

Author

Slabý, Jiří, Šmidrkal, Václav, and Kučera, Jaroslav

Subjects
Expulsion of Germans, Bavaria, záchytné tábory, vysídlení Němců, Refugee Camps, Bavorsko, integrace vysídlených Němců, Integration of the Expellees
Published
2021

21. Využití softwarových nástrojů pro týmovou spolupráci ve škole

Author

Slabý, Jiří, Vaňková, Petra, and Leipert, Jiří

Subjects
ComputingMilieux_COMPUTERSANDEDUCATION, scénáře, Canvas Instructure, license, Team Collaboration, Edmodo, comparison, Workplace by Facebook, Microsoft Teams, multiple-criteria analysis, Google Hangouts Chat, scenarios, Office 365, licence, vícekriteriální rozhodování, Týmová spolupráce, cloud, porovnání
Abstract

TITLE: Use of Software Tools for Teamwork at School AUTHOR: Jiří Slabý DEPARTMENT: Department of Information Technology and Education SUPERVISOR: PhDr. Petra Vaňková, Ph.D. ABSTRACT: The work is focused on software tools for teamwork including comparison and deployment in a pilot solution in a particular high school. By conducting searches in literature and Internet resources related to the given topic, basic concepts related to teamwork are described and activities that take place within the scope of teamwork are outlined. Software tools for teamwork are analyzed, suitable selection criteria and their weights are set, and a comparison of selected software tools is performed using multiple-criteria analysis. The aim is to choose a suitable tool for teamwork and to propose its use in a particular school. Based on the results of the comparison, the Microsoft Teams team collaboration tool is selected and deployed because it matches the needs of a particular school in the best way. The benefit of this work is an overview and comparison of tools that enable teamwork and communication; the proposed scenarios and practical use of software team tools at school are beneficial, too. Another benefit of the work lies in describing how to deploy the selected Microsoft Teams tool. The thesis work summarizes...

Published
2019

28. ClabureDB: Classified Bug-Reports Database Tool for Developers of Program Analysis Tools

Author

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

Subjects
Bug database, classified bug-reports
Abstract

We present a database that can serve as a tool for tuning and evaluation of miscellaneous program analysis tools. The database contains bug-reports produced by various tools applied to various source codes. The bug-reports are classified as either real errors or false positives. The database currently contains more than 800 bug-reports detected in the Linux kernel 2.6.28. Support of other software projects written in various programming languages is planned. The database can be downloaded and manipulated by SQL queries, or accessed via a web frontend. Představujeme databázi, která může sloužit jako nástroj pro ladění a evaluaci nástrojů pro analýzu programů. Databáze obsahuje záznamy o chybách vyprodukované různými nástroji spuštěnými na různé zdrojové kódy. Tyto záznamy jsou klasifikovány buď jako skutečn0 chyby nebo jako falešná hlášení. Databáza v současnosti obsahuje přes 800 záznamů pro Linux kernel 2.6.28. Je plánována i podpora pro další softwarové projekty napsané v různých programovacích jazycích. Databázi je možno stáhnout a využívat pomocí SQL dotazů nebo s pomocí webového rozhraní.

Published
2013

29. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution)

Author

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

Subjects
instrumentation, symbolic execution, program slicing
Abstract

Symbiotic is a tool for detection of bugs described by finite state machines in C programs. The tool combines three well-known techniques: instrumentation, program slicing, and symbolic execution. This paper briefly describes the approach of Symbiotic including its strengths, weaknesses, and modifications for SV-COMP 2013. Architecture and installation of the tool are described as well. Symbiotic je nástroj pro detekci chyb popsaných pomocí konečně-stavových strojů v programech v jazyce C. Tento nástroj kombinuje tři dobře známé techniky: instrumentaci, program slicing a symbolickou exekuci. Článek stručně popisuje přístup Symbioticu včetně jeho silných a slabých stránek a úprav pro soutěž SV-COMP 2013. Také je popsána architektura a instalace nástroje.

Published
2013

30. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution

Author

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

Subjects
Bug finding, Symbolic execution, Program slicing, FSM property specification, Code instrumentation
Abstract

We introduce a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs. 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. Představujeme novou techniku pro ověřování vlastností popsaných konečně-stavovými stroji. Tato technika je založena na synergii tří známých metod: instrumentace, prořezání programu a symbolické vykonání. Přesněji, instrumentujeme daný program kódem, který sleduje běh stavových strojů představujících různé vlastnosti. Dále program prořežeme, abychom zmenšili jeho velikost při zachování běhů stavových strojů. Nakonec prořezaný program symbolicky vykonáme, abychom našli skutečné porušení ověřovaných vlastností, t.j. skutečné chyby. Podle použitého druhu symbolického vykonání může být tato technika použita jako samostatná metoda pro detekci chyb nebo k vytřídění některých falešných hlášení z výstupu jiných nástrojů pro detekci chyb. Poskytujeme několik příkladů, které dokumentují praktickou použitelnost naší techniky.

Published
2012

31. Business Plan of Family Amusement Center Funland

Author

Slabý, Jiří, Hartman, Ladislav, and Potluka, Oto

Subjects
Amusement Center, centrum volného času, Leisure, podnikatelský plán, volný čas, Business Plan
Abstract

The main purpose of this thesis is business plan of new family fun center and evaluates its business plan. The diploma thesis is divided to two parts. The first part of thesis concentrates on theoretical part and prepares basis for the practical part and deals with issues in its spare time from different angles, the actual business plan and selecting appropriate legal forms of business. Second part includes business plan which will be used for dealings with financial institutions and investors. The business plan contains all the key parts such as the introduction of company, PEST analysis or analysis of competitors, marketing plan, operation and financial plan.

Published
2011

32. Poptávka po dovolené v Chorvatsku

Author

Slabý, Jiří, Macáková, Libuše, and Nováček, Jan

Subjects
Chorvatsko, cestovní ruch, ekonomie volného času
Abstract

Tato bakalářská práce se zabývá faktory, které působí na cestování českých občanů do Chorvatska, a důvody, proč je tato země nejoblíbenější destinací českých turistů. Součástí práce je také analýza výjezdového cestovního ruchu občanů České republiky a průzkum zabývající se především cestováním do Chorvatska.

Published
2008

45. Moderní informační infrastruktura organizace - na konkrétním případě

Author

Žemlička, Jan, Kubešová, Vlasta, and Slabý, Jiří

Subjects
SAP, NetWeaver, systém řízení, informační systém, informační infrastruktura
Abstract

Diplomová práce se zabývá problematikovu budování informační infrastruktury organizace. V první, teoretické, části se zabývá obecně pojmem informace, jejími atributy, významem a účelem, který přestavuje pro současné podniky jeden z klíčových faktorů úspěchu. V druhé, praktické, části naznačuje na konkrétním případě možnosti budování informační infrastruktury na platformě produktů společnosti SAP, s ohledem na organizační a uživatelské požadavky.

Published
2006

Catalog

Books, media, physical & digital resources
See catalog results