26 Search Results for "Vojnar, Tomas"


Volume

OASIcs, Volume 16

Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers

MEMICS 2010, October 22-24, 2010, Mikulov, Czech Republic

Editors: Ludek Matyska, Michal Kozubek, Tomas Vojnar, Pavel Zemcik, and David Antos

Volume

OASIcs, Volume 13

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)

MEMICS 2009, November 13-15, 2009, Znojmo, Czech Republic

Editors: Petr Hlinený, Václav Matyáš, and Tomáš Vojnar

Document
Artifact
Low-Level Bi-Abduction (Artifact)

Authors: Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)


Abstract
Broom is a new static analyzer for C written in OCaml. Broom primarily aims at open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds of lists - that employ advanced low-level pointer operations. It is based on separation logic and the principle of bi-abductive reasoning. The artifact is a VirtualBox image of a Linux machine with Ubuntu 20.04 operating system. It contains source code and binary of the Broom tool, benchmarks, and scripts for running our and the competing tools we compare to.

Cite as

Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger. Low-Level Bi-Abduction (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 11:1-11:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{holik_et_al:DARTS.8.2.11,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Peringer, Petr and Rogalewicz, Adam and \v{S}okov\'{a}, Veronika and Vojnar, Tom\'{a}\v{s} and Zuleger, Florian},
  title =	{{Low-Level Bi-Abduction (Artifact)}},
  pages =	{11:1--11:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Hol{\'\i}k, Luk\'{a}\v{s} and Peringer, Petr and Rogalewicz, Adam and \v{S}okov\'{a}, Veronika and Vojnar, Tom\'{a}\v{s} and Zuleger, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.11},
  URN =		{urn:nbn:de:0030-drops-162092},
  doi =		{10.4230/DARTS.8.2.11},
  annote =	{Keywords: programs with dynamic linked data structures, programs with pointers, low-level pointer operations, static analysis, shape analysis, separation logic, bi-abduction}
}
Document
Low-Level Bi-Abduction

Authors: Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)


Abstract
The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds of lists - that employ advanced low-level pointer operations. The goal is to allow such programs be analysed without a need of writing analysis harnesses that would first initialise the structures being handled. The approach builds on a special flavour of separation logic and the approach of bi-abduction. The code of interest is analyzed along the call tree, starting from its leaves, with each function analysed just once without any call context, leading to a set of contracts summarizing the behaviour of the analysed functions. In order to handle the considered programs, methods of abduction existing in the literature are significantly modified and extended in the paper. The proposed approach has been implemented in a tool prototype and successfully evaluated on not large but complex programs.

Cite as

Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger. Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.ECOOP.2022.19,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Peringer, Petr and Rogalewicz, Adam and \v{S}okov\'{a}, Veronika and Vojnar, Tom\'{a}\v{s} and Zuleger, Florian},
  title =	{{Low-Level Bi-Abduction}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{19:1--19:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.19},
  URN =		{urn:nbn:de:0030-drops-162477},
  doi =		{10.4230/LIPIcs.ECOOP.2022.19},
  annote =	{Keywords: programs with dynamic linked data structures, programs with pointers, low-level pointer operations, static analysis, shape analysis, separation logic, bi-abduction}
}
Document
Complete Volume
OASIcs, Volume 13, MEMICS'09, Complete Volume

Authors: Petr Hlinený, Václav Matyáš, and Tomáš Vojnar

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)


Abstract
OASIcs, Volume 13, MEMICS'09, Complete Volume

Cite as

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Proceedings{hlineny_et_al:OASIcs.MEMICS.2009,
  title =	{{OASIcs, Volume 13, MEMICS'09, Complete Volume}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2009},
  URN =		{urn:nbn:de:0030-drops-35756},
  doi =		{10.4230/OASIcs.MEMICS.2009},
  annote =	{Keywords: Mathematics of Computing, Physical Sciences and Engineering}
}
Document
Complete Volume
OASIcs, Volume 16, MEMICS'10, Complete Volume

Authors: Ludek Matyska, Michal Kozubek, Tomáš Vojnar, Pavel Zemcík, and David Antos

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
OASIcs, Volume 16, MEMICS'10, Complete Volume

Cite as

Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Proceedings{matyska_et_al:OASIcs.MEMICS.2010,
  title =	{{OASIcs, Volume 16, MEMICS'10, Complete Volume}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010},
  URN =		{urn:nbn:de:0030-drops-35789},
  doi =		{10.4230/OASIcs.MEMICS.2010},
  annote =	{Keywords: Control structures and microprogramming, Input/output and data communications, Integrated circuits, Performance and reliability}
}
Document
Front Matter
Frontmatter, Preface, Table of Contents, Workshop Organization

Authors: Ludek Matyska, Michal Kozubek, Tomas Vojnar, Pavel Zemcik, and David Antos

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
Frontmatter, Preface, Table of Contents, Workshop Organization

Cite as

Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. i-viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{matyska_et_al:OASIcs.MEMICS.2010.i,
  author =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  title =	{{Frontmatter, Preface, Table of Contents, Workshop Organization}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{i--viii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.i},
  URN =		{urn:nbn:de:0030-drops-30574},
  doi =		{10.4230/OASIcs.MEMICS.2010.i},
  annote =	{Keywords: Frontmatter, Preface, Table of Contents, Workshop Organization}
}
Document
CUDA Accelerated LTL Model Checking -­ Revisited

Authors: Petr Bauch and Milan Ceska

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
Recently, the massively parallel architecture has been used to significantly accelerate many computation demanding tasks. For example, in [Baier, Kateon, The MIT Press, 2009; Barnat, Brim, Ceska, ICPADS 2009] we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. In this paper we redesign the One-Way-Catch-Them-Young (OWCTY) algorithm [Cerna, Pelanek, SPIN'03] in order to devise a new CUDA accelerated OWCTY algorithm that will significantly outperform the original CUDA accelerated algorithm and will be resistant to slowdown caused by improper ordering of the input data representation.

Cite as

Petr Bauch and Milan Ceska. CUDA Accelerated LTL Model Checking -­ Revisited. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{bauch_et_al:OASIcs.MEMICS.2010.1,
  author =	{Bauch, Petr and Ceska, Milan},
  title =	{{CUDA Accelerated LTL Model Checking -­ Revisited}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{1--8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.1},
  URN =		{urn:nbn:de:0030-drops-30729},
  doi =		{10.4230/OASIcs.MEMICS.2010.1},
  annote =	{Keywords: LTL Model Checking, CUDA, OWCTY}
}
Document
Process Algebra for Modal Transition Systemses

Authors: Nikola Benes and Jan Kretinsky

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged. Therefore, we introduce transition system with obligations as a general model encompassing all the aforementioned models, and equip it with a process algebra description. Using these instruments, we then compare the previously studied subclasses and characterize their relationships.

Cite as

Nikola Benes and Jan Kretinsky. Process Algebra for Modal Transition Systemses. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 9-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{benes_et_al:OASIcs.MEMICS.2010.9,
  author =	{Benes, Nikola and Kretinsky, Jan},
  title =	{{Process Algebra for Modal Transition Systemses}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{9--18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.9},
  URN =		{urn:nbn:de:0030-drops-30701},
  doi =		{10.4230/OASIcs.MEMICS.2010.9},
  annote =	{Keywords: modal transition systems, process algebra, specification}
}
Document
A Simple Topology Preserving Max-Flow Algorithm for Graph Cut Based Image Segmentation

Authors: Ondrej Danek and Martin Maska

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
In this paper, we propose a modification to the Boykov-Kolmogorov maximum flow algorithm [Boykov, Kolmogorv, IEEE 2004] in order to make the algorithm preserve the topology of an initial interface. This algorithm is being widely used in computer vision and image processing fields for its efficiency and speed when dealing with problems such as graph cut based image segmentation. Using our modification we are able to incorporate a topology prior into the algorithm allowing us to apply it in situations in which the inherent topological flexibility of graph cuts is inconvenient (e.g., biomedical image segmentation). Our approach exploits the simple point concept from digital geometry and is simpler and more straightforward to implement than previously introduced methods [Zeng, Samaras, Chen, Peng, Computer Vision and Image Understanding, 2008]. Due to the NP-completeness of the topology preserving problem our algorithm is only an approximation and is initialization dependent. However, promising results are demonstrated on graph cut based segmentation of both synthetic and real image data.

Cite as

Ondrej Danek and Martin Maska. A Simple Topology Preserving Max-Flow Algorithm for Graph Cut Based Image Segmentation. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 19-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{danek_et_al:OASIcs.MEMICS.2010.19,
  author =	{Danek, Ondrej and Maska, Martin},
  title =	{{A Simple Topology Preserving Max-Flow Algorithm for Graph Cut Based Image Segmentation}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{19--25},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.19},
  URN =		{urn:nbn:de:0030-drops-30695},
  doi =		{10.4230/OASIcs.MEMICS.2010.19},
  annote =	{Keywords: maximum flow, topology preserving, image segmentation, graph cuts}
}
Document
Haptic Rendering Based on RBF Approximation from Dynamically Updated Data

Authors: Jan Fousek, Tomas Golembiovsky, Jiri Filipovic, and Igor Peterlik

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
In this paper, an extension of our previous research focused on haptic rendering based on interpolation from precomputed data is presented. The technique employs the radial-basis function (RBF) interpolation to achieve the accuracy of the force response approximation, however, it assumes that the data used by the interpolation method are generated on-the-fly during the haptic interaction. The issue caused by updating the RBF coefficients during the interaction is analyzed and a force-response smoothing strategy is proposed.

Cite as

Jan Fousek, Tomas Golembiovsky, Jiri Filipovic, and Igor Peterlik. Haptic Rendering Based on RBF Approximation from Dynamically Updated Data. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 26-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{fousek_et_al:OASIcs.MEMICS.2010.26,
  author =	{Fousek, Jan and Golembiovsky, Tomas and Filipovic, Jiri and Peterlik, Igor},
  title =	{{Haptic Rendering Based on RBF Approximation from Dynamically Updated Data}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{26--31},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.26},
  URN =		{urn:nbn:de:0030-drops-30592},
  doi =		{10.4230/OASIcs.MEMICS.2010.26},
  annote =	{Keywords: haptic rendering, radial-basis function approximation, precomputation, deformation modeling}
}
Document
Modeling Gene Networks using Fuzzy Logic

Authors: Artur Gintrowski

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
Recently, almost uncontrolled technological progress allows so called high-throughput data collection for sophisticated and complex experimental biological systems analysis. Especially, it concerns the whole cellular genome. Therefore it becomes more and more vital to suggest and elaborate gene network models, which can be used for more complete interpretation of large and complex data sets. The presented paper concerns modeling of interactions in yeast genome. With the reference to previously published papers concerning the same subject, our paper presents a significant improvement in calculation procedure leading to very effective reduction of time of calculation.

Cite as

Artur Gintrowski. Modeling Gene Networks using Fuzzy Logic. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 32-39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{gintrowski:OASIcs.MEMICS.2010.32,
  author =	{Gintrowski, Artur},
  title =	{{Modeling Gene Networks using Fuzzy Logic}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{32--39},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.32},
  URN =		{urn:nbn:de:0030-drops-30749},
  doi =		{10.4230/OASIcs.MEMICS.2010.32},
  annote =	{Keywords: Fuzzy network, gene expression, time optimization}
}
Document
Compression of Vector Field Changing in Time

Authors: Tomas Golembiovsky and Ales Krenek

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
One of the problems connected with a real-time protein-ligand docking simulation is the need to store series of precomputed electrostatic force fields of a molecule changing in time. A single frame of the force field is a 3D array of floating point vectors and it constitutes approximately 180 MB of data. Therefore requirements on storage grow rapidly if several hundreds of such frames need to be stored. We propose a lossy compression method of such force field, based on audio and video coding, and we evaluate its properties and performance.

Cite as

Tomas Golembiovsky and Ales Krenek. Compression of Vector Field Changing in Time. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 40-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{golembiovsky_et_al:OASIcs.MEMICS.2010.40,
  author =	{Golembiovsky, Tomas and Krenek, Ales},
  title =	{{Compression of Vector Field Changing in Time}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{40--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.40},
  URN =		{urn:nbn:de:0030-drops-30640},
  doi =		{10.4230/OASIcs.MEMICS.2010.40},
  annote =	{Keywords: Protein-ligand docking, vector compression}
}
Document
Automatic C Compiler Generation from Architecture Description Language ISAC

Authors: Adam Husar, Miloslav Trmac, Jan Hranac, Tomas Hruska, and Karel Masarik

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
This paper deals with retargetable compiler generation. After an introduction to application-specific instruction set processor design and a review of code generation in compiler backends, ISAC architecture description language is introduced. Automatic approach to instruction semantics extraction from ISAC models which result is usable for backend generation is presented. This approach was successfully tested on three models of MIPS, ARM and TI MSP430 architectures. Further backend generation process that uses extracted instruction is semantics presented. This process was currently tested on the MIPS architecture and some preliminary results are shown.

Cite as

Adam Husar, Miloslav Trmac, Jan Hranac, Tomas Hruska, and Karel Masarik. Automatic C Compiler Generation from Architecture Description Language ISAC. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 47-53, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{husar_et_al:OASIcs.MEMICS.2010.47,
  author =	{Husar, Adam and Trmac, Miloslav and Hranac, Jan and Hruska, Tomas and Masarik, Karel},
  title =	{{Automatic C Compiler Generation from Architecture Description Language ISAC}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{47--53},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.47},
  URN =		{urn:nbn:de:0030-drops-30654},
  doi =		{10.4230/OASIcs.MEMICS.2010.47},
  annote =	{Keywords: ISAC architecture, compiler generation}
}
Document
Efficient Computation of Morphological Greyscale Reconstruction

Authors: Pavel Karas

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)


Abstract
Morphological reconstruction is an important image operator from mathematical morphology. It is very often used for filtering, segmentation, and feature extraction. However, its computation can be very time-consuming for some input data. In this paper we review several efficient algorithms to compute the reconstruction, and compare their performance on real 3D images of large sizes. Furthermore, we propose a GPU implementation which performs up to 15x faster than the CPU methods. To our best knowledge, this is the first GPU implementation of the morphological reconstruction, described in literature.

Cite as

Pavel Karas. Efficient Computation of Morphological Greyscale Reconstruction. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 54-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{karas:OASIcs.MEMICS.2010.54,
  author =	{Karas, Pavel},
  title =	{{Efficient Computation of Morphological Greyscale Reconstruction}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{54--61},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.54},
  URN =		{urn:nbn:de:0030-drops-30679},
  doi =		{10.4230/OASIcs.MEMICS.2010.54},
  annote =	{Keywords: GPU, morphological reconstruction}
}
  • Refine by Author
  • 5 Vojnar, Tomáš
  • 3 Hruska, Tomas
  • 3 Kozubek, Michal
  • 3 Vojnar, Tomas
  • 2 Antos, David
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Formal software verification
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Separation logic

  • Refine by Keyword
  • 2 GPU
  • 2 bi-abduction
  • 2 low-level pointer operations
  • 2 programs with dynamic linked data structures
  • 2 programs with pointers
  • Show More...

  • Refine by Type
  • 24 document
  • 2 volume

  • Refine by Publication Year
  • 19 2011
  • 3 2009
  • 2 2012
  • 2 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail