Starý web fakulty najdete na adrese https://old.fit.cvut.cz/.

Laboratoř výzkumu programování

V Laboratoři výzkumu programování (PRL@PRG) se zabýváme hlubším pochopením programovacích jazyků a jejich využitím. Laboratoř vede prof. Jan Vitek z Khoury College of Computer Sciences, Northeastern University v Bostnu.

Více o nás

Administrativní pracovníci

Projekty

Evolving Language Ecosystems

Období
2016 - 2021
Popis
Anotace

Big Code: Škálovatelná analýza rozsáhlých bází programů

Program
OPVVV - Operační program Výzkum, vývoj a vzdělávání - Strukturální fondy EU
Období
2019 - 2022
Popis
V rámci projektu BigCode bude na Českém vysokém učení technickém v Praze, Fakultě informačních technologií (FIT) vytvořen Institut pro škálovatelnou analýzu kódu (ISCA), první výzkumné centrum v ČR zaměřené na analýzu rozsáhlých bází programových kódů na internetu, které představují obrovský znalostní potenciál, který ale neumíme zatím využít. Projekt BigCode si klade za cíl tuto bázi pomocí technik programovacích jazyků a statistického strojového učení zanalyzovat a umožnit porozumění získaným informacím. Požadované prostředky budou použity na vybudování hardwarové a softwarové infrastruktury centra a na mzdové prostředky pro mezinárodně uznávané výzkumné pracovníky. Výzkumná náplň projektu je v souladu s již existujícím výzkumem na FIT -- softwarové a znalostní inženýrství, vytěžování dat, paralelní výpočty. Díky mezinárodním kontaktům členů výzkumného týmu projektu BigCode centrum následně předpokládá získávání podpory od předních softwarových firem, jako jsou Google a Oracle.

Publikace

Online Abstraction with MDP Homomorphisms for Deep Learning

Autoři
Bíža, O.; Platt, R.
Rok
2019
Publikováno
Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems. New York: ACM, 2019. p. 1125-1133. ISSN 2523-5699. ISBN 978-1-4503-6309-9.
Typ
Stať ve sborníku
Anotace
Abstraction of Markov Decision Processes is a useful tool for solving complex problems, as it can ignore unimportant aspects of an environment, simplifying the process of learning an optimal policy. In this paper, we propose a new algorithm for finding abstractMDPs in environments with continuous state spaces. It is based on MDP homomorphisms, a structure-preserving mapping betweenMDPs. We demonstrate our algorithm’s ability to learn abstractions from collected experience and show how to reuse the abstractions to guide exploration in new tasks the agent encounters. Our novel task transfer method outperforms baselines based on a deep Q-network in the majority of our experiments. The source code is at https://github.com/ondrejba/aamas_19.

R melts brains: an IR for first-class environments and lazy effectful arguments

Autoři
Flückiger, O.; Hain, J.; Chari, G.; Ječmen, J.; Vítek, J.; Yee, M.
Rok
2019
Publikováno
Proceedings of the 15th ACM SIGPLAN International Symposium on Dynamic Languages. ACM New York, 2019. p. 55-66. ISBN 978-1-4503-6996-1.
Typ
Stať ve sborníku
DOI
10.1145/3359619.3359744
Anotace
The R programming language combines a number of features considered hard to analyze and implement efficiently: dynamic typing, reflection, lazy evaluation, vectorized primitive types, first-class closures, and extensive use of native code. Additionally, variable scopes are reified at runtime as first-class environments. The combination of these features renders most static program analysis techniques impractical, and thus, compiler optimizations based on them ineffective. We present our work on PIR, an intermediate representation with explicit support for first-class environments and effectful lazy evaluation. We describe two dataflow analyses on PIR: the first enables reasoning about variables and their environments, and the second infers where arguments are evaluated. Leveraging their results, we show how to elide environment creation and inline functions.

Všechny publikace

Can android run on time? Extending and measuring the android platform's timeliness

Autoři
Dantu, K.; Gokul, G.; Ko, S.Y.; Vítek, J.; ZIAREK, L.; Yan, Y.
Rok
2019
Publikováno
ACM Transactions on Embedded Computing Systems. 2019, 17(6), ISSN 1539-9087.
Související osoby
Typ
Článek
DOI
10.1145/3289257
Anotace
Time predictability is dificult to achieve in the complex, layered execution environments that are common inmodern embedded devices such as smartphones. We explore adopting the Android programming model for arange of embedded applications that extends beyond mobile devices, under the constraint that changes towidely used libraries should be minimized. The challenges we explore include: the interplay between real-timeactivities and the rest of the system, how to express the timeliness requirements of components, and how wellthose requirements can be met on stock embedded platforms. We detail the design and implementation of ourmodifications to the Android framework along with a real-time VM and OS, and provide experimental datavalidating feasibility over five applications.

 How to Evaluate the Performance of Gradual Type Systems

Autoři
Greeman, B.; Vítek, J.; Felleisen, M.; Feltey, D.; Findler, R.B.; New, M.S.; Takikawa, A.
Rok
2019
Publikováno
JOURNAL OF FUNCTIONAL PROGRAMMING. 2019, 29 ISSN 0956-7968.
Související osoby
Typ
Článek
DOI
10.1017/S0956796818000217
Anotace
A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interaction between typed and untyped components. The literature on gradual typing lacks rigorous descriptions of methods for measuring the performance of gradual type systems. This gap has consequences for the implementors of gradual type systems and developers who use such systems. Without systematic evaluation of mixed-typed programs, implementors cannot precisely determine how improvements to a gradual type system affect performance. Developers cannot predict whether adding types to part of a program will significantly degrade (or improve) its performance. This paper presents the first method for evaluating the performance of sound gradual type systems. The method quantifies both the absolute performance of a gradual type system and the relative performance of two implementations of the same gradual type system. To validate the method, the paper reports on its application to twenty programs and three implementations of Typed Racket.

Feature-specific profiling

Autoři
Andersen, L.; Felleisen, M.; St-Amour, V.; Vítek, J.
Rok
2019
Publikováno
ACM Transactions on Programming Languages and Systems. 2019, 41(1), ISSN 0164-0925.
Související osoby
Typ
Článek
DOI
10.1145/3275519
Anotace
While high-level languages come with significant readability and maintainability benefits, their performance remains difficult to predict. For example, programmers may unknowingly use language features inappropriately, which cause their programs to run slower than expected. To address this issue, we introduce feature-specific profiling, a technique that reports performance costs in terms of linguistic constructs. Feature-specific profilers help programmers find expensive uses of specific features of their language. We describe the architecture of a profiler that implements our approach, explain prototypes of the profiler for two languages with different characteristics and implementation strategies, and provide empirical evidence for the approach's general usefulness as a performance debugging tool. © 2018 Copyright held by the owner/author(s).

Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

Autoři
Cachera, D; Demange, D; Jagannathan, S; Petri, G; Pichardie, D; Vítek, J.; Zakowski, Y
Rok
2017
Publikováno
International Conference on Interactive Theorem Prooving (ITP). Berlin: Springer-Verlag, 2017.
Související osoby
Typ
Stať ve sborníku

Kde nás najdete?

Laboratoř výzkumu programování
Fakulta informačních technologií
České vysoké učení technické v Praze

Místnost TH:A-1250, 1252, 1254
(Budova A, 12. patro)
Thákurova 7
Praha 6 – Dejvice
160 00

Kontaktní osoba

Ing. Lucie Lerch

Za obsah stránky zodpovídá: doc. Ing. Štěpán Starosta, Ph.D.