arXiv 1606.059472016-06-20cs.LO

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli

备注：: In Proceedings HaTT 2016, arXiv:1606.05427
发表信息：: EPTCS 210, 2016, pp. 21-29
DOI：: 10.4204/EPTCS.210.5

英文摘要：

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

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

继续探索

相关论文

ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The exp…

2021-11-25cs.LO

BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)

Program verification on concurrent programs is a big challenge due to general undecidable results. Petri nets and its extensions are used in most works. However, existing verifiers based on Petri nets are difficult to be complete and efficient. Basic Parallel Process (BPP), as a subclass of Petri nets, can be used as a model for describing and verifying concurrent programs with lower complexity. We propose and implement BPPChecker, the first model checker for verifying a subclass of CTL on BPP. We propose constraint-based algorithms for the problem of model checking on BPPs and handle formulas…

2021-10-25cs.FLcs.LO

SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking

In semi-symbolic (control-explicit data-symbolic) model checking the state-space explosion problem is fought by representing sets of states by first-order formulas over the bit-vector theory. In this model checking approach, most of the verification time is spent in an SMT solver on deciding satisfiability of quantified queries, which represent equality of symbolic states. In this paper, we introduce a new scheme for decomposition of symbolic states, which can be used to significantly improve the performance of any semi-symbolic model checker. Using the decomposition, a model checker can issue…

2017-11-20cs.LOcs.PL

A Decision Procedure for Separation Logic in SMT

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL($T$) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model c…

2016-05-19cs.LO

Cargo Sherlock: 基于 SMT 的软件信任成本检查器

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

University of California, Davis（加州大学戴维斯分校）

Cargo Sherlock 是一种基于 SMT 的软件信任成本检查器，通过结合形式化方法和人为因素，用于检测供应链攻击并评估软件依赖项的信任成本。

2026-02-03cs.LOcs.SE

First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving

In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate…

2021-09-07cs.LO

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

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)

We propose DAB -- a data-aware extension of BPMN where the process operates over case and persistent data (partitioned into a read-only database called catalog and a read-write database called repository). The model trades off between expressiveness and the possibility of supporting parameterized verification of safety properties on top of it. Specifically, taking inspiration from the literature on verification of artifact systems, we study verification problems where safety properties are checked irrespectively of the content of the read-only catalog, and accepting the potential presence of u…

2019-06-24cs.LO

Interpolation and the Array Property Fragment

Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, otherwise. This approach works well for quantifier-free theories, like equality theory or linear arithmetic. For quantified formulas, there are SMT solvers that can decide expressive fragments of quantified formulas, e. g., EPR, the array property fragment, and the finite almost uninterpreted fragment. However, these solvers do not support in…

2019-04-25cs.LO

基于SMT求解器的多线程软件有界模型检验

Bounded Model Checking of Multi-threaded Software using SMT solvers

从单核处理器到多核处理器的过渡使得多线程软件成为计算机辅助验证的一个重要课题。在这里，我们描述和评估的ESBMC模型检查器的扩展，以支持验证多线程软件共享的变量和锁使用有界模型检验（BMC）的基础上可满足性模理论（SMT）。我们描述了三种方法来模型检查多线程软件和我们的建模的同步原语的Pthread库。在惰性方法中，我们生成所有可能的交织，并分别对每个交织调用BMC过程，直到我们找到一个bug，或者系统地探索了所有交织。在时间表记录方法中，我们将所有可能的交织编码成一个单一的公式，然后利用SMT求解器的高速。在欠近似加宽方法中，我们通过从SMT求解器生成的不可满足性证明中提取状态变量和交织的数量来减少状态空间。在所有这三种方法中，我们都使用了部分降阶（POR）技术来减少交织的数量。实验表明，我们的方法可以分析更大的问题，并大大减少验证时间相比，国家的最先进的技术，结合经典的POR方法与符号算法和其他实现反例引导抽象细化技术。

2010-03-19cs.LOcs.SE

Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version)

We present an alternative approach to solve the hardware (HW) and software (SW) partitioning problem, which uses Bounded Model Checking (BMC) based on Satisfiability Modulo Theories (SMT) in conjunction with a multi-core support using Open Multi-Processing. The multi-core SMT-based BMC approach allows initializing many verification instances based on processors cores numbers available to the model checker. Each instance checks for a different optimum value until the optimization problem is satisfied. The goal is to show that multi-core model-checking techniques can be effective, in particular …

2015-09-08cs.LOcs.SE

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

We describe a new SMT bit-blasting API for floating-points and evaluate it using different out-of-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floating-point API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using floating-point API, outperforms the solvers with native support for floating-points, correctly verifying more programs in less time. Experimental results also show t…

2020-04-29cs.LOcs.SE

Verification of Data-Aware Processes via Array-Based Systems (Extended Version)

We study verification over a general model of artifact-centric systems, to assess (parameterized) safety properties irrespectively of the initial database instance. We view such artifact systems as array-based systems, which allows us to check safety by adapting backward reachability, establishing for the first time a correspondence with model checking based on Satisfiability-Modulo-Theories (SMT). To do so, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems, and represents the main origi…

2019-02-27cs.LO

Imandra中用于深度神经网络验证的认证证明检查器

A Certified Proof Checker for Deep Neural Network Verification in Imandra

针对DNN验证器信任问题，本文在Imandra中实现Marabou证书检查，获得证书正确性完整证明，提供更强独立保证并推动DNN验证器与ITP结合。

2025-06-24cs.AIcs.LOcs.PL

用于表达性精化类型的基础约束求解

Foundational Constraint Solving for Expressive Refinement Typing

Independent（独立研究者）；University of California San Diego（加州大学圣地亚哥分校）；University of Chile（智利大学）

研究基于SMT的程序验证器的问题，提出在LEAN中实现的基础约束Horn子句求解器FLEX。通过编码CHC为LEAN命题、实现验证CHC生成器及利用LEAN证明机制超越SMT限制，自动消除95.7%的CHC，证明其作为可信CHC后端的可行性。

2026-07-15cs.LOcs.PLcs.SE