• 検索結果がありません。

変数値域を限定した試行に基づく高次制約問題の充足可能性推定方法の検討

N/A
N/A
Info
ダウンロード
Protected

Academic year: 2021

シェア "変数値域を限定した試行に基づく高次制約問題の充足可能性推定方法の検討"

Copied!
1
0
0

読み込み中.... (全文を見る)

今ダウンロードする ( 1 ページ )

全文

(1)情報処理学会論文誌. プログラミング. Vol.10 No.1 34 (Jan. 2017). 発表概要. 変数値域を限定した試行に基づく高次制約問題の 充足可能性推定方法の検討 中山 寛己1,a). 高野 保真1. 千代 英一郎1. 2016年6月10日発表. 近年，SMT ソルバの研究がさかんに行われてきており，様々な制約問題を解けるよう飛躍的に進歩して いる．しかしながら，SMT ソルバは線形制約式の解を短時間で求められることが多いのに対し，高次の制 約式の解を求めるのに時間がかかってしまうことがある．たとえば，代表的なプログラム検査であるルー プ停止性検査等で必要となる複雑な制約式の場合，検査に数日を要することもあり，実用上の課題となっ ている．この問題に対して，本発表では，変数のとりうる値域を限定した検査を，値域を変えて繰り返す ことで，制約式の充足可能性を推定する方法について報告する．それぞれの試行を短い時間で打ち切るこ とにより，結果が得られないことを避けることができる．. Estimation of Satisfiability for High Order Constraint Problem Based on Trials with Range Restriction of Variabels Hiroki Nakayama1,a). Yasunao Takano1. Eichiro Chishiro1. Presented: June 10, 2016. In recent years, studies of SMT solvers are conducted flourishingly and progress drastically to be able to solve various constraint satisfaction problems. However, while the SMT solver tends to find solution of linear constraints efficiently, it may take a few days to find solutions of the higher degree constraints needed for checking loop termination. For this problem, we examine methods to estimate the satisfiability of constraints by iterative checking (trial) with range restriction of variables. In this presentation, we report some experimental results about trial.. 1. a). 成蹊大学大学院理工学研究科 Graduate School of Science and Technology, Seikei University, Musashino, Tokyo 180–8633, Japan [email protected]. c 2017 Information Processing Society of Japan . 34.

(2)

参照

今ダウンロードする ( PDF - 1 ページ - 92.28 KB )

関連したドキュメント

We introduce some of the basic ideas of this theory in the context of dynam- ical system models of speciation in evolution

The general context for a symmetry- based analysis of pattern formation in equivariant dynamical systems is sym- metric (or equivariant) bifurcation theory.. This is surveyed

Here, we examine the same question for singular equations, but we refer the reader to [12] for a more detailed description of the history of this problem

[9] DiBenedetto, E.; Gianazza, U.; Vespri, V.; Harnack’s inequality for degenerate and singular parabolic equations, Springer Monographs in Mathematics, Springer, New York (2012),

In this article, we establish the existence of nontrivial solutions by employing the fibering method introduced by Pohozaev

Recently, Velin [44, 45], employing the fibering method, proved the existence of multiple positive solutions for a class of (p, q)-gradient elliptic systems including systems

In this work, we present some sensitivity results arising from the solution of the PDE

We use these to show that a segmentation approach to the EIT inverse problem has a unique solution in a suitable space using a fixed point

We show the existence of the traveling wave so- lutions for this system by this iteration scheme

A monotone iteration scheme for traveling waves based on ordered upper and lower solutions is derived for a class of nonlocal dispersal system with delay.. Such system can be used

In this article, we study a free boundary problem modeling the growth of tumors with drug application

In this article we study a free boundary problem modeling the tumor growth with drug application, the mathematical model which neglect the drug application was proposed by A..

ACTA UNIVERSITATIS APULENSIS No 18/2009

In this paper, we establish some iterative methods for solving real and complex zeroes of nonlinear equations by using the modified homotopy perturbation method which is mainly due

ALMOST STABLE ITERATION SCHEMES FOR LOCAL STRONGLY PSEUDOCONTRACTIVE AND LOCAL STRONGLY ACCRETIVE OPERATORS IN REAL UNIFORMLY SMOOTH BANACH SPACES

In this paper we establish the strong convergence and almost stability of the Ishikawa iteration methods with errors for the iterative approximations of either fixed points of