Model Checking Programs Export

@inproceedings{citeulike:3846895, abstract = {The majority of 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, proof checkers and model checkers. In this paper we will attempt to give convincing 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 big states, and partial order and symmetry reduction, slicing, abstraction, and runtime 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, runtime analysis, and slicing with model checking.}, author = {Visser, Willem and Havelund, Klaus and Brat, Guillaume}, booktitle = {Automated Software Engineering Journal}, citeulike-article-id = {3846895}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8176}, keywords = {2000, java, modelchecking, thread}, pages = {3--12}, posted-at = {2009-02-05 14:17:50}, priority = {3}, title = {Model Checking Programs}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8176}, volume = {10}, year = {2000} }

TY - CONF ID - citeulike:3846895 L3 - citeulike-article-id:3846895 N2 - The majority of 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, proof checkers and model checkers. In this paper we will attempt to give convincing 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 big states, and partial order and symmetry reduction, slicing, abstraction, and runtime 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, runtime analysis, and slicing with model checking. EP - 12 TI - Model Checking Programs VL - 10 T2 - Automated Software Engineering Journal SP - 3 KW - 2000 KW - java KW - modelchecking KW - thread AU - Visser, Willem AU - Havelund, Klaus AU - Brat, Guillaume PY - 2000/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8176 ER -