Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate produce unacceptable results. While the numerical methods literature provides techniques mitigate applying these requires manually rearranging expressions understanding finer details of We introduce Herbie, a tool automatically discovers rewrites experts perform improve accuracy. Herbie's heuristic search estimates...

Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate produce unacceptable results. While the numerical methods literature provides techniques mitigate applying these requires manually rearranging expressions understanding finer details of We introduce Herbie, a tool automatically discovers rewrites experts perform improve accuracy. Herbie's heuristic search estimates...

Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues large floating-point applications, must identify root causes, which is difficult because errors are generally non-local, non-compositional, non-uniform.

Formally verifying system properties is one of the most effective ways improving quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpora to synthesize proofs have just begun show their promise. These tools are because richness data contain. This comes stylistic conventions followed communities developers, together with powerful logical systems beneath assistants. However, this remains...

Foundational verification allows programmers to build software which has been empirically shown have high levels of assurance in a variety important domains. However, the cost producing foundationally verified remains prohibitively for most projects, as it requires significant manual effort by highly trained experts. In this paper we present Proverbot9001, proof search system using machine learning techniques produce proofs correctness interactive theorem provers. We demonstrate...

Formal verification is an effective but extremely work-intensive method of improving software quality. Verifying the correctness systems often requires significantly more effort than implementing them in first place, despite existence proof assistants, such as Coq, aiding process. Recent work has aimed to fully automate synthesis formal proofs, little tool support exists for practitioners. This paper presents oofster, a web-based at assisting developers with process via synthesis. oofster...

Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues large floating-point applications, must identify root causes, which is difficult because errors are generally non-local, non-compositional, non-uniform. This paper presents Herbgrind, tool help causes code written low-level languages like C/C++ Fortran. Herbgrind dynamically tracks dependencies between operations program...

Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues large floating-point applications, must identify root causes, which is difficult because errors are generally non-local, non-compositional, non-uniform. This paper presents Herbgrind, tool help causes code written low-level C/C++ Fortran. Herbgrind dynamically tracks dependencies between operations program outputs avoid false...

Proof engineering tools make it easier to develop and maintain large systems verified using interactive theorem provers. Developing useful proof hinges on understanding the development processes of engineers. This paper breaks down one barrier achieving that understanding: remotely collecting granular data developments as they happen.

Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing fall into two broad categories. Some are goal-directed, producing specifically help a user make progress from given proof state, but they have limited expressiveness in terms that can be produced. Other highly expressive, able generate arbitrary grammar, completely undirected and hence not amenable interactive usage. In this paper, we develop...

Formal verification is a promising method for producing reliable software, but the difficulty of manually writing proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding search through space using theorem prover. Unfortunately, prover provides only crudest estimate progress, resulting effectively undirected search. To address this problem, we create QEDCartographer, an proof-synthesis tool that combines supervised and reinforcement...

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, process requires significant expertise and manual effort to write proofs. Recent work has explored automating synthesis machine learning large language models (LLMs). This shown that identifying relevant premises, lemmas definitions, can aid synthesis. We present Rango, a fully automated tool for Coq automatically identifies premises also similar proofs from current project uses...

Formally verifying system properties is one of the most effective ways improving quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from proof corpora to suggest proofs, have just begun show their promise. These tools are because richness data contain. This comes stylistic conventions followed communities developers, together with logical systems beneath assistants. However, this remains...

Web applications often handle large amounts of sensitive user data. Modern secure web frameworks protect this data by (1) using declarative languages to specify security policies alongside database schemas and (2) automatically enforcing these at runtime. Unfortunately, do not the very common situation in which or need evolve over time---and updates be performed a carefully coordinated way. Mistakes during schema policy migrations can unintentionally leak introduce privilege escalation bugs....

Foundational verification allows programmers to build software which has been empirically shown have high levels of assurance in a variety important domains. However, the cost producing foundationally verified remains prohibitively for most projects,as it requires significant manual effort by highly trained experts. In this paper we present Proverbot9001,a proof search system using machine learning techniques produce proofs correctness interactive theorem provers. We demonstrate...