Computer Science ›› 2014, Vol. 41 ›› Issue (8): 42-46.doi: 10.11896/j.issn.1002-137X.2014.08.008
Previous Articles Next Articles
ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang
| [1] Matsumoto M,Anada K,Ueshima D,et al．Model Checking ofState Transition Matrix[R]．ITSSV 2005,AIST Technical Report．2005:2-11 [2] Watanabe M．Extended Hierarchy State Transition Matrix Design Method -Version 2.0[R]．CATS Technical Report．1998 [3] Clarke E,Kroening D,Ouaknine J,et al．Completeness and complexity of bounded model checking[C]∥Proceedings of the Ve-rification,Model Checking,and Abstract Interpretation．Springer Berlin Heidelberg,2004:85-96 [4] Clarke E M,Grumberg O,Peled D．Model checking[M]．The MIT press,1999 [5] Armando A,Mantovani J,Platania L．Bounded model checking of software using SMT solvers instead of SAT solvers[M]∥Model Checking Software．Springer Berlin Heidelberg,2006:146-162 [6] Kong Wei-qiang,Fukuda A,Watanabe M．An SMT approach tobounded model checking of design in state transition matrix[C]∥Proceedings of the Computational Science and Its Applications (ICCSA)．2010:231-238 [7] Kong Wei-qiang,Katahira N,Watanabe,et al．Formal verification of software designs in hierarchical state transition matrix with SMT-based bounded model checking[C]∥Proceedings of the Software Engineering Conference (APSEC)．2011:81-88 [8] Latvala T,Biere A,Heljanko K,et al．Simple bounded LTLmodel checking[C]∥Proceedings of the Formal Methods in Computer-Aided Design-2004．2004:186-200 [9] Jussila T,Dubrovin J,Junttila T,et al．Model checking dynamic and hierarchical UML state machines[C]∥Proc．MoDeV2a:Model Development,Validation and Verification．2006:94-110 [10] Dubrovin J,Junttila T．Symbolic model checking of hierarchical UML state machines[C]∥Proceedings of the Application of Concurrency to System Design．2008:108-117 [11] Biere A,Cimatti A,Clarke EM,et al．Symbolic Model Checking without BDDs[C]∥TACAS 1999．1999:193-207 [12] Latvala T,Biere A,Heljanko K,et al．Simple is better:Efficient bounded model checking for past LTL[C]∥Proceedings of the Verification,Model Checking,and Abstract Interpretation．2005:380-395 [13] Lee E A,Seshia S A．Introduction to embedded systems:A cyber-physical systems approach[M]．Lee & Seshia,2011 [14] Barrett C,Sebastiani R,Seshia S A,et al．Satisfiability modulo theories[J]．Handbook of Satisfiability,2009,185:825-885 [15] Veanes M,Bjrner N,Alexander R．An SMT approach tobounded reachability analysis of model programs[C]∥Procee-dings of the Formal Techniques for Networked and Distributed Systems-FORTE 2008．Springer Berlin Heidelberg,2008:53-68 [16] 曾锃,赵建华．基于程序分析的代码查询技术[J].计算机科学,2012,9(2):143-147 [17] 何炎祥,吴伟,陈勇,等．基于 SMT 求解器的路径敏感程序验证[J].软件学报,2012,23(10) [18] Dubrovin J,Junttila T,Heljanko K．Symbolic step encodings for object based communicating state machines[M]．Springer Berlin Heidelberg,2008:96-112 [19] Cousot P．Abstract interpretation based formal methods and fu-ture challenges[C]∥Proceedings of the Informatics．2001:138-156 [20] De Moura L,Bjrner N．Z3:An efficient SMT solver[M]∥Tools and Algorithms for the Construction and Analysis of Systems．Springer Berlin Heidelberg,2008:337-340 |
| No related articles found! |
|
||
Home