Zobrazeno 1 - 9
of 9
pro vyhledávání: '"KuncakViktor"'
Publikováno v:
OOPSLA
We consider from a practical perspective the problem of checking equivalence of context-free grammars. We present techniques for proving equivalence, as well as techniques for finding counter-examples that establish non-equivalence. Among the key bui
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4c5551a31b92c7001f9c7d82cfeb8cc7
https://doi.org/10.1145/2814270.2814304
https://doi.org/10.1145/2814270.2814304
Autor:
KuncakViktor, DarulovaEva
Publikováno v:
POPL
Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued implementation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7463d8d6148f839e1b880255f58b7dd4
https://doi.org/10.1145/2535838.2535874
https://doi.org/10.1145/2535838.2535874
Publikováno v:
OOPSLA
We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complet
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b30ddfbfbcdc24914c6efaf0f2cbaec
https://doi.org/10.1145/2509136.2509555
https://doi.org/10.1145/2509136.2509555
Publikováno v:
PLDI
Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::093bab0903dae3010d70fae762ccd23f
https://doi.org/10.1145/2491956.2462192
https://doi.org/10.1145/2491956.2462192
Autor:
DarulovaEva, KuncakViktor
Publikováno v:
OOPSLA
Modern computing has adopted the floating point type as a default way to describe computations with real numbers. Thanks to dedicated hardware support, such computations are efficient on modern architectures, even in double precision. However, rigoro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b08834ed6a17a1ab07af15bae3d80364
https://doi.org/10.1145/2048066.2048094
https://doi.org/10.1145/2048066.2048094
Publikováno v:
PLDI
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way - they should succeed for a we
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9a30bc330c30ba57264aac1a43a52288
https://doi.org/10.1145/1806596.1806632
https://doi.org/10.1145/1806596.1806632
Publikováno v:
POPL
We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a22cc84f87f0689bcbb23a1937b34922
https://doi.org/10.1145/1706299.1706325
https://doi.org/10.1145/1706299.1706325
Publikováno v:
PLDI
We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verif
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::748bfa2ac420d26e2208e38731c59f5d
https://doi.org/10.1145/1375581.1375624
https://doi.org/10.1145/1375581.1375624
Publikováno v:
MIT Web Domain
OOPSLA
OOPSLA
We present an efficient, modular, and feature-rich framework for automated generation and validation of complex structures, suitable for tasks that explore a large space of structured values. Our framework is capable of exhaustive, incremental, paral
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::490f95e46aaed32ea0a43f23a544004e
https://infoscience.epfl.ch/record/216773
https://infoscience.epfl.ch/record/216773
