Zobrazeno 1 - 10
of 209
pro vyhledávání: '"Chlipala, Adam"'
Autor:
Kuepper, Joel, Erbsen, Andres, Gross, Jason, Conoly, Owen, Sun, Chuyue, Tian, Samuel, Wu, David, Chlipala, Adam, Chuengsatiansup, Chitchanok, Genkin, Daniel, Wagner, Markus, Yarom, Yuval
Manual engineering of high-performance implementations typically consumes many resources and requires in-depth knowledge of the hardware. Compilers try to address these problems; however, they are limited by design in what they can do. To address thi
Externí odkaz:
http://arxiv.org/abs/2305.19586
Publikováno v:
J Autom Reasoning 68, 19 (2024)
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and red
Externí odkaz:
http://arxiv.org/abs/2305.02521
Autor:
Kuepper, Joel, Erbsen, Andres, Gross, Jason, Conoly, Owen, Sun, Chuyue, Tian, Samuel, Wu, David, Chlipala, Adam, Chuengsatiansup, Chitchanok, Genkin, Daniel, Wagner, Markus, Yarom, Yuval
Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have the patience to write directly in assembly language. However, cryptograp
Externí odkaz:
http://arxiv.org/abs/2211.10665
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach
Externí odkaz:
http://arxiv.org/abs/2205.00862
As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof assistant evolution. We present the Coq Bug Minimizer, a tool for reproducing buggy behav
Externí odkaz:
http://arxiv.org/abs/2202.13823
Autor:
Bourgeat, Thomas, Clester, Ian, Erbsen, Andres, Gruetter, Samuel, Singh, Pratap, Wright, Andrew, Chlipala, Adam
Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use se
Externí odkaz:
http://arxiv.org/abs/2104.00762
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Though many safety-critical software systems use floating point to represent real-world input and output, programmers usually have idealized versions in mind that compute with real numbers. Significant deviations from the ideal can cause errors and j
Externí odkaz:
http://arxiv.org/abs/1805.00468
Autor:
Delaware, Benjamin, Suriyakarn, Sorawit, Pit--Claudel, Clément, Ye, Qianchuan, Chlipala, Adam
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encode
Externí odkaz:
http://arxiv.org/abs/1803.04870
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to cope with la
Externí odkaz:
http://arxiv.org/abs/1401.7694