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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Model checking programs


    Beteiligte:
    Visser, W. (Autor:in) / Havelund, K. (Autor:in) / Brat, G. (Autor:in) / Park, Seungjoon (Autor:in)


    Erscheinungsdatum :

    2000


    Format / Umfang :

    9 Seiten, 43 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch





    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 of Robot Gathering

    Doan, Ha Thi Thu / Ogata, Kazuhiro | BASE | 2018

    Freier Zugriff

    Model Checking UAV Mission Plans

    Humphrey, Laura | AIAA | 2012