The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. In this paper, we give arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy, we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle large states, and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, run-time analysis and slicing with model checking.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Model checking programs


    Contributors:
    Visser, W. (author) / Havelund, K. (author) / Brat, G. (author) / Park, Seungjoon (author)


    Publication date :

    2000


    Size :

    9 Seiten, 43 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English





    Model Checking

    Dill, D. / United States; National Aeronautics and Space Administration | British Library Conference Proceedings | 1995


    Automated statechart model checking

    Mikk, E. / Pingree, P. J. | NTRS | 2002


    Model checking for autonomous vehicles

    FERGUSON DAVID I / DOLGOV DMITRI A / URMSON CHRISTOPHER | European Patent Office | 2016

    Free access

    Model Checking UAV Mission Plans

    Humphrey, Laura | AIAA | 2012