Art

J-GLOBAL ID：200902288653108015   Reference number：07A1187322

Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints

等価性制約下で等式と未解釈関数を伴う論理に対する充足可能性検査

Author (3)： KOZAWA Hiroaki (Osaka Univ., Toyonaka-shi, JPN) ,  HAMAGUCHI Kiyoharu (Osaka Univ., Toyonaka-shi, JPN) ,  KASHIWABARA Toshinobu (Osaka Univ., Toyonaka-shi, JPN)
Material： IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Institute of Electronics, Information and Communication Engineers)  (IEICE Trans Fundam Electron Commun Comput Sci (Inst Electron Inf Commun Eng))
Volume： E90-A  Issue： 12  Page： 2778-2789  Publication year： Dec. 01, 2007 
JST Material Number： F0699C  ISSN： 0916-8508  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： ENGLISH (EN)

Thesaurus term： equivalency ,...
Semi thesaurus term： *formal verification ,...

   To see more with JDream III (charged).   {{ this.onShowAbsJLink("http://jdream3.com/lp/jglobal/index.html?docNo=07A1187322&from=J-GLOBAL&jstjournalNo=F0699C") }}

JST classification (2)： CAD,CAM  (JE10000A) ,  Logic circuits  (NC05070B)

Reference (10)：

• ANDROUS, Z. S. Refinement strategies for verification methods based on datapath abstraction. Asia and South Pacific Design Automation Conference, 2006. 2006, 19-24
• BRYANT, R. E. Exploiting positive equality in a logic of equality with uninterpreted functions. International Conference on Computer Aided Verification 1999. 1999, 470-482
• CURRIE, D. W. Automatic formal verification of DSP software. Design Automation Conference, 2000. 2000, 130-135
• BARRETT, C. W. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. Ph. D. Dissertation, Stanford University. 2003
• FILLIATRE, J.-C. ICS : Integrated canonizer and solver. International Conference on Computer Aided Verification, 2001. 2001, 246-249

Terms in the title (6)： 等価性 ,  制約 ,  関数 ,  論理 ,  充足可能性 ,  検査