Formal analysis of Java']Java programs in Java']JavaFAN

被引：0
|
作者：
Farzan, A [1 ]
Chen, F [1 ]
Meseguer, J [1 ]
Rosu, G [1 ]
机构：
[1] Univ Illinois, Dept Comp Sci, Urbana, IL 61801 USA
来源：
COMPUTER AIDED VERIFICATION | 2004年 / 3114卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN's implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories.
引用
下载
收藏
页码：501 / 505
页数：5
相关论文
共 50 条
  • [1] Formal JVM code analysis in Java']JavaFAN
    Farzan, A
    Meseguer, J
    Rosu, G
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 132 - 147
  • [2] DynAlloy as a formal method for the analysis of Java']Java programs
    Galeotti, Juan P.
    Frias, Marcelo F.
    SOFTWARE ENGINEERING TECHNIQUES: DESIGN FOR QUALITY, 2006, 227 : 249 - +
  • [3] Formal techniques for Java']Java programs
    Jacobs, B
    Leavens, GT
    Müller, P
    Poetzsch-Heffter, A
    OBJECT-ORIENTED TECHNOLOGY, 1999, 1743 : 97 - 115
  • [4] Formal techniques for Java']Java programs
    Drossopoulou, S
    Eisenbach, S
    Jacobs, B
    Leavens, GT
    Müller, P
    Poetzsch-Heffter, A
    OBJECT-ORIENTED TECHNOLOGY, PROCEEDINGS, 2000, 1964 : 41 - 54
  • [5] Formal Techniques for Java']Java Programs
    Leavens, GT
    Drossopoulou, S
    Eisenbach, S
    Poetzsch-Heffter, A
    Poll, E
    OBJECT-ORIENTED TECHNOLOGY, PROCEEDINGS, 2002, 2323 : 30 - 40
  • [6] Special issue: Formal techniques for Java']Java programs
    Eisenbach, S
    Leavens, GT
    CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2001, 13 (13): : 1121 - 1123
  • [7] Formal techniques for Java']Java-like programs
    Boyland, John
    Clarke, Dave
    Leavens, Gary
    Logozzo, Francesco
    Poetzsch-Heffter, Arnd
    OBJECT-ORIENTED TECHNOLOGY: ECOOP 2007 WORKSHOP READER, 2008, 4906 : 99 - +
  • [8] Formal techniques for Java']Java-like programs
    Eisenbach, S
    Leavens, GT
    Müller, P
    Poetzsch-Heffter, A
    Poll, E
    OBJECT-ORIENTED TECHNOLOGY, 2003, 3013 : 62 - 71
  • [9] Formal verification of protocol properties of sequential Java']Java programs
    Jin, Ying
    COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 475 - 482
  • [10] A dynamic Logic for the formal verification of Java']Java Card programs
    Beckert, B
    JAVA ON SMART CARDS: PROGRAMMING AND SECURITY, 2001, 2041 : 6 - 24
12345