scholarly journals Craig Interpolation for the Integers: Results, Implementation, and Experiences

10.29007/9rxz ◽  
2018 ◽  
Author(s):  
Philipp Rümmer
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Safety Analysis ◽  
Craig Interpolation ◽  
Integer Arithmetic ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Versatile Tool ◽  
Runtime Infrastructure

Craig interpolation is a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. Over the last years, a variety of interpolation procedures for linear integer arithmetic (and extensions) have been developed. I will give an overview of the existing algorithms and design choices, and then discuss implementations of such procedures within theorem provers and SMT solvers. In particular, I will describe an implementation done using the multi-paradigm language Scala, which is built on top of the Java runtime infrastructure, and evaluate performance and engineering aspects.

scholarly journals Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

10.29007/zfkw ◽  
2018 ◽  
Author(s):  
Angelo Brillout ◽  
Daniel Kroening ◽  
Philipp Rümmer ◽  
Thomas Wahl
Keyword(s):  
Model Checking ◽  
Program Verification ◽  
Model Checker ◽  
Craig Interpolation ◽  
Presburger Arithmetic ◽  
C Programs ◽  
Full Theory ◽  
Software Model ◽  
Interpolation Procedure ◽  
Versatile Tool

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

scholarly journals Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Research Directions ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

scholarly journals Automatic Synthesis of Generalized Winning Strategies of Impartial Combinatorial Games Using SMT Solvers

2020 ◽  
Author(s):  
Kaisheng Wu ◽  
Liangda Fang ◽  
Liping Xiong ◽  
Zhao-Rong Lai ◽  
Yong Qiao ◽  
...  
Keyword(s):  
Artificial Intelligence ◽  
Game Theory ◽  
Experimental Results ◽  
Combinatorial Games ◽  
Logical Framework ◽  
Automatic Synthesis ◽  
Integer Arithmetic ◽  
Smt Solvers ◽  
Winning Strategies

Strategy representation and reasoning has recently received much attention in artificial intelligence. Impartial combinatorial games (ICGs) are a type of elementary and fundamental games in game theory. One of the challenging problems of ICGs is to construct winning strategies, particularly, generalized winning strategies for possibly infinitely many instances of ICGs. In this paper, we investigate synthesizing generalized winning strategies for ICGs. To this end, we first propose a logical framework to formalize ICGs based on the linear integer arithmetic fragment of numeric part of PDDL. We then propose an approach to generating the winning formula that exactly captures the states in which the player can force to win. Furthermore, we compute winning strategies for ICGs based on the winning formula. Experimental results on several games demonstrate the effectiveness of our approach.

A Methodology for Automatic Formal Verification of Enterprise Architecture

2019 ◽  
Vol 10 (1) ◽  
pp. 1-19
Author(s):  
Eduard Babkin ◽  
Pavel Malyzhenkov ◽  
Marina Ivanova ◽  
Nikita Ponomarev
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Iterative Process ◽  
Enterprise Architecture ◽  
Description Language ◽  
Architecture Description Language ◽  
Business Modeling ◽  
Business Alignment ◽  
Architecture Description ◽  
Software Prototype

For over a decade, IT-business alignment has been ranked as a top-priority management concern, but there is little research on practical ways to achieve the alignment. EA development is a continuous iterative process, which implicitly ensures the achievement of a specific IT-business alignment level. Therefore, it is necessary to formalize the requirements for architecture and be able to automatically verify them. The authors propose a new methodology for detecting logical contradictions in enterprise architecture models based on a model checking approach adopted in the context of business modeling. In such a methodology, they use ArchiMate standard for a conceptual enterprise architecture description language which is fully aligned with TOGAF. The authors also offer several important verification queries and demonstrate practical applicability of their approach using a software prototype of the modeling tool which exploits MIT Alloy Analyzer model checking framework integrated with AchiMate Archi workbench.

scholarly journals System Level Formal Verification via Model Checking Driven Simulation

2013 ◽  
pp. 296-312 ◽  
Author(s):  
Toni Mancini ◽  
Federico Mari ◽  
Annalisa Massini ◽  
Igor Melatti ◽  
Fabio Merli ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
System Level
Sign in / Sign up

Export Citation Format

Share Document