首页/论文/0804.3762

arXiv 0804.37622008-04-23cs.LO

从形式证明到数学证明：一种安全的、渐进的一阶决策过程的构建方法

From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub

发表信息：: Dans TCS 2008 5th IFIP International Conference on Theoretical Computer Science (2008)

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们在这里研究了一个新版本的归纳构造演算（CIC），证明助手Coq是基于它的：一致归纳构造演算，它通过构建任意的一阶决策过程来真正扩展CIC：deduction仍然负责CIC内核，而计算则外包给专用的一阶决策程序，这些程序可以从货架上取下来，只要它们提供证明证书。整个系统的可靠性是证书检查器和内核可靠性的增量属性。一个详细的例子表明，由此产生的证明风格变得更接近工作数学家。

英文摘要：

We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order decision procedures: deduction is still in charge of the CIC kernel, while computation is outsourced to dedicated first-order decision procedures that can be taken from the shelves provided they deliver a proof certificate. The soundness of the whole system becomes an incremental property following from the soundness of the certificate checkers and that of the kernel. A detailed example shows that the resulting style of proofs becomes closer to that of the working mathematician.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Encoding Incremental NACs in Safe Graph Grammars using Complementation

In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique. We consider the correctness of our encoding under the assumption that the grammar is safe and NACs are incremental, and outline how this result can be extended to unsafe, attributed grammars.

2020-12-03cs.LO

Incremental Computation of Concept Diagrams

Suppose a formal context K=(G,M,I) is given, whose concept lattice B(K) with an attribute-additive concept diagram is already known, and an attribute column C=(G,{n},J) shall be inserted to or removed from it. This paper introduces and proves an incremental update algorithm for both tasks.

2019-03-06cs.LO

用前向-后向推理和预言简化安全证明

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy

Tel Aviv University（特拉维夫大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）；Weizmann Institute of Science（魏茨曼科学研究所）

本文提出一种增量方法，通过将复杂归纳不变量分解为更简单的证明步骤来简化安全证明。结合前向推理、后向推理和预言步骤，证明了每个规则的正确性，并展示了如何通过增量证明恢复安全不变量，从而减少证明安全性的不变量搜索空间。

2026-04-16cs.LOcs.PL

通过信号时态逻辑规范增量分解的安全规划

Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications

Carnegie Mellon University（卡内基梅隆大学）；Pennsylvania State University（宾夕法尼亚州立大学）

本文提出通过时间分解信号时态逻辑规范为可达性和不变性约束并顺序调度，以提升轨迹规划效率，在线性和非线性系统上优于现有方法。

2024-03-19cs.LOcs.ROcs.SY

Incremental Monoidal Grammars

University of Oxford（牛津大学）；UCL（伦敦大学学院）

In this work we define formal grammars in terms of free monoidal categories, along with a functor from the category of formal grammars to the category of automata. Generalising from the Booleans to arbitrary semirings, we extend our construction to weighted formal grammars and weighted automata. This allows us to link the categorical viewpoint on natural language to the standard machine learning notion of probabilistic language model.

2020-01-10cs.AIcs.FLcs.LO

Incremental Bounded Model Checking of Artificial Neural Networks in CUDA

Federal University of Amazonas（亚马逊联邦大学）；SIDIA Instituto de Ciência e Tecnologia（SIDIA科学技术研究所）；University of Manchester（曼彻斯特大学）

Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for safety-critical systems might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are hardly interpretable. Here we develop and evaluate a novel symbolic software verification framework based on incremental bounded model checking (BMC) to check for adversarial cases and coverage methods in multi-layer perceptron …

2019-07-30cs.LGcs.LOcs.NE

更多相关论文收起更多论文

Evolving the Incremental λ Calculus into a Model of Forward Automatic Differentiation (AD)

Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental $λ$-calculus, or ILC, a "theory of changes" that deploys a formal apparatus allowing the automatic generation of efficient update functions which perform incremental computation. The ILC is not only defined, but given a formal machine-understandable definition---accompanied by mechanically verifiable proofs of various properties, including in particular …

2016-11-10cs.LOcs.PL

用于大规模可验证安全流网络的增量和模块化设计的领域专用语言（初步报告）

A Domain-Specific Language for Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks (Preliminary Report)

我们定义了一个特定领域的语言（DSL）归纳组装流网络从小网络或模块产生任意大的，可互换的功能等效的部分。我们的小网络或模块只是作为这个归纳定义中的构建块才是“小”的（它们的大小没有限制）。与我们的DSL相关联的是一个类型论，这是一个正式的注释系统，用来表达流网络的理想属性，以及在它们的接口上将它们作为不变量执行的规则，即，当我们从较小的网络构建较大的网络时，这些规则保证这些属性得到保留。类型论的先决条件是一个形式语义，即，一个严格的定义，有资格作为可行的流通过网络的实体，可能限制，以满足额外的效率或安全要求。这可以通过两种方式之一来实现，作为指称语义或作为操作（或归约）语义;我们选择第一种优先于第二种，部分是为了避免操作方法中的指数增长重写。我们建立了一个类型系统，并证明了它的可靠性，为我们的DSL。

2011-09-05cs.DCcs.LOcs.PL

增量式、归纳式覆盖率

Incremental, Inductive Coverability

我们给出了一个增量的，归纳的（IC 3）过程来检查良好结构的过渡系统的可覆盖性。我们的程序概括了IC 3程序的安全验证，已成功地应用于有限状态的硬件验证到无限状态良好的结构转换系统。我们表明，我们的程序是健全的，完整的，并终止向下有限的结构良好的过渡系统-其中每个状态有一个有限数量的状态低于它-一类包含扩展的Petri网，广播协议，和有损信道系统。我们已经实现了我们的算法检查覆盖的Petri网。我们描述了如何可以有效地实现该算法，而不使用SMT求解器。我们对标准Petri网基准测试的实验表明，IC 3是具有竞争力的国家的最先进的实现的覆盖性的基础上，符号向后分析或扩展放大和检查算法所需的时间和空间使用。

2013-02-22cs.LO

从zonotope到证明证书：一个用于安全控制包的正式流程

From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes

Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Technical University of Munich（慕尼黑工业大学）；Carnegie Mellon University（卡内基梅隆大学）

本文提出了一种结合高斯可达性算法与形式验证的流程，用于生成安全控制包的证明证书，以提高安全关键系统的可靠性。

2025-09-24cs.LO

自动驾驶交叉口安全的形式化验证

Formal Verification of Intersection Safety for Automated Driving

National Institute of Informatics（国立信息学研究所）；Japanese-French Laboratory for Informatics（日法信息学实验室）；AIST（产业技术综合研究所）；SOKENDAI（综合研究大学院大学）

本文扩展 dFHL 并引入混合控制流图，构建首个面向交叉口场景的 RSS 形式化验证框架，以自动发现并验证安全且不过度保守的控制策略条件。

2023-08-13cs.LOcs.RO

用于安全医疗设备控制的正式定义模式的分布式实时的仿真

Distributed Real-Time Emulation of Formally-Defined Patterns for Safe Medical Device Control

医疗器械及其互操作的安全性是一个尚未解决的问题，导致严重的，有时是致命的事故，病人令人震惊的频率。形式化方法，特别是支持高度可重用和可证明安全的模式，可以实例化到许多设备实例，可以在这方面提供帮助。然而，这仍然留下了一个问题，即如何从逻辑时间上的正式规范传递到可执行的仿真，这些仿真可以在物理时间上与其他设备以及患者和/或医生行为的模拟进行互操作。这项工作提出了一种基于规范的方法，其中虚拟仿真环境可以很容易地从正式规范在实时的【形】Maude开发，并可以支持与其他真实设备和仿真模型的交互。这种一般的方法进行了详细的解释，并说明了两个具体的情况下，这两个实例的一个共同的安全正式模式：一个场景涉及到一个可证明的安全起搏器与模拟心脏的相互作用;另一个涉及到一个安全的控制器的相互作用，病人诱导镇痛与一个真正的注射泵。

2010-09-22cs.LOcs.SE

Formalism for Supporting the Development of Verifiably Safe Medical Guidelines with Statecharts

Illinois Institute of Technology（伊利诺伊理工学院）；San Diego State University（圣地亚哥州立大学）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）

Improving the effectiveness and safety of patient care is the ultimate objective for medical cyber-physical systems. Many medical best practice guidelines exist, but most of the existing guidelines in handbooks are difficult for medical staff to remember and apply clinically. Furthermore, although the guidelines have gone through clinical validations, validations by medical professionals alone do not provide guarantees for the safety of medical cyber-physical systems. Hence, formal verification is also needed. The paper presents the formal semantics for a framework that we developed to support…

2019-09-23cs.CLcs.FLcs.LO