编辑与验证
计算机科学中的逻辑
2007-08-07 v1
摘要
自动定理证明器被用于扩展静态检查，其中它们是性能瓶颈。扩展静态检查器通常在代码发生增量更改后运行。我们建议利用这种使用模式来提高性能。我们提出了两种实现方法以及一个完整的解决方案。
引用
@article{arxiv.0708.0713,
title = {Edit and verify},
author = {Radu Grigore and Michał Moskal},
journal= {arXiv preprint arXiv:0708.0713},
year = {2007}
}
相关论文
查看更多相关论文 →
编程语言 · 计算机科学
Iteratively Composing Statically Verified Traits
Isaac Oscar Gariano, Marco Servetto, Alex Potanin, Hrshikesh Arora
2019-08-21
编程语言 · 计算机科学
An Approach to Static Performance Guarantees for Programs with Run-time Checks
Maximiliano Klemen, Nataliia Stulova, Pedro Lopez-Garcia, José F. Morales +1
2018-04-09
编程语言 · 计算机科学
Stratified Static Analysis Based on Variable Dependencies
David Monniaux, Julien Le Guen
2011-09-13
计算机科学中的逻辑 · 计算机科学
Mining State-Based Models from Proof Corpora
Thomas Gransden, Neil Walkinshaw, Rajeev Raman
2014-05-15
计算机科学中的逻辑 · 计算机科学
SCTL: Towards Combining Model Checking and Proof Checking
Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji
2017-10-03
计算机科学中的逻辑 · 计算机科学
Automatic verification and interactive theorem proving
Andrea Asperti
2017-01-16
计算机科学中的逻辑 · 计算机科学
Hammering Higher Order Set Theory
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025-09-11
计算机科学中的逻辑 · 计算机科学
Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
Manqing Zhang, Yunwei Dong, Lingru Zhou, Bingxu Xiao +1
2026-04-28
编程语言 · 计算机科学
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)
Felix A. Wolf, Malte Schwerhoff, Peter Müller
2021-08-16
计算机科学中的逻辑 · 计算机科学
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)
Giles Reger, Martin Suda, Andrei Voronkov
2017-04-12
软件工程 · 计算机科学
A Survey on Theorem Provers in Formal Methods
M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun +1
2019-12-09
计算机科学中的逻辑 · 计算机科学
Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
David Monniaux
2024-07-12
人工智能 · 计算机科学
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek, David Cerna, Thibault Gauthier, Jan Jakubův +3
2025-06-23
计算机科学中的逻辑 · 计算机科学
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
Mertcan Temel
2022-05-25
编程语言 · 计算机科学
Correctness is Demanding, Performance is Frustrating
Artjoms Sinkarovs, Thomas Koopman, Sven-Bodo Scholz
2024-06-18
机器学习 · 统计学
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
Sho Sonoda, Shunta Akiyama, Yuya Uezato
2026-05-26
编程语言 · 计算机科学
Exploiting Term Hiding to Reduce Run-time Checking Overhead
Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo
2017-10-17
计算机科学中的逻辑 · 计算机科学
Proof Simplification and Automated Theorem Proving
Michael Kinyon
2021-01-19
软件工程 · 计算机科学
Execution-free Program Repair
Li Huang, Bertrand Meyer, Ilgiz Mustafin, Manuel Oriol
2024-05-10
软件工程 · 计算机科学
Re-evaluation of Logical Specification in Behavioural Verification
Radoslaw Klimek, Jakub Semczyszyn
2025-05-26
计算机科学中的逻辑 · 计算机科学
Automatic Error Localization for Software using Deductive Verification
Robert Koenighofer, Ronald Toegl, Roderick Bloem
2014-09-17
编程语言 · 计算机科学
VeriFly: On-the-fly Assertion Checking via Incrementality
Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Victor Perez-Carrasco, Jose F. Morales +2
2021-08-18
计算机科学中的逻辑 · 计算机科学
How the Analyzer can Help the User Help the Analyzer
Yannick Moy
2021-08-09
人工智能 · 计算机科学
InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying +4
2025-10-22
软件工程 · 计算机科学
Initial steps towards assessing the usability of a verification tool
Mansur Khazeev, Victor Rivera, Manuel Mazzara, Leonard Johard
2017-06-20