检索结果-内蒙古大学图书馆

36th International Conference on Computer-Aided Verification (CAV)

作者： Chiari, Michele Geatti, Luca Gigante, Nicola Pradella, Matteo TU Wien Treitlstr 3 A-1040 Vienna Austria Univ Udine Udine Italy Free Univ Bozen Bolzano Bolzano Italy Politecn Milan Milan Italy

ISBN: (纸本)9783031656262;9783031656279

Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in the Precedence Oriented Temporal Logic (POTL), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of POTL have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, smt-based approach for model checking POTL properties. While previous approaches construct the automaton for both the POTL formula and the model of the program, we encode them into a (sequence of) smt formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an smt-solver, in a Bounded model checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.

关键词： smt-based model checking Tree-shaped Tableau Temporal Logic Operator Precedence Languages

来源：评论

学校读者我要写书评

暂无评论

Inductive Validity Cores

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2021年第2期47卷 279-299页

作者： Ghassabani, Elaheh Whalen, Michael Gacek, Andrew Heimdahl, Mats Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA Adv Technol Ctr Rockwell Collins Cedar Rapids IA 52498 USA

Symbolic model checkers can construct proofs of properties over highly complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, measure completeness of a set of requirements over a model, and assist with design optimization given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute inductive validity cores (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current smt solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as all inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.

关键词： Computational modeling Analytical models Tools Safety Mathematical model Approximation algorithms model checking Inductive validity cores smt-based model checking requirements analysis proof explanation

来源：评论

学校读者我要写书评

暂无评论

Online Enumeration of All Minimal Inductive Validity Cores 16th

Online Enumeration of All Minimal Inductive Validity Cores

引用

16th International Conference on Software Engineering and Formal Methods (SEFM) Held as Part of Conference on Software Technologies - Applications and Foundations (STAF)

作者： Bendik, Jaroslav Ghassabani, Elaheh Whalen, Michael Cerna, Ivana Masaryk Univ Fac Informat Brno Czech Republic Univ Minnesota Dept Comp Sci & Engn Minneapolis MN USA

ISBN: (纸本)9783319929705;9783319929699

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Minimal Inductive Validity Cores (MIVCs) trace a property to a minimal set of model elements necessary for constructing a proof, and can help to explain why a property is true of a model. In addition, the traceability information provided by MIVCs can be used to perform a variety of engineering analysis such as coverage analysis, robustness analysis, and vacuity detection. The more MIVCs are identified, the more precisely such analyses can be performed. Nevertheless, a full enumeration of all MIVCs is in general intractable due to the large number of possible model element sets. The bottleneck of existing algorithms is that they are not guaranteed to emit minimal IVCs until the end of the computation, so returned results are not known to be minimal until all solutions are produced. In this paper, we propose an algorithm that identifies MIVCs in an online manner (i.e., one by one) and can be terminated at any time. We benchmark our new algorithm against existing algorithms on a variety of examples, and demonstrate that our algorithm not only is better in intractable cases but also completes the enumeration of MIVCs faster than competing algorithms in many tractable cases.

关键词： Inductive validity cores smt-based model checking Inductive proofs Traceability Proof cores

来源：评论

学校读者我要写书评

暂无评论

Efficient Generation of All Minimal Inductive Validity Cores 17

Efficient Generation of All Minimal Inductive Validity Cores

引用

17th International Conference on Formal Methods in Computer-Aided Design (FMCAD)

作者： Ghassabani, Elaheh Whalen, Michael Gacek, Andrew Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA Rockwell Collins Adv Technol Ctr Cedar Rapids IA USA

ISBN: (纸本)9780983567875

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Recently, proof cores (alternately, for inductive model checkers, Inductive Validity Cores (IVCs)) were introduced to trace a property to a minimal set of model elements necessary for proof. Minimal IVCs facilitate several engineering tasks, including performing traceability and analyzing requirements completeness, that usually rely on the minimality of IVCs. However, existing algorithms for generating an IVC are either expensive or only able to find an approximately minimal IVC. Besides minimality, computing all minimal IVCs of a given property is an interesting problem that provides several useful analyses, including regression analysis for testing/proof, determination of the minimum (as opposed to minimal) number of model elements necessary for proof, the diversity examination of model elements leading to proof, and analyzing fault tolerance. This paper proposes an efficient method for finding all minimal IVCs of a given property proving its correctness and completeness. We benchmark our algorithm against existing IVC-generating algorithms and show, in many cases, the cost of finding all minimal IVCs by our technique is similar to finding a single minimal IVC using existing algorithms.

关键词： Inductive Validity Cores UNSAT-core generation smt-based model checking Inductive proofs

来源：评论

学校读者我要写书评

暂无评论

Merit and Blame Assignment with Kind 2 26th

Merit and Blame Assignment with Kind 2

引用

26th International Conference on Formal Methods for Industrial Critical Systems (FMICS)

作者： Larraz, Daniel Laurent, Mickael Tinelli, Cesare Univ Iowa Dept Comp Sci Iowa City IA 52242 USA Univ Paris CNRS IRIF Paris France

ISBN: (纸本)9783030852481;9783030852474

We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models. This new version of Kind 2 can identify minimal sets of design elements, known as Minimal Inductive Validity Cores, which are sufficient to prove a given set of safety properties, and also determine the set of MUST elements, design elements that are necessary to prove the given properties. In addition, Kind 2 is able to find minimal sets of design constraints, known as Minimal Cut Sets, whose violation leads the system to an unsafe state. We illustrate with an example how to use the computed information for tracking the safety impact of model changes, and for analyzing the tolerance and resilience of a system against faults.

关键词： smt-based model checking Inductive validity cores Traceability MUST-set generation Minimal Cut Sets

来源：评论

学校读者我要写书评

暂无评论

LTL falsification in infinite-state systems

引用

INFORMATION AND COMPUTATION 2022年第PartA期289卷

作者： Cimatti, Alessandro Griggio, Alberto Magnago, Enrico Fdn Bruno Kessler Trento Italy

In finite-state systems, if an LTL property is false, there is always a counterexample path (i.e. a witness) for it which is ultimately periodic (i.e. in a lasso-shaped form). When dealing with infinite-state systems, this is no longer the case. In this work, we address this issue by proposing an automatic approach that presents witnesses in an indirect way. The approach is based on two key insights. First, we leverage the notion of well-founded funnel, where a ranking function ensures that the states in the source set are guaranteed to inevitably reach the destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. Second, we adopt a compositional approach to partition the original system into projections and to prove that they result in a non-empty under-approximation of the original system that only contains fair paths. Then, we propose an algorithm that, working in an abstract space induced by a set of predicates, identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order. We experimentally evaluate the approach on examples taken from software, timed and hybrid systems, showing its wide applicability and expressiveness, with an implementation that outperforms various competitor tools.(c) 2022 Elsevier Inc. All rights reserved.

关键词： First -order linear -time temporal logic smt-based model checking Temporal satisfiability Infinite -state transition systems

来源：评论

学校读者我要写书评

暂无评论

smt-based satisfiability of first -order LTL with event freezing functions and metric operators ?

引用

INFORMATION AND COMPUTATION 2020年 272卷 104502-104502页

作者： Cimatti, Alessandro Griggio, Alberto Magnago, Enrico Roveri, Marco Tonetta, Stefano FBK Irst Via Sommarive 18 Trento Italy

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (smt)). We show that the “at next” and “at last” can encode (first-order) MTL0,∞ with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in the nuXmv model checker enabling the analysis of LTL-EF and MTL0,∞ based on smt-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

关键词： First-order linear-time temporal logic Metric temporal logic smt-based model checking Temporal satisfiability

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：